Talk:Computation tree logic

Names?

Does anybody know the full name for CTL*?
And by the way, I'm not sure if the correct name is "Computational tree logic" or "Computation tree logic". I've seen both. Which is the (more) correct one?

--[[User:Gedeon|Ged (talk)]] 18:45, 20 Jul 2004 (UTC)

As far As I know CTL is the "Computation tree logic", while CTL* is commonly referred as "Full Computation tree logic" or "Full Branching time logic"

State & path operators

I just came up with the terms "state operators" and "path operators" myself. If there is another "official" name for those or someone find something better, please edit... --[[User:Gedeon|Ged (talk)]] 02:00, 21 Jul 2004 (UTC)

move to CTL & state/path operators

Move

It's easier to explain what CTL* is and then say CTL is the subset where every temporal operator must be preceeded by a path quantifier.

Should there be only one page describing CTL, LTL, CTL* (unsure about the name though)?
Should the article on CTL* parctically duplicate the definitions used here? (My answer: NO)

Ripper234

state/path operators

There are no state/path operators. There are temporal operators, temporal quantifiers (could be considered as operators also, I don't know), and state and path formulas. I corrected it in the article.

I Always forget to sign :((( Ripper234 17:06, 2 April 2006 (UTC)[reply]

This is CTL*

This description of CTL is wrong. Though the given examples are valid CTL-Formulas, the description doesn't distinct between CTL and CTL* -- Neatlittleeraser 13:12, 6 July 2006 (UTC)[reply]

I agree, the description of the syntax is a bit confusing. The main different between CTL and CTL* is that in CTL it is not possible to nest temporal operator using classical connectives.

What about something like :

$CTL^*$ is an extension of the language for propositional logic with temporal connectives. In particular we consider countably many propositional variables $AP$ and the connectives $\lnot, \land, A, E, X, {\cal U}$. The ``Before modality is defined as the dual of ``Until. The ``Generally modality and ``Sometimes modality are defined, respectively, as ${\cal G} \varphi := (\bot \; {\cal B} \; \varphi)$ and ${\cal F} \varphi := (\top \; {\cal U} \; \varphi)$ . Abbreviations $\lor$, $\rightarrow$, $\leftrightarrow$ are defined in the usual way.

The class of state formulae (formulae that are true or false when evaluated in a state) and the class of path formulae (true or false of paths) are defined as:

State Formulae:
- S1 each atomic proposition is a state formula
- S2 if $p,q$ are state formulae then so are $p \land q$ and $\lnot q$
- S3 if $p$ is a path formula then $E p$ and $A p$ are state formulae
Path Formulae:
- P1 each state formula is also a path formula
- P2 if $p,q$ are path formulae then so are $p \land q$ and $\lnot q$
- P3 if $p,q$ are path formulae then so are $X p$ and $p {\cal U} q$

The minimal set satisfying the rules S1-3 and P1-3 forms the language $CTL^*$. The syntax of the logic $CTL$ is obtained by restricting the syntax to disallow boolean combinations and nesting of linear time operators. Formally, the $CTL$ syntax is obtained by replacing P1-3 with

P0 if $p,q$ are path formulae the so are $X p$ and $p {\cal U} q$