D | |
---|---|

[DLM16] | Amélie David,
François Laroussinie et
Nicolas Markey.
On the expressiveness of QCTL.
In CONCUR'16,
Leibniz International Proceedings in Informatics 59, pages 28:1-28:15. Leibniz-Zentrum für Informatik, août 2016.
- Résumé
QCTL extends the temporal logic CTL with quantification over atomic propositions. While the algorithmic questions for QCTL and its fragments with limited quantification depth are well-understood (e.g. satisfiability of QCTLk, with at most k nested blocks of quantifiers, is k+1-EXPTIME-complete), very few results are known about the expressiveness of this logic. We address such expressiveness questions in this paper. We first consider the *distinguishing power*of these logics (i.e., their ability to separate models), their relationship with behavioural equivalences, and their ability to capture the behaviours of finite Kripke structures with so-called characteristic formulas. We then consider their*expressive power*(i.e., their ability to express a property), showing that in terms of expressiveness the hierarchy QCTLk collapses at level 2 (in other terms, any QCTL formula can be expressed using at most two nested blocks of quantifiers).
@inproceedings{concur2016-DLM, author = {David, Am{\'e}lie and Laroussinie, Fran{\c c}ois and Markey, Nicolas}, title = {On~the expressiveness of~{QCTL}}, editor = {Desharnais, Jules and Jagadeesan, Radha}, booktitle = {{P}roceedings of the 27th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'16)}, acronym = {{CONCUR}'16}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, series = {Leibniz International Proceedings in Informatics}, volume = {59}, pages = {28:1-28:15}, year = {2016}, month = aug, doi = {10.4230/LIPIcs.CONCUR.2016.28}, abstract = {QCTL extends the temporal logic CTL with quantification over atomic propositions. While the algorithmic questions for QCTL and its fragments with limited quantification depth are well-understood (e.g. satisfiability of QCTL\textsuperscript{\(k\)}, with at most \(k\) nested blocks of quantifiers, is \(k+1\)-EXPTIME-complete), very few results are known about the expressiveness of this logic. We~address such expressiveness questions in this paper. We first consider the \emph{distinguishing power} of these logics (i.e.,~their ability to separate models), their relationship with behavioural equivalences, and their ability to capture the behaviours of finite Kripke structures with so-called characteristic formulas. We then consider their \emph{expressive power} (i.e.,~their ability to express a property), showing that in terms of expressiveness the hierarchy QCTL\textsuperscript{\(k\)} collapses at level~2 (in~other terms, any~QCTL formula can be expressed using at most two nested blocks of quantifiers).}, } |

- 1
- 1
- 1