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

lmcs:1029 - Logical Methods in Computer Science, December 25, 2014, Volume 10, Issue 4 - https://doi.org/10.2168/LMCS-10(4:17)2014
Quantified CTL: Expressiveness and ComplexityArticle

Authors: François Laroussinie ; Nicolas Markey ORCID

    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).


    Volume: Volume 10, Issue 4
    Published on: December 25, 2014
    Imported on: April 5, 2013
    Keywords: Computer Science - Logic in Computer Science
    Funding:
      Source : OpenAIRE Graph
    • EQualIS : Enhancing the Quality of Interacting Systems; Funder: European Commission; Code: 308087

    19 Documents citing this article

    Consultation statistics

    This page has been seen 1228 times.
    This article's PDF has been downloaded 391 times.