research-article

Efficiently Deciding μ-Calculus with Converse over Finite Trees

Authors:

Pierre Genevès,

Nabil Layaïda,

Nils GesbertAuthors Info & Claims

ACM Transactions on Computational Logic (TOCL), Volume 16, Issue 2

Article No.: 16, Pages 1 - 41

https://doi.org/10.1145/2724712

Published: 02 April 2015 Publication History

Abstract

We present a sound and complete satisfiability-testing algorithm and its effective implementation for an alternation-free modal μ-calculus with converse, where formulas are cycle-free and are interpreted over finite ordered trees. The time complexity of the satisfiability-testing algorithm is 2^O(n) in terms of formula size n. The algorithm is implemented using symbolic techniques (BDD). We present crucial implementation techniques and heuristics that we used to make the algorithm as fast as possible in practice. Our implementation is available online and can be used to solve logical formulas of significant size and practical value. We illustrate this in the setting of XML trees.

References

[1]

Loredana Afanasiev, Patrick Blackburn, Ioanna Dimitriou, Bertrand Gaiffe, Evan Goris, Maarten Marx, and Maarten de Rijke. 2005. PDL for ordered trees. Journal of Applied Non-Classical Logics 15, 2 (2005), 115--135.

[2]

Everardo Bárcenas, Pierre Genevès, and Nabil Layaïda. 2009. On the analysis of queries with counting constraints. In Proceedings of the 9th ACM Symposium on Document Engineering (DocEng’09). ACM, New York, NY, 21--24.

Digital Library

[3]

Everardo Barcenas, Pierre Genevès, Nabil Layaïda, and Alan Schmitt. 2011. Query reasoning on trees with types, interleaving and counting. In Proceedings of the 22nd International Joint Conference on Artificial Intelligence (IJCAI’11). 718--723.

Digital Library

[4]

Véronique Benzaken, Giuseppe Castagna, and Alain Frisch. 2003. CDuce: An XML-centric general-purpose language. In Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming (ICFP’03). ACM Press, New York, NY, 51--63.

Digital Library

[5]

Scott Boag, Don Chamberlin, Mary F. Fernández, Daniela Florescu, Jonathan Robie, and Jérôme Siméon. 2007. XQuery 1.0: An XML Query Language, W3C Recommendation. (January 2007).

[6]

Randal E. Bryant. 1986. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers 35, 8 (1986), 677--691.

Digital Library

[7]

Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, and Moshe Y. Vardi. 2008. Regular XPath: Constraints, query containment and view-based answering for XML documents. In Proceedings of the 2008 International Workshop on Logic in Databases (LID’08).

[8]

Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, and Moshe Y. Vardi. 2009. An automata-theoretic approach to regular XPath. In Proceedings of the 12th International Symposium on Database Programming Languages (DBPL’09) (Lecture Notes in Computer Science), Vol. 5708. Springer, 18--35.

Digital Library

[9]

Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, and Moshe Y. Vardi. 2010. Node selection query languages for trees. In AAAI, Maria Fox and David Poole (Eds.). AAAI Press.

[10]

James Clark and Steve DeRose. 1999. XML Path Language (XPath) Version 1.0, W3C Recommendation. Retrieved from http://www.w3.org/TR/1999/REC-xpath-19991116.

[11]

Edmund M. Clarke and E. Allen Emerson. 1981. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Logic of Programs, Workshop (LNCS), Vol. 131. Springer-Verlag, London, UK, 52--71.

Digital Library

[12]

Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. 1999. Model checking. MIT Press, Cambridge, MA.

Digital Library

[13]

M. J. Fischer and R. E. Ladner. 1979. Propositional dynamic logic of regular programs. JCSS 18, 2 (1979), 194--211.

[14]

Oliver Friedmann and Martin Lange. 2009. The PGSolver collection of parity game solvers. Retrieved from http://www2.tcs.ifi.lmu.de/pgsolver/.

[15]

Oliver Friedmann and Martin Lange. 2010. A solver for modal fixpoint logics. Electronic Notes in Theoretical Computer Science 262 (May 2010), 99--111.

Digital Library

[16]

Pierre Genevès, Nils Gesbert, Nabil Layaïda, and Alan Schmitt. 2014. A Satisfiability Solver for XML and XPath. Retrieved http://wam.inrialpes.fr/websolver.

[17]

Pierre Genevès and Nabil Layaïda. 2006. A system for the static analysis of XPath. ACM Transactions in Information Systems 24, 4 (2006), 475--502.

Digital Library

[18]

Pierre Genevès, Nabil Layaïda, and Alan Schmitt. 2007. Efficient static analysis of XML paths and types. In Proceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’07). ACM, New York, NY, 342--351.

Digital Library

[19]

Erich Grädel, Wolfgang Thomas, and Thomas Wilke. 2002. Automata logics, and infinite games: a guide to current research. Springer-Verlag, New York, NY.

[20]

