eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2016-08-24
28:1
28:15
10.4230/LIPIcs.CONCUR.2016.28
article
On the Expressiveness of QCTL
David, Amélie
Laroussinie, Francois
Markey, Nicolas
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 QkCTL, 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 QkCTL collapses at level 2 (in other terms, any QCTL formula can be expressed using at most two nested blocks of quantifiers).
https://drops.dagstuhl.de/storage/00lipics/lipics-vol059-concur2016/LIPIcs.CONCUR.2016.28/LIPIcs.CONCUR.2016.28.pdf
Specification
Verification
Temporal Logic
Expressiveness
Tree automata