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)

Ripper234

[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

[edit] GF.p and CTL

GF.p is expressible in CTL. It's equivalent to AG.AF.p.

Here's a proof: Assume a model M and start state s satisfying GF.p Then take any computation path π out of s. Consider any state si on this path. And consider any path π' out of si π' is not necessarily a sub-path of π, but, since si is by construction reachable from s, π' is a sub-path of some path out of s. Since GF.p holds for all paths out of s, we have F.p holds for the sub-path π'. Thus we have F.p holds for any path out of si. Thus, si satisfies AF.p Thus we have AF.p for any state on path π. Thus. π satisfies G.AF.p. Thus we have G.AF.p for all paths out of s. Thus, s satisfies AG.AF.p.

So GF.p→AG.AF.p

Next assume a model M and start state s satisfying AG.AF.p. Take any path π out of s. Consider any state si on this path. Since we have AG.AF.p, π satisfies G.AF.p, so si satisfies AF.p, so the subpath π' of π beginning at si satisfies F.p. si was arbitrary, so all subpaths of π satisfy F.p. So π satisfies GF.p π was arbitrary, so s satisfies GF.p.

So AG.AF.p→GF.p

So they're equivalent. GF.p is expressible in CTL.


I've changed it to FG.p. This actually isn't expressible in CTL.

Now, I think the original erroneous example was a mis-copy of an example in Huth and Ryan. The example Huth and Ryan actually uses is GF.p→GF.q. Since I think this is what the original editor intended, perhaps this should be used in place of FG.p. I don't think it really matters.

On the subject of Huth and Ryan though, if you're using it as reference, the examples seem to imply that FG.p is expressible as AF.AG.p, but this is not true. Consider the system of three states, with transitions

1→1, 1→2, 2→3, 3→3

where p is true in states 1 and 3, but not in state 2. I assume 1 as start state.

On all paths, there is some state after which p is always true, so FG.p holds. However, there is a path, specifically 1→1→1→1→1→…, on which no state satisfies AG.p (even though this path does satisfy G.p) since at state 1 we always have the possible path 1→2→3→3→…, which does not satisfy G.p. Thus the model does not satisfy AF.AG.p. Huth and Ryan's examples for FG.p and AF.AG.p seem equivalent because it uses deadlock as p, and deadlock states tend to always satisfy AG.deadlock. —The preceding unsigned comment was added by 18.243.5.80 (talk) 08:42, 2 May 2007 (UTC).

[edit] No derivation for weak until

There is no derivation of the weak until operators from the minimal set of operators. --Marco Bakera 05:48, 3 May 2007 (UTC)

[edit] Inconsistent use of N/X

The "state operators" definition says

N φ - Next: φ has to hold at the next state (this operator is sometimes noted X instead of N).

But below, only X is used. I'll exchange N and X in the definition (less work ;)). If anyone objects, just change every X to N below.

132.231.54.1 16:20, 3 May 2007 (UTC)

[edit] Notation

I've changed the article to using \Rightarrow over \rightarrow for logical implication to distinguish this from the notation used to represent the state transition function. This could equally be the other way round, so long as they're distinct, but it appears standard in the literature to use them this way. --Rallfo 10:22, 4 June 2007 (UTC)

Somebody has turned it back at the definition (but not in the rest of the article), so I fixed it again to at least be consistent. However, I think this article should use \rightarrow, since this is the notation used in all other logic articles (LTL etc.). Logical \rightarrow is syntax, and state transition is at the meta level, so I don't think they will be confused. 220.157.232.180 (talk) 00:14, 24 March 2008 (UTC)

[edit] Merge from CTL*

Currently there isn't anything useful at CTL* - I suggest turning it into a redirect. Ripper234 (talk) 23:35, 13 December 2007 (UTC)