Content deleted Content added
m →References: HTTP → HTTPS for Carnegie Mellon CS, replaced: http://www.cs.cmu.edu/ → https://www.cs.cmu.edu/ |
|||
Line 143:
*'''AG'''(P<math>\Rightarrow</math>(('''EX'''.Q)<math>\land</math>('''EX'''¬Q))) and '''AG.EF'''.P exist in CTL but not in LTL.
== Extensions ==
CTL has been extended with second order quantifier <math>\exists p</math> and <math>\forall p</math>. There are two semantics:
* the tree semantics. We label nodes of the computation tree. QCTL* = QCTL = MSO over trees. Model checking and satisfiability are tower-complete.
* the structure semantics. We label states. QCTL* = QCTL = MSO over graphs. Model checking is PSPACE-complete but satisfiability is undecidable.
<br />
==See also==
*[[Probabilistic CTL]]
| |||