Talk:Computation tree logic

Examples (again)

In the example it is not clear where to put the parentheses: is it EF(EG p => AF r) or is it (EF EG p) => AF r? Both are possible and I'm going to edit the section to match the first variant. This variant has the advantage that it truly is a formula according to the grammar given. The other is not as the implication formally needs parentheses. Xlae (talk) 16:39, 27 August 2014 (UTC)

Examples

Hi, I have a question about the examples. Are they supposed to be pure CTL, or CTL*? Because the last 2 are actually CTL* formulas. In order for them to be CTL, until operator needs to be path-quantified also.

Cheers,

-- Krle — Preceding unsigned comment added by 93.87.39.27 (talk) 12:35, 4 November 2012 (UTC)

You are right, I've just noticed it too. I'm going to edit the section and add a note that those two are CTL*. 62.245.100.121 (talk) 12:38, 10 January 2013 (UTC)

Reorder the Page?

As written currently, the page defines the syntax before giving the interpretation of the operators, which is awkward if you haven't seen CTL before. If there are no objections, I'll swap the two sections and touch up the text (if necessary).

-- Gilbert (sorry I don't have a wikipedia account) 23 June 2009

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"

CTL = 'Computation Tree Logic' not Computational Tree Logic!

You can look it up in the paper cited in the article (Clarke, E. M., Emerson, E. A., and Sistla, A. P. (1986). "Automatic verification of finite-state concurrent systems using temporal logic specifications". ACM Transactions on Programming Languages and Systems 8 (2): 244–26), but also in lots of other articles using CTL. In fact I came across this when I noticed someone using 'Computational Tree Logic' - I am a little suspicious that in fact Wikipedia itself is spreading this! Think about it: it is a logic that follows the tree of a computation - that's where the name comes from. It's a not a logic of 'Computational Tres' (as such a thing does not exist to the the best of my knowledge(, and it is also not a computational version of some 'tree logic'.

So is there a quick way to update Wikipedia so that this page is called 'Computation Tree Logic'? I will change it on the page myself.

Cweise (talk) 12:37, 9 September 2008 (UTC)

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

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)

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$

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

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 s_i on this path. And consider any path π' out of s_i π' is not necessarily a sub-path of π, but, since s_i 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 s_i. Thus, s_i 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 s_i on this path. Since we have AG.AF.p, π satisfies G.AF.p, so s_i satisfies AF.p, so the subpath π' of π beginning at s_i satisfies F.p. s_i 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).

Sorry this paragraph is plain wrong, GF p is fairness. "start state s satisfying GF.p" => no, GF p is true or false of infinite traces, not of states. — Preceding unsigned comment added by 81.64.148.250 (talk) 20:03, 29 January 2016 (UTC)

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)

There are A[$\phi$W$\psi$] == A[$\phi$U$\psi$] $\lor$ AG($\phi$) and E[$\phi$W$\psi$] == E[$\phi$U$\psi$] $\lor$ EG($\phi$) . Maybe they are not obvious for beginners, should they be put on the main page? 192.93.2.32 (talk) 13:24, 11 May 2010 (UTC)

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)

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. --Someguy137 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)

Lecture slides

The notation used in the slides linked is really bad. It's very unconventional. —Preceding unsigned comment added by 87.194.191.26 (talk) 01:21, 13 February 2009 (UTC)

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)

transformation of EFφ

• F is define as "F φ - Finally: φ eventually has to hold (somewhere on the subsequent path)."
  
• U is define as "φ U ψ - Until: φ has to hold until at some position ψ holds. This implies that ψ will be verified in the future."
  
• and it is said that : " Fφ == [trueU(φ)] "

but Fφ doesn't impose that φ have to be verified unlike [trueU(φ)] which implies that φ will be verified.

Where is the bug? does Fφ means that φ has to hold (not eventually)? —Preceding unsigned comment added by 152.77.200.242 (talk) 13:20, 6 July 2010 (UTC)

Ok, from your IP you are French, but i know the same problem from German, too. Eventually in English does not translate to "éventuel" (or "eventuell" in German), but more "enfin" (fr)/"schließlich" (de). So, "eventually φ" means that at some point φ will hold (although it's not important at which point exactly), which also is expressed by "trueUφ". But you're not alone with this, the same question was raised in some of the lectures I attended that involved temporal logics ;-) Thomas5388 (talk) 04:08, 26 November 2010 (UTC)

Examples (once more)

The AG(PUQ) example seems to be explained badly. PUQ must hold on every path forever. So one likes chocolate until it is warm outside, but once it is warm, and then becomes cold again, one still has to like chocolate until it is warm. The textual description does not make this at all clear. — Preceding unsigned comment added by 78.27.127.183 (talk) 09:13, 26 October 2020 (UTC)