Revision as of 20:49, 21 December 2020 edit Tom.Reding (talk \| contribs) Autopatrolled, Extended confirmed users, Page movers, Template editors 4,364,437 edits m Enum 1 author/editor WL; WP:GenFixes on Tag: AWB ← Previous edit		Revision as of 08:11, 19 January 2021 edit undo Narky Blert (talk \| contribs) Autopatrolled, Extended confirmed users, Page movers 419,248 edits Link to DAB page repaired Next edit →
Line 149: * 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~~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\|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>

Computation tree logic: Difference between revisions