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 characterize the complexity of its model-checking problem, 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). We also show how these results apply to model checking ATL-like temporal logics for games.

@inproceedings{concur2012-DLM,
  author =              {Da{~}Costa, Arnaud and Laroussinie, Fran{\c c}ois
                         and Markey, Nicolas},
  title =               {Quantified~{CTL}: Expressiveness and Model Checking},
  editor =              {Koutny, Maciej and Ulidowski, Irek},
  booktitle =           {{P}roceedings of the 23rd {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'12)},
  acronym =             {{CONCUR}'12},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7454},
  pages =               {177-192},
  year =                {2012},
  month =               sep,
  doi =                 {10.1007/978-3-642-32940-1_14},
  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
                         characterize the complexity of its model-checking
                         problem, 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). We also show how these
                         results apply to model checking ATL-like temporal
                         logics for games.},
}