Neue Frage
1

Basic difference between CTL/LTL/CTL*

gefragt 2017-08-17 12:36:43 +0100

blackmamba Gravatar-Bild

aktualisiert 2017-08-17 12:36:57 +0100

As far as I understand LTL has path quantifiers only - A,E, [a U b], [a W b], [a B b]

CTL has path quantifiers followed by state quantifiers - AFa

And CTL* has no restriction.

How would I know if the formula is both CTL and LTL? How do I distinguish? What is the basic difference that I need to remember to distinguish between LTL, CTL?

Also, why is this E[(¬a) W b] a CTL and not LTL?

Can you please explain all the three types with suitable example?

bearbeiten retag Als beleidigend melden schließen löschen

1 Antwort

4

geantwortet 2017-08-17 16:08:03 +0100

PS Gravatar-Bild

To start with: U,W,B,G,F, and X are temporal operators which are defined on paths, but they do not quantify on paths. Instead, A and E are path quantifiers, which means something should hold on all infinite or some infinite paths. We do not have state quantifiers, so please call U,W,B,G,F, and X just temporal operators.

Historically, people have defined LTL just on infinite paths and not even on Kripke structures. Thus, they just said the following were LTL formulas (I am ignoring here the past-time temporal operators as well as some syntactic sugar):

  • [LTL SU LTL] | [LTL WU LTL] | X LTL | G LTL | F LTL
  • LTL ∧ LTL | LTL ∨ LTL | ¬LTL | VAR

Then, other people defined state-based logics like the µ-calculus and CTL, and they used Kripe structures and defined that a state formula holds on the structure iff it holds on all of its initial states.

After that, people tried to combine the two approaches, and then wanted the classic LTL formulas (the ones defined above) to hold on all the infinite paths that start in the initial states of the Kripke structure. To avoid a separate definition for being true on a structure, it makes sense to put a universal path quantifier in front of the classic LTL formulas $\varphi$ so that the state-based definition of being satisfied by a Kripke structure also holds for that kind of LTL (note that $A\varphi$ holds on all initial states iff $\varphi$ holds on all infinite paths starting in intial states).

So, the LTL embedded in CTL* is defined as the formulas $A\varphi$ where $\varphi$ is constructed by temporal and propositional operators only as shown above.

Second, CTL is the logic defined by pairs of operators where one is a path quantifier (A,E) and the other is a temporal operator. Thus, we have the following

  • A[CTL SU CTL] | A[CTL WU CTL] | AX CTL | AG CTL | AF CTL
  • E[CTL SU CTL] | E[CTL WU CTL] | EX CTL | EG CTL | EF CTL
  • CTL ∧ CTL | CTL ∨ CTL | ¬CTL | VAR

Formulas that are both CTL and LTL must therefore be of one of the forms

A[Prop SU Prop] | A[Prop WU Prop] | AX Prop | AG Prop | AF Prop

where Prop denotes a propositional logic formula. Note however that some formulas that do (syntactically) not belong to one of these logics can possibly be rewritten to an equivalent formula that belongs to a considered logic. Hence, we have to distinguish between "is the formula in one of the logics" and "is there an equivalent formula in that logic" which are two different questions.

Concerning E[(¬a) WW b], it is not LTL since it starts with an E-quantifier which is against the definition of LTL. Either we demand no path quantifiers (classic definition) or a leading A (but not an E).

  • LTL examples are A[x SU y], A(x ∨ G y), A[x SU (z ∨ G y)]
  • CTL examples are A[x SU y], AG(E[x SU y] ∨ AG z), E[(A[x SU y]) WU (x ∧ AG y)]
  • CTL* examples are E[(¬a) WU b] ∧ AFG x
bearbeiten Als beleidigend melden löschen publish Link mehr

Kommentare

So this is also a CTL - A(x ∨ G y), A[x SU (z ∨ G y)], right?

blackmamba ( 2017-08-17 16:47:12 +0100 )bearbeiten
2

No, none of them is a CTL formula: * in A(x ∨ G y), ∨ follows the A (not a temp. op.), and in front of G there is no path quant. * in A[x SU (z ∨ G y)], in front of G (a temporal operator), there is ∨ which is not a path quantifier. The pair A-SU is fine for CTL, however

PS ( 2017-08-17 16:54:38 +0100 )bearbeiten

So if I write AFGa, then this is CTL?

blackmamba ( 2017-08-17 17:07:25 +0100 )bearbeiten
2

No, AFGa is also not a CTL formula. AF is a CTL operator, but the G occurs without path quantifier. AF AG a or AF EG a or EF AG a would be CTL formulas. Path operators (A,E) must be coupled in pairs with temporal operators (SU, WU, X, G, F,...) in CTL so you cannot use one of them without the other.

PS ( 2017-08-17 17:11:09 +0100 )bearbeiten
1

Both formulas are of course in CTL*, but none of them is in CTL ∪ LTL. However, they are equivalent to CTL formulas: EFGa = EFEGa and E(Ga v [a U Xb]) = EGa v E[a U EXb]. You can check this with http://es.cs.uni-kl.de/tools/teaching/TemporalLogicProver.html

PS ( 2017-08-18 18:33:33 +0100 )bearbeiten

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-17 12:36:43 +0100

Gesehen: 120 mal

Letztes Update: Aug 17