Quantified CTL: Expressiveness and Complexity

François Laroussinie; Nicolas Markey

doi:10.2168/LMCS-10(4:17)2014

François Laroussinie ; Nicolas Markey - Quantified CTL: Expressiveness and Complexity

lmcs:1029 - Logical Methods in Computer Science, December 25, 2014, Volume 10, Issue 4 - https://doi.org/10.2168/LMCS-10(4:17)2014

Quantified CTL: Expressiveness and ComplexityArticle

Authors: François Laroussinie ; Nicolas Markey

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

https://doi.org/10.2168/LMCS-10(4:17)2014

Source: arXiv.org:1411.4332

Volume: Volume 10, Issue 4

Published on: December 25, 2014

Imported on: April 5, 2013

Keywords: Computer Science - Logic in Computer Science

Licence: arXiv.org - Non-exclusive license to distribute

Funding:

Source : OpenAIRE Graph

EQualIS : Enhancing the Quality of Interacting Systems; Funder: European Commission; Code: 308087

Bibliographic References

19 Documents citing this article

Bernd Finkbeiner, 2023, Logics and Algorithms for Hyperproperties, INDIGO (University of Illinois at Chicago), 10, 2, pp. 4-23, 10.1145/3610392.3610394, https://figshare.com/articles/journal_contribution/Logics_and_Algorithms_for_Hyperproperties/24612636.

Patricia Bouyer;Orna Kupferman;Nicolas Markey;Bastien Maubert;Aniello Murano;et al., 2023, Reasoning about Quality and Fuzziness of Strategic Behaviors, ACM Transactions on Computational Logic, 24, 3, pp. 1-38, 10.1145/3582498, https://doi.org/10.1145/3582498.

Alexander Bolotov, 2022, On the Expressive Power of the Normal Form for Branching-Time Temporal Logics, arXiv (Cornell University), 358, pp. 254-269, 10.4204/eptcs.358.19.

Bartosz Bednarczyk;Stéphane Demri, 2022, Why Does Propositional Quantification Make Modal and Temporal Logics on Trees Robustly Hard?, Logical Methods in Computer Science, Volume 18, Issue 3, 10.46298/lmcs-18(3:5)2022, https://doi.org/10.46298/lmcs-18(3:5)2022.

Bartosz Bednarczyk;Stéphane Demri;Raul Fervari;Alessio Mansutti, 2022, On Composing Finite Forests with Modal Logics, ACM Transactions on Computational Logic, 24, 2, pp. 1-46, 10.1145/3569954.

Dylan Bellier;Massimo Benerecetti;Dario Della Monica;Fabio Mogavero, 2022, Good-for-Game QPTL: An Alternating Hodges Semantics, ACM Transactions on Computational Logic, 24, 1, pp. 1-57, 10.1145/3565365, https://doi.org/10.1145/3565365.

Jakob Piribauer;Christel Baier;Nathalie Bertrand;Ocan Sankur, Quantified Linear Temporal Logic over Probabilistic Systems with an Application to Vacuity Checking, 2021, 10.4230/lipics.concur.2021.7, https://hal.science/hal-03408379.

Liping Xiong;Sumei Guo, 2021, Representation and Reasoning about Strategic Abilities with ω-Regular Properties, Mathematics, 9, 23, pp. 3052, 10.3390/math9233052, https://doi.org/10.3390/math9233052.

Raphaël Berthon;Bastien Maubert;Aniello Murano;Sasha Rubin;Moshe Y. Vardi, 2021, Strategy Logic with Imperfect Information, ACM Transactions on Computational Logic, 22, 1, pp. 1-51, 10.1145/3427955, https://doi.org/10.1145/3427955.

Akash Hossain;François Laroussinie, 2020, QCTL model-checking with QBF solvers, arXiv (Cornell University), 280, pp. 104642, 10.1016/j.ic.2020.104642, https://arxiv.org/abs/2010.03185.

Alessio Mansutti, Lecture notes in computer science, An Auxiliary Logic on Trees: on the Tower-Hardness of Logics Featuring Reachability and Submodel Reasoning, pp. 462-481, 2020, 10.1007/978-3-030-45231-5_24, https://doi.org/10.1007/978-3-030-45231-5_24.

Bartosz Bednarczyk;Stéphane Demri;Raul Fervari;Alessio Mansutti, Modal Logics with Composition on Finite Forests, 2020, Saarbrücken Germany, 10.1145/3373718.3394787, https://hal.archives-ouvertes.fr/hal-03005865.

Francesco Belardinelli;Alessio Lomuscio;Aniello Murano;Sasha Rubin, 2020, Verification of multi-agent systems with public actions against strategy logic, Spiral (Imperial College London), 285, pp. 103302, 10.1016/j.artint.2020.103302, http://hdl.handle.net/10044/1/78963.

Bartosz Bednarczyk;Stephane Demri, Why Propositional Quantification Makes Modal Logics on Trees Robustly Hard?, 41, pp. 1-13, 2019, Vancouver, BC, Canada, 10.1109/lics.2019.8785656, https://hal.archives-ouvertes.fr/hal-02350328.

Norine Coenen;Bernd Finkbeiner;Christopher Hahn;Jana Hofmann, arXiv (Cornell University), The Hierarchy of Hyperlogics, 2019, Vancouver, BC, Canada, 10.1109/lics.2019.8785713, https://arxiv.org/abs/2005.05934.

S. Akshay;Paul Gastin;Vincent Juge;Shankara Narayanan Krishna, Timed Systems through the Lens of Logic, abs 1904 6942, pp. 1-13, 2019, Vancouver, BC, Canada, 10.1109/lics.2019.8785684, https://hal.science/hal-03185736.

Laura Bozzelli;Aniello Murano, 2017, On the Complexity of ATL and ATL* Module Checking, arXiv (Cornell University), 256, pp. 268-282, 10.4204/eptcs.256.19.

Raphaël Berthon;Bastien Maubert;Aniello Murano;Sasha Rubin;Moshe Vardi, arXiv (Cornell University), Strategy logic with imperfect information, 2017, Reykjavik, Iceland, 10.1109/lics.2017.8005136, https://arxiv.org/abs/1805.12592.

François Laroussinie;Nicolas Markey;Arnaud Sangnier, 2015, ATLsc with partial observation, arXiv (Cornell University), 193, pp. 43-57, 10.4204/eptcs.193.4.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 1584 times.

This article's PDF has been downloaded 430 times.