Computation tree logic: Difference between revisions

Revision as of 17:10, 15 April 2020

Revision as of 17:56, 18 April 2020

Line 144:

== Extensions ==

CTL has been extended with second order quantifier <math>\exists p</math> and <math>\forall p</math>.<ref>{{Cite journal|last=David|first=Amélie|last2=Laroussinie|first2=Francois|last3=Markey|first3=Nicolas|date=2016|editor-last=Desharnais|editor-first=Josée|editor2-last=Jagadeesan|editor2-first=Radha|title=On the Expressiveness of QCTL|url=http://drops.dagstuhl.de/opus/volltexte/2016/6164|journal=27th International Conference on Concurrency Theory (CONCUR 2016)|series=Leibniz International Proceedings in Informatics (LIPIcs)|___location=Dagstuhl, Germany|publisher=Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik|volume=59|pages=28:1–28:15|doi=10.4230/LIPIcs.CONCUR.2016.28|isbn=978-3-95977-017-0}}</ref>. 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.

A reduction from the model checking problem of QCTL with the structure semantics, to TQBF (true quantified binary formulae) has been proposed, in order to take advantage of the QBF solvers.<ref>{{Cite journal|last=Hossain|first=Akash|last2=Laroussinie|first2=François|date=2019|editor-last=Gamper|editor-first=Johann|editor2-last=Pinchinat|editor2-first=Sophie|editor3-last=Sciavicco|editor3-first=Guido|title=From Quantified CTL to QBF|url=http://drops.dagstuhl.de/opus/volltexte/2019/11369|journal=26th International Symposium on Temporal Representation and Reasoning (TIME 2019)|series=Leibniz International Proceedings in Informatics (LIPIcs)|___location=Dagstuhl, Germany|publisher=Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik|volume=147|pages=11:1–11:20|doi=10.4230/LIPIcs.TIME.2019.11|isbn=978-3-95977-127-6}}</ref>.<br />

==See also==

*[[Probabilistic CTL]]

Line 156 ⟶ 157:

==References==

{{Reflist}}

* {{cite journal |author1=E.M. Clarke |author2=E.A. Emerson | title=Design and synthesis of synchronisation skeletons using branching time temporal logic| journal=Logic of Programs, Proceedings of Workshop, Lecture Notes in Computer Science, Vol. 131 | publisher= Springer, Berlin | year=1981 |pages= 52–71|url=https://www.cs.cmu.edu/afs/cs/user/emc/www/papers/Invited%20Conference%20Articles/Design%20and%20Synthesis%20of%20Synchronization%20Skeletons%20Using%20Branching%20Time%20Temporal%20Logic.pdf}}

* {{cite book |author1=Michael Huth |author2=Mark Ryan | title=Logic in Computer Science (Second Edition) | year=2004| page=207 | publisher=Cambridge University Press | isbn=978-0-521-54310-1}}