The Complexity of Enriched Mu-Calculi

Piero A. Bonatti; Carsten Lutz; Aniello Murano; Moshe Y. Vardi

doi:10.2168/LMCS-4(3:11)2008

Piero A. Bonatti ; Carsten Lutz ; Aniello Murano ; Moshe Y. Vardi - The Complexity of Enriched Mu-Calculi

lmcs:993 - Logical Methods in Computer Science, September 22, 2008, Volume 4, Issue 3 - https://doi.org/10.2168/LMCS-4(3:11)2008

The Complexity of Enriched Mu-CalculiArticle

Authors: Piero A. Bonatti ; Carsten Lutz ; Aniello Murano ; Moshe Y. Vardi

The fully enriched μ-calculus is the extension of the propositional μ-calculus with inverse programs, graded modalities, and nominals. While satisfiability in several expressive fragments of the fully enriched μ-calculus is known to be decidable and ExpTime-complete, it has recently been proved that the full calculus is undecidable. In this paper, we study the fragments of the fully enriched μ-calculus that are obtained by dropping at least one of the additional constructs. We show that, in all fragments obtained in this way, satisfiability is decidable and ExpTime-complete. Thus, we identify a family of decidable logics that are maximal (and incomparable) in expressive power. Our results are obtained by introducing two new automata models, showing that their emptiness problems are ExpTime-complete, and then reducing satisfiability in the relevant logics to these problems. The automata models we introduce are two-way graded alternating parity automata over infinite trees (2GAPTs) and fully enriched automata (FEAs) over infinite forests. The former are a common generalization of two incomparable automata models from the literature. The latter extend alternating automata in a similar way as the fully enriched μ-calculus extends the standard μ-calculus.

https://doi.org/10.2168/LMCS-4(3:11)2008

Source: arXiv.org:0809.0360

Volume: Volume 4, Issue 3

Published on: September 22, 2008

Imported on: January 7, 2007

Keywords: Computer Science - Logic in Computer Science,Computer Science - Computation and Language,F.3.1,F.4.1

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

Funding:

Source : OpenAIRE Graph

MRI: Acquisition of CITI Terascale Cluster (CTC); Funder: National Science Foundation; Code: 0216467
Automata-Theoretic Approach to Design Verification; Funder: National Science Foundation; Code: 0311326

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

28 Documents citing this article

Bartosz Bednarczyk;Oskar Fiuk, Lecture notes in computer science, Presburger Büchi Tree Automata with Applications to Logics with Expressive Counting, pp. 295-308, 2022, 10.1007/978-3-031-15298-6_19.

Luisa D'Amore;Aniello Murano;Loredana Sorrentino;Rossella Arcucci;et al., 2020, Toward a multilevel scalable parallel Zielonka's algorithm for solving parity games, Concurrency and Computation Practice and Experience, 33, 4, 10.1002/cpe.6043.

Y. Limón;E. Bárcenas;E. Benítez-Guerrero;G. Molero Castillo;A. Velázquez-Mena, 2020, Mu-Calculus Satisfiability with Arithmetic Constraints, Programming and Computer Software, 46, 8, pp. 503-510, 10.1134/s0361768820080137.

Aniello Murano;Mimmo Parente;Sasha Rubin;Loredana Sorrentino, 2019, Model-checking graded computation-tree logic with finite path semantics, Theoretical Computer Science, 806, pp. 577-586, 10.1016/j.tcs.2019.09.021, https://doi.org/10.1016/j.tcs.2019.09.021.

Laura Bozzelli;Aniello Murano;Loredana Sorrentino, 2019, Alternating-time temporal logics with linear past, Theoretical Computer Science, 813, pp. 199-217, 10.1016/j.tcs.2019.11.028, https://doi.org/10.1016/j.tcs.2019.11.028.

Yensen Limon;Edgard Benitez-Guerrero;Everardo Barcenas;Guillermo Molero-Castillo;Alejandro Velazquez-Mena, 2019 7th International Conference in Software Engineering Research and Innovation (CONISOFT), A Satisfiability Algorithm For The Mu-Calculus For Trees With Presburger Constraints, 2, pp. 72-79, 2019, Mexico City, Mexico, 10.1109/conisoft.2019.00020.

Benjamin Aminof;Aniello Murano;Sasha Rubin, 2018, CTL* with graded path modalities, Information and Computation, 262, pp. 1-21, 10.1016/j.ic.2018.05.001, https://doi.org/10.1016/j.ic.2018.05.001.

Gaëlle Fontaine;Fabio Mogavero;Aniello Murano;Giuseppe Perelli;Loredana Sorrentino, 2018, Cycle detection in computation tree logic, Information and Computation, 262, pp. 265-279, 10.1016/j.ic.2018.09.007, https://doi.org/10.1016/j.ic.2018.09.007.

Vadim Malvone;Aniello Murano, Lecture notes in computer science, Reasoning About Additional Winning Strategies in Two-Player Games, pp. 163-171, 2018, 10.1007/978-3-030-01713-2_12.

