Revision as of 09:41, 18 February 2020 edit Fschwarzentruber (talk \| contribs) 238 edits →See also Tag: Visual edit ← Previous edit		Revision as of 09:43, 18 February 2020 edit undo Fschwarzentruber (talk \| contribs) 238 edits →Extensions Tag: Visual edit Next edit →
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: ~~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.

Computation tree logic: Difference between revisions