Ramin Hojati, Sriram C. Krishnan, and Robert K. Brayton. 1996. Early quantification and partitioned transition relations. In Proceedings of the 1996 International Conference on Computer Design, VLSI in Computers and Processors (ICCD’96). IEEE Computer Society, Washington, DC, 12--19.

Digital Library

[21]

Haruo Hosoya, Jérôme Vouillon, and Benjamin C. Pierce. 2005. Regular expression types for XML. ACM Transactions in Programming Language Systems 27, 1 (2005), 46--90.

Digital Library

[22]

Gérard P. Huet. 1997. The zipper. Journal of Functional Programming 7, 5 (1997), 549--554.

Digital Library

[23]

Dexter Kozen. 1983. Results on the propositional μ-calculus. Theoretical Computer Science 27 (1983), 333--354.

[24]

Dexter Kozen. 1997. Kleene algebra with tests. ACM Transactions on Programming Languages and Systems (TOPLAS) 19 (May 1997), 427--443. Issue 3.

Digital Library

[25]

O. Kupferman and M. Y. Vardi. 1999. The weakness of self-complementation. In Proceedings of the 16th Symposium on Theoretical Aspects of Computer Science (LNCS), Vol. 1563. Springer, London, UK, 455--466.

Digital Library

[26]

Martin Lange. 2005. Weak automata for the linear time μ-calculus. In Verification, Model Checking, and Abstract Interpretation, Radhia Cousot (Ed.). Lecture Notes in Computer Science, Vol. 3385. Springer Berlin, 267--281.

Digital Library

[27]

Leonid Libkin and Cristina Sirangelo. 2008. Reasoning about XML with temporal logics and automata. In Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR’08). Springer-Verlag, Berlin, 97--112.

Digital Library

[28]

Leonid Libkin and Cristina Sirangelo. 2010. Reasoning about XML with temporal logics and automata. Journal of Applied Logic 8, 2 (2010), 210--232.

[29]

Radu Mateescu. 2002. Local model-checking of modal μ-calculus on acyclic labeled transition systems. In Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’02). Springer-Verlag, London, UK, 281--295.

Digital Library

[30]

Gerome Miklau and Dan Suciu. 2004. Containment and equivalence for a fragment of XPath. Journal of the ACM 51, 1 (2004), 2--45.

Digital Library

[31]

Makoto Murata, Dongwon Lee, Murali Mani, and Kohsuke Kawaguchi. 2005. Taxonomy of XML schema languages using formal language theory. ACM Transactions on Internet Technology 5, 4 (2005), 660--704.

Digital Library

[32]

Dan Olteanu, Holger Meuss, Tim Furche, and Francois Bry. 2002. XPath: Looking forward. In Proceedings of the Workshop on XML-Based Data Management (EDBT’02) (LNCS), Vol. 2490. Springer-Verlag, London, UK, 109--127. citeseer.ist.psu.edu/olteanu02xpath.html.

Digital Library

[33]

Guoqiang Pan, Ulrike Sattler, and Moshe Y. Vardi. 2006. BDD-based decision procedures for the modal logic K. Journal of Applied Non-classical Logics 16, 1--2 (2006), 169--208.

[34]

V. R. Pratt. 1981. A decidable mu-calculus: Preliminary report. In Proceedings 22nd Annual Symposium on Foundations of Computer Science (SFCS’81). 421--427.

Digital Library

[35]

S. Safra. 1988. On the complexity of omega -automata. In Proceedings of the 29th Annual Symposium on Foundations of Computer Science. IEEE Computer Society, Washington, DC, 319--327.

Digital Library

[36]

Yoshinori Tanabe, Koichi Takahashi, and Masami Hagiya. 2008. A decision procedure for alternation-free modal μ-calculi. In Advances in Modal Logic. 341--362.

[37]

Yoshinori Tanabe, Koichi Takahashi, Mitsuharu Yamamoto, Akihiko Tozawa, and Masami Hagiya. 2005. A decision procedure for the alternation-free two-way modal μ-calculus. In TABLEAUX 2005 (LNCS), Vol. 3702. Springer-Verlag, London, UK, 277--291.

Digital Library

[38]

Akihiko Tozawa. 2004. On binary tree logic for XML and its satisfiability test. In Proceedings of the 6th JSSST Workshop on Programming and Programming Languages (PPL’04).

[39]

Moshe Y. Vardi. 1998. Reasoning about the past with two-way automata. In Proceedings of the 25th International Colloquium on Automata, Languages and Programming (ICALP’98). Springer-Verlag, London, UK, 628--641.

Digital Library

[40]

Jakob Voss. 2007. Wikipedia DTD. Retrieved from http://meta.wikimedia.org/wiki/Wikipedia_DTD.

[41]

Karen Zee, Viktor Kuncak, and Martin C. Rinard. 2008. Full functional verification of linked data structures. In PLDI, Rajiv Gupta and Saman P. Amarasinghe (Eds.). ACM, 349--361.

Digital Library

Cited By

