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

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