Editing Computation tree logic (section)

== Extensions ==
CTL has been extended with [[second-order logic|second-order]] quantification <math>\exists p</math> and <math>\forall p</math> to ''quantified computational tree logic'' (QCTL).<ref>{{Cite journal|last1=David|first1=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|doi-access=free |isbn=978-3-95977-017-0}}</ref> There are two semantics:

* the tree semantics. We label nodes of the computation tree. QCTL* = QCTL = [[monadic second-order logic|MSO]] over trees. Model checking and satisfiability are tower complete.
* the structure semantics. We label states. QCTL* = QCTL = MSO over [[Graph (discrete mathematics)|graph]]s. Model checking is [[PSPACE-complete]] but satisfiability is [[undecidable problem|undecidable]].

A reduction from the model-checking problem of QCTL with the structure semantics, to TQBF (true quantified Boolean formulae) has been proposed, in order to take advantage of the QBF solvers.<ref>{{Cite journal|last1=Hossain|first1=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|doi-access=free |isbn=978-3-95977-127-6|s2cid=195345645 }}</ref>