Chlyah SGesbert NGenevès PLayaïda N(2025)Efficient iterative programs with distributed data collectionsJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2025.101047144(101047)Online publication date: Mar-2025
https://doi.org/10.1016/j.jlamp.2025.101047
Im HGenevès PGesbert NLayaïda N(2020)Backward type inference for XML queriesTheoretical Computer Science10.1016/j.tcs.2020.03.020823(69-99)Online publication date: Jul-2020
https://doi.org/10.1016/j.tcs.2020.03.020
Hague MLin AHong C(2019)CSS Minification via Constraint SolvingACM Transactions on Programming Languages and Systems10.1145/331033741:2(1-76)Online publication date: 19-Jun-2019
https://dl.acm.org/doi/10.1145/3310337
Show More Cited By

Index Terms

Efficiently Deciding μ-Calculus with Converse over Finite Trees

Recommendations

Alternation-Free Weighted Mu-Calculus

In this paper we introduce WMC, a weighted version of the alternation-free modal mu-calculus for weighted transition systems. WMC subsumes previously studied weighted extensions of CTL and resembles previously proposed time-extended versions of the ...
Adding the modal mu-calculus to the instruction-set process calculus
Two Is Enough – Bisequent Calculus for S5
Frontiers of Combining Systems
Abstract
We present a generalised sequent calculus based on the use of pairs of ordinary sequents called bisequents. It may be treated as the weakest kind of system in the rich family of systems operating on items being some collections of ordinary ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Computational Logic

ACM Transactions on Computational Logic Volume 16, Issue 2

March 2015

260 pages

ISSN:1529-3785

EISSN:1557-945X

DOI:10.1145/2737801

Editor:
Dale Miller
INRIA Saclay, France

Issue’s Table of Contents

Copyright © 2015 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 02 April 2015

Accepted: 01 January 2015

Revised: 01 January 2015

Received: 01 November 2011

Published in TOCL Volume 16, Issue 2

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

11
Total Citations
View Citations
150
Total Downloads

Downloads (Last 12 months)6
Downloads (Last 6 weeks)1

Reflects downloads up to 07 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Chlyah SGesbert NGenevès PLayaïda N(2025)Efficient iterative programs with distributed data collectionsJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2025.101047144(101047)Online publication date: Mar-2025
https://doi.org/10.1016/j.jlamp.2025.101047
Im HGenevès PGesbert NLayaïda N(2020)Backward type inference for XML queriesTheoretical Computer Science10.1016/j.tcs.2020.03.020823(69-99)Online publication date: Jul-2020
https://doi.org/10.1016/j.tcs.2020.03.020
Hague MLin AHong C(2019)CSS Minification via Constraint SolvingACM Transactions on Programming Languages and Systems10.1145/331033741:2(1-76)Online publication date: 19-Jun-2019
https://dl.acm.org/doi/10.1145/3310337
Baelde DLick ASchmitz SSuciu DSkritek SKoch C(2019)Decidable XPath Fragments in the Real WorldProceedings of the 38th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems10.1145/3294052.3319685(285-302)Online publication date: 25-Jun-2019
https://dl.acm.org/doi/10.1145/3294052.3319685
Limon YBarcenas EBenitez-Guerrero EMedina M(2017)Depth-first search satisfiability of the μ-calculus with converse over trees2017 International Conference on Electronics, Communications and Computers (CONIELECOMP)10.1109/CONIELECOMP.2017.7891827(1-7)Online publication date: 2017
https://doi.org/10.1109/CONIELECOMP.2017.7891827
Bosch MGenevès PLayaïda N(2015)Reasoning with styleProceedings of the 24th International Conference on Artificial Intelligence10.5555/2832415.2832558(2227-2233)Online publication date: 25-Jul-2015
https://dl.acm.org/doi/10.5555/2832415.2832558
Genevès PSchmitt A(2015)Expressive logical combinators for freeProceedings of the 24th International Conference on Artificial Intelligence10.5555/2832249.2832292(311-317)Online publication date: 25-Jul-2015
https://dl.acm.org/doi/10.5555/2832249.2832292
Genevès PGesbert N(2015)XQuery and static typing: tackling the problem of backward axesACM SIGPLAN Notices10.1145/2858949.278474650:9(88-100)Online publication date: 29-Aug-2015
https://dl.acm.org/doi/10.1145/2858949.2784746
Gesbert NGenevès PLayaïda N(2015)A Logical Approach to Deciding Semantic SubtypingACM Transactions on Programming Languages and Systems10.1145/281280538:1(1-31)Online publication date: 16-Oct-2015
https://dl.acm.org/doi/10.1145/2812805
Genevès PGesbert NFisher KReppy J(2015)XQuery and static typing: tackling the problem of backward axesProceedings of the 20th ACM SIGPLAN International Conference on Functional Programming10.1145/2784731.2784746(88-100)Online publication date: 29-Aug-2015
https://dl.acm.org/doi/10.1145/2784731.2784746
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents