Efficiently Deciding μ-Calculus with Converse over Finite Trees

DOI10.1145/2724712zbMath1354.68124OpenAlexW2131842699MaRDI QIDQ2957698

Nils Gesbert, Alan Schmitt, Nabil Layaïda, Pierre Genevès

Publication date: 27 January 2017

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/2724712

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Modal logic (including the logic of norms) (03B45) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Data structures (68P05)

Related Items

Backward type inference for XML queries

Uses Software

• XQuery
• CDuce
• PGSolver
• XPath

Cites Work

• Rewriting of regular expressions and regular path queries
• Results on the propositional \(\mu\)-calculus
• Reasoning about XML with temporal logics and automata
• Propositional dynamic logic of regular programs
• Automata, logics, and infinite games. A guide to current research
• XML Type Checking Using High-Level Tree Transducer
• PDL for ordered trees
• BDD-based decision procedures for the modal logic K ★
• Solving Parity Games in Practice
• Graph-Based Algorithms for Boolean Function Manipulation
• The Zipper
• CDuce
• Automated Reasoning with Analytic Tableaux and Related Methods
• Containment and equivalence for a fragment of XPath
• Reasoning about XML with Temporal Logics and Automata
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item