Talk:Computational tree logic
From Wikipedia, the free encyclopedia
Contents |
[edit] 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"
[edit] 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)
[edit] move to CTL & state/path operators
[edit] 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)
[edit] 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)
[edit] 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)
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$
[edit] Software for constructing/modeling a tree?
Is there any software out there to make trees like this, at any level of implementation?
I'm interested in taking the wiki source code and extending it to be able to make trees like this, using the group editing model of wiki.
My intention is to model the known information surrounding some topic of controversy, so as to better relate it and visualize it (and even perform operations on it) versus a flat representation or outline-form like wikipedia. This could integrate multiple viewpoints and remove bias in information presentation.
Anyone who would wants to help with this please send me a comment!
-Aaron
