Efficiently deciding -calculus with converse over finite trees

DOI10.1145/2724712zbMATH Open1354.68124OpenAlexW2131842699MaRDI QIDQ2957698FDOQ2957698

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

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

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)

Cites Work

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

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

Uses Software

• XQuery
• CDuce
• PGSolver
• XPath

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)