Musterlösung

Ludwig-Maximilians-Universität München
SoSe 2015
Institut für Informatik
Dr. M. Hölzl, C. Kroiÿ
Formale Techniken der Software-Entwicklung
Übungsblatt 9
Besprechung am 03.07.2015
Musterlösung
Aufgabe 1:
Gegeben sei das Transitionssystem
M
in Abbildung 1.
r
p,t,r
p, q
q,r
Abbildung 1: Transitionssystem
(a) Zeichnen Sie, beginnend bei Zustand s0 , die entfalteten Ablauf-Pfade des Transitionssystems
zu einer Pfadlänge von 4.
Lösung:
M bis
FTSE SoSe 2015 - Übungsblatt 9
Musterlösung
Seite 2/3
(b) Entscheiden Sie für die folgenden CTL- bzw. LTL-Formeln
φ1 bis φn , ob M, s0 |= φi und M, s2 |= φi
gilt und begründen Sie Ihre Antwort.
(i)
(ii)
(iii)
(iv)
(v)
(vi)
(vii)
(viii)
φ1
φ2
φ3
φ4
φ5
φ6
φ7
φ8
:= ¬p =⇒ r
:= F t
:= ¬ E G r
:= E(t U q)
:= F q
:= E F q
:= E G r
:= G(r ∨ q)
Lösung:
(i)
(ii)
φ1
gilt in
φ2
gilt nicht in
s0
und
Transition nach
s2
weil in beiden
r
gilt.
s0 weil es die Möglichkeit
s1 erfolgen muss.
einer Endlosschleife gibt.
φ2
gilt in
s2 ,
weil die
(iii)
φ3
gilt weder in
s0
noch in
s2
weil von beiden aus einen Pfad gibt, auf dem immer
(iv)
φ4
gilt weder in
s0
noch in
s2
weil
(v)
φ5
gilt nicht in
(vi)
φ6
gilt in
s0
und in
(vii)
φ7
gilt in
s0
wegen der Endlosschleife und in
(viii)
φ8
gilt in in
s0
s0
aber in
s2
und in
s2 ,
t
r
gilt.
in beiden Zuständen nicht gilt.
siehe ii)
weil von
s0
aus
s3
erreichbar ist und
s2
weil
r
q
sowieso in
sowohl in
s2
s2
gilt.
als auch in
s1
gilt.
s2 .
Aufgabe 2:
Drücken Sie die folgenden Eigenschaften falls möglich in CTL und LTL aus. Wenn die Eigenschaft weder
∗
in CTL noch in LTL ausdrückbar ist, versuchen Sie es mit CTL .
(a) Immer wenn auf
p
nach einer endlichen Anzahl von Schritten
Phase ein, während der kein
r
eintritt bevor schlieÿlich
Lösung:
CTL:
LTL:
A G(p =⇒ A X A G(¬q ∨ A[¬r U t]))
G(p =⇒ X G(¬q ∨ ¬r U t))
t
gilt.
q
folgt, dann tritt das System in eine
FTSE SoSe 2015 - Übungsblatt 9
(b) Ereignis
p
Musterlösung
Seite 3/3
geht in allen Ablaufpfaden sowohl
s
als auch
t
voraus.
Hinweis:
Es kann hilfreich sein,
zunächst die Negation dieser Eigenschaft zu formulieren.
Lösung:
¬(E ¬p U(s ∨ t)) ≡ A ¬(¬p U(s ∨ t)) ≡ A p R ¬(s ∨ t)
LTL: p R ¬(s ∨ t)
Hierbei wurde die Äquivalenz ¬(φ U ψ) ≡ ¬φ R ¬ψ verwendet.
CTL:
(c) Für alle Ausführungspfade gilt: Nach
ist
p
q
niemals wahr.
Lösung:
LTL:
CTL:
G(p =⇒ G ¬q)
A G(p =⇒ A G ¬q)
(d) Zwischen den Ereignissen
q
und
r
is
p
niemals wahr.
Lösung:
LTL:
G q =⇒ ((¬p U r) ∨ G ¬r)
(e) Transitionen zu Zuständen, in denen
p
wahr ist, treten höchstens zweimal auf.
Lösung:
G((¬p ∧ X p) =⇒ G((¬p ∧ X p) =⇒ G ¬(p ∧ X p)))
(f ) Es gibt einen Ausführungspfad, auf dem
Lösung:
Wenn an die Aussage so versteht, dass
p
in jedem zweiten Zustand wahr ist.
p genau in jedem 2. Zustand wahr sein soll und annimmt,
dass man mit dem 2. Schritt ausgehend vom Anfangszustand anfängt:
∗
CTL :
E ¬p ∧ G((¬p =⇒ X p) ∧ (p =⇒ X ¬p))

Download Report