Nicolas Markey

Résumé

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

@article{lmcs10(4)-LM,
  author =              {Laroussinie, Fran{\c c}ois and Markey, Nicolas},
  title =               {Quantified~{CTL}: expressiveness and complexity},
  journal =             {Logical Methods in Computer Science},
  volume =              {10},
  number =              {4},
  year =                {2014},
  month =               dec,
  doi =                 {10.2168/LMCS-10(4:17)2014},
  abstract =            {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).},
}