Efficiently deciding -calculus with converse over finite trees

DOI10.1145/2724712MaRDI QIDQ2957698zbMATH OpenOpenAlexFDO

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

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

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

Recommendations

• Mu-calculus satisfiability with arithmetic constraints
• Automated Reasoning with Analytic Tableaux and Related Methods
• Satisfiability and Finite Model Property for the Alternating-Time μ-Calculus
• On model checking for the \(\mu\)-calculus and its fragments
• scientific article; zbMATH DE number 1223729

Cites work

• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• scientific article; zbMATH DE number 1223729 (Why is no real title available?)
• scientific article; zbMATH DE number 1304332 (Why is no real title available?)
• scientific article; zbMATH DE number 1086671 (Why is no real title available?)
• scientific article; zbMATH DE number 2017841 (Why is no real title available?)
• scientific article; zbMATH DE number 2080055 (Why is no real title available?)
• scientific article; zbMATH DE number 2241908 (Why is no real title available?)
• A decision procedure for alternation-free modal \(\mu\)-calculi
• Automata, logics, and infinite games. A guide to current research
• Automated Reasoning with Analytic Tableaux and Related Methods
• BDD-based decision procedures for the modal logic K ★
• CDuce: an XML-centric general-purpose language
• Containment and equivalence for a fragment of XPath
• Graph-Based Algorithms for Boolean Function Manipulation
• PDL for ordered trees
• Propositional dynamic logic of regular programs
• Reasoning about XML with Temporal Logics and Automata
• Reasoning about XML with temporal logics and automata
• Results on the propositional \(\mu\)-calculus
• Rewriting of regular expressions and regular path queries
• Solving parity games in practice
• The Zipper
• XML Type Checking Using High-Level Tree Transducer

Cited in

(4)

• Mu-calculus satisfiability with arithmetic constraints
• The Nesting-Depth of Disjunctive μ-Calculus for Tree Languages and the Limitedness Problem
• Backward type inference for XML queries
• Automated Reasoning with Analytic Tableaux and Related Methods

Describes a project that uses

Uses Software

• XPath
• PGSolver
• CDuce
• XQuery

This page was built for publication: Efficiently deciding \(\mu\)-calculus with converse over finite trees

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2957698)