D | |
---|---|
[DLM12] | Arnaud Da Costa,
François Laroussinie et
Nicolas Markey.
Quantified CTL: Expressiveness and Model Checking.
In CONCUR'12,
Lecture Notes in Computer Science 7454, pages 177-192. Springer-Verlag, septembre 2012.
@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.}, } |
- 1
- 1
- 1