Revision as of 09:43, 18 February 2020 edit Fschwarzentruber (talk \| contribs) 238 edits →Extensions Tag: Visual edit ← Previous edit		Revision as of 10:13, 18 February 2020 edit undo Fschwarzentruber (talk \| contribs) 238 edits →Extensions Tag: Visual edit Next edit →
Line 149: * 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 /> ~~<br />~~ ==See also== *[[Probabilistic CTL]]

Computation tree logic: Difference between revisions