Laroussinie, François and Markey, Nicolas - Quantified CTL: Expressiveness and Complexity

lmcs:1029 - Logical Methods in Computer Science, December 25, 2014, Volume 10, Issue 4
Quantified CTL: Expressiveness and Complexity

Authors: Laroussinie, François and Markey, Nicolas

While it was defined long ago, the extension of CTL with quantification over atomic propositions has never been studied extensively. Considering two different semantics (depending whether propositional quantification refers to the Kripke structure or to its unwinding tree), we study its expressiveness (showing in particular that QCTL coincides with Monadic Second-Order Logic for both semantics) and characterise the complexity of its model-checking and satisfiability problems, depending on the number of nested propositional quantifiers (showing that the structure semantics populates the polynomial hierarchy while the tree semantics populates the exponential hierarchy).


Source : oai:arXiv.org:1411.4332
DOI : 10.2168/LMCS-10(4:17)2014
Volume: Volume 10, Issue 4
Published on: December 25, 2014
Submitted on: April 5, 2013
Keywords: Computer Science - Logic in Computer Science


Share

Consultation statistics

This page has been seen 94 times.
This article's PDF has been downloaded 33 times.