Neue Frage
0

LTL / CTL queries

gefragt 2017-08-19 18:54:12 +0200

blackmamba Gravatar-Bild

aktualisiert 2017-08-19 18:55:17 +0200

How are these derived?

([!a W b] & Fb) -> [!a SW b]
G(a&b) -> FGb
GFa -> Fa
bearbeiten retag Als beleidigend melden schließen löschen

1 Antwort

2

geantwortet 2017-08-19 20:25:46 +0200

PS Gravatar-Bild

These are all LTL formulas, and you are asking how to prove their validity. I will show you that for the last one, i.e., $ GFa \to Fa$ in three different ways below.

The first way would be to prove it by the semantics: The following are easily seen to be equivalent to each other by the definition of the semantics of LTL:

  • $K,\pi,0 \models GFa \to Fa$
  • $K,\pi,0 \models GFa$ implies $K,\pi,0 \models F a$
  • $\forall t_0. K,\pi, t_0 \models Fa$ implies $\exists t_2. K,\pi,t_2 \models a$
  • $\forall t_0. \exists t_1. t_0\leq t_1 \wedge K,\pi, t_1 \models a$ implies $\exists t_2. K,\pi,t_2\models a$

The latter is easily seen to hold when you instantiate $t_0 := 0$ in the assumption (so you obtain $\exists t_1. K,\pi, t_1 \models a$) and get the conclusion by renaming $t_2 := t_1$.

A second way would be to use a calculus to derive the validity, e.g. similar to a sequent calculus (as you may find on https://www.csc.kth.se/~mfd/Courses/Temporal_logic/lecture2.pdf). That has not been considered in VRS.

A third and fully automated way (that can also be used for LTL model checking) is to translate the negation of the formula to an equivalent $\omega$-automaton and check its emptiness. For $GFa \to Fa$, we first abbreviate $Fa$ by $q_0$ and then $Gq_0$ by $q_1$ so that we finally obtain the following Büchi automaton for the negation $\neg(GFa \to Fa)$:

  • initial states $!(q_1\to q_0)$
  • transition relation $(q_0\leftrightarrow a\vee next(q_0)) \wedge (q_1\leftrightarrow q_0\wedge next(q_1))$
  • acceptance condition $GF(q_0\to a)$

Looking at the state transition diagram reveals that the single initial state has no outgoing transition, so the $\omega$-automaton does not accept any word. Hence, the negation of the formula is unsatisfiable, and thus, the original formula is valid.

Bildbeschreibung

You can use the online tool http://es.cs.uni-kl.de/tools/teaching/TemporalLogicProver.html to check LTL formulas for validity (it will also generate a counterexample in case the formula will not be valid).

For CTL or even CTL*, one could follow similar ways, but we would need tree automata to describe them.

bearbeiten Als beleidigend melden löschen publish Link mehr

Ihre Antwort

Du kannst deinen Eintrag bereits als Gast verfassen. Deine Antwort wird zwischengespeichert, bis du dich eingeloggt oder registriert hast.
Bitte nur konstruktive Antworten auf diese konkrete Frage posten.
Falls du eine Frage stellen willst, dann stelle eine neue Frage.
Für kurze Diskussionen und Nachfragen benutze bitte die Kommentar-Funktion.
Deine Fragen und Antworten kannst du jederzeit nachbearbeiten und verbessern.
Gute Fragen und Antworten kannst du mit einem Upvote oder Downvote bewerten.

Schreibe deine Antwort auf diese Frage

[Vorschau ausblenden]

Fragen-Tools

Beobachten
1 Follower

Statistik

Gefragt: 2017-08-19 18:54:12 +0200

Gesehen: 23 mal

Letztes Update: Aug 19