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

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

18 Documents citing this article

Bernd Finkbeiner, 2023, Logics and Algorithms for Hyperproperties, Figshare, 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;Giuseppe Perelli, 2023, Reasoning about Quality and Fuzziness of Strategic Behaviors, SPIRE - Sciences Po Institutional REpository, 24, 3, pp. 1-38, 10.1145/3582498, https://inria.hal.science/hal-04219131.

Alexander Bolotov, 2022, On the Expressive Power of the Normal Form for Branching-Time Temporal Logics, Electronic Proceedings in Theoretical Computer Science, 358, pp. 254-269, 10.4204/eptcs.358.19, https://doi.org/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, SPIRE - Sciences Po Institutional REpository, 24, 2, pp. 1-46, 10.1145/3569954, https://hal.science/hal-04056877.

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.

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.

Piribauer, Jakob;Baier, Christel;Bertrand, Nathalie;Sankur, Ocan, 2021, Quantified Linear Temporal Logic over Probabilistic Systems with an Application to Vacuity Checking, DROPS (Schloss Dagstuhl – Leibniz Center for Informatics), 10.4230/lipics.concur.2021.7, https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.7.

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, Information and Computation, 280, pp. 104642, 10.1016/j.ic.2020.104642.

Bartosz Bednarczyk;Stéphane Demri;Raul Fervari;Alessio Mansutti, 2020, Modal Logics with Composition on Finite Forests, pp. 167-180, 10.1145/3373718.3394787, https://hal.science/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, 2019, Why Propositional Quantification Makes Modal Logics on Trees Robustly Hard?, SPIRE - Sciences Po Institutional REpository, pp. 1-13, 10.1109/lics.2019.8785656.

Norine Coenen;Bernd Finkbeiner;Christopher Hahn;Jana Hofmann, 2019, The Hierarchy of Hyperlogics, arXiv (Cornell University), pp. 1-13, 10.1109/lics.2019.8785713, http://arxiv.org/abs/2005.05934.

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

Laura Bozzelli;Aniello Murano, 2017, On the Complexity of ATL and ATL* Module Checking, Electronic Proceedings in Theoretical Computer Science, 256, pp. 268-282, 10.4204/eptcs.256.19, https://doi.org/10.4204/eptcs.256.19.

Raphael Berthon;Bastien Maubert;Aniello Murano;Sasha Rubin;Moshe Y. Vardi, 2017, Strategy logic with imperfect information, arXiv (Cornell University), pp. 1-12, 10.1109/lics.2017.8005136, http://arxiv.org/abs/1805.12592.

François Laroussinie;Nicolas Markey;Arnaud Sangnier, 2015, ATLsc with partial observation, Electronic Proceedings in Theoretical Computer Science, 193, pp. 43-57, 10.4204/eptcs.193.4, https://doi.org/10.4204/eptcs.193.4.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 2270 times.

This article's PDF has been downloaded 1139 times.