Yensen Limon;Everardo Barcenas;Edgard Benitez-Guerrero;Maria Auxilio Medina, 2017 International Conference on Electronics, Communications and Computers (CONIELECOMP), Depth-first search satisfiability of the μ-calculus with converse over trees, pp. 1-7, 2017, Cholula, Mexico, 10.1109/conielecomp.2017.7891827.

Benjamin Aminof;Vadim Malvone;Aniello Murano;Sasha Rubin, 2016, Extended Graded Modalities in Strategy Logic, arXiv (Cornell University), 218, pp. 1-14, 10.4204/eptcs.218.1.

Everardo Barcenas;Guillermo Molero;Gabriela Sanchez;Edgard Benitez-Guerrero;Carmen Mezura-Godoy, 2016 International Conference on Electronics, Communications and Computers (CONIELECOMP), Reasoning on expressive description logics with arithmetic constraints, 2, pp. 180-185, 2016, Cholula, Mexico, 10.1109/conielecomp.2016.7438572.

Gaëlle Fontaine;Fabio Mogavero;Aniello Murano;Giuseppe Perelli;Loredana Sorrentino, 2016, Cycle Detection in Computation Tree Logic, arXiv (Cornell University), 226, pp. 164-177, 10.4204/eptcs.226.12.

Benjamin Aminof;Aniello Murano;Sasha Rubin, reposiTUm (TU Wien), On CTL* with Graded Path Modalities, pp. 281-296, 2015, 10.1007/978-3-662-48899-7_20, http://resolver.obvsg.at/urn:nbn:at:at-ubtuw:3-3808.

Cristina Feier;Thomas Eiter, Lecture notes in computer science, Reasoning with Forest Logic Programs Using Fully Enriched Automata, pp. 346-353, 2015, 10.1007/978-3-319-23264-5_29.

Everardo Bárcenas;Edgard Benítez-Guerrero;Jesús Lavalle, Lecture notes in computer science, On the Model Checking of the Graded $$\mu $$ -calculus on Trees, pp. 178-189, 2015, 10.1007/978-3-319-27060-9_14.

Franz Baader;Stefan Borgwardt;Marcel Lippmann, CiteSeer X (The Pennsylvania State University), Temporal Conjunctive Queries in Expressive Description Logics with Transitive Roles, pp. 21-33, 2015, 10.1007/978-3-319-26350-2_3, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.703.2446.

John C. McCabe-Dansted;Tim French;Sophie Pinchinat;Mark Reynolds, 2015, Expressiveness and succinctness of a logic of robustness, Journal of Applied Non-Classical Logics, 25, 3, pp. 193-228, 10.1080/11663081.2015.1050907.

Massimo Benerecetti;Fabio Mogavero;Aniello Murano, 2015, Reasoning About Substructures and Games, ACM Transactions on Computational Logic, 16, 3, pp. 1-51, 10.1145/2757286.

Benjamin Aminof;Swen Jacobs;Ayrat Khalimov;Sasha Rubin, arXiv (Cornell University), Parameterized Model Checking of Token-Passing Systems, pp. 262-281, 2014, 10.1007/978-3-642-54013-4_15, https://arxiv.org/abs/1311.4425.

Fabio Mogavero;Aniello Murano;Giuseppe Perelli;Moshe Y. Vardi, 2014, Reasoning About Strategies, DROPS (Schloss Dagstuhl – Leibniz Center for Informatics), 15, 4, pp. 1-47, 10.1145/2631917, https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010.133.

Fabio Mogavero;Aniello Murano;Moshe Y. Vardi, 2014, Relentful strategic reasoning in alternating-time temporal logic, CiteSeer X (The Pennsylvania State University), 26, 5, pp. 1663-1695, 10.1093/logcom/exu052, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.303.1795.

Benjamin Aminof;Fabio Mogavero;Aniello Murano, 2013, Synthesis of hierarchical systems, Science of Computer Programming, 83, pp. 56-79, 10.1016/j.scico.2013.07.001, https://doi.org/10.1016/j.scico.2013.07.001.

Massimo Benerecetti;Fabio Mogavero;Aniello Murano, CiteSeer X (The Pennsylvania State University), Substructure Temporal Logic, 2013, New Orleans, LA, USA, 10.1109/lics.2013.43, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.307.9528.

Alessandro Bianco;Fabio Mogavero;Aniello Murano, 2012, Graded computation tree logic, ACM Transactions on Computational Logic, 13, 3, pp. 1-53, 10.1145/2287718.2287725.

Benjamin Aminof;Axel Legay;Aniello Murano;Olivier Serre;Moshe Y. Vardi, 2012, Pushdown module checking with imperfect information, 223, pp. 1-17, 10.1016/j.ic.2012.11.005, https://hal.inria.fr/hal-01260664.

Giacomo Lenzi, 2011, On P-transitive graphs and applications, arXiv (Cornell University), 54, pp. 222-236, 10.4204/eptcs.54.16.

Alessandro Bianco;Fabio Mogavero;Aniello Murano, 2009 24th Annual IEEE Symposium on Logic In Computer Science, Graded Computation Tree Logic, 2009, Los Angeles, California, USA, 10.1109/lics.2009.28.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 1627 times.

This article's PDF has been downloaded 354 times.