A Proof System for the Linear Time μ-Calculus

DOI10.1007/11944836_26MaRDI QIDQ5385992zbMATH OpenOpenAlexFDO

Authors Christian Dax, Martin Hofmann, Martin Lange

Publication date 17 April 2008

Published in FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11944836_26

Mathematics Subject Classification ID

Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Temporal logic (03B44) Logic in computer science (03B70) Complexity of proofs (03F20)

Recommendations

• Constructive completeness for the linear-time \(\mu \)-calculus
• scientific article; zbMATH DE number 2102740
• Towards completeness via proof search in the linear time \(\mu\)-calculus: the case of Büchi inclusions
• From linear time to branching time
• Satisfiability of linear time mu-calculus on finite traces

Cited in

(29)

• Size-change termination and satisfiability for linear-time temporal logics
• Loop-type sequent calculi for temporal logic
• Complete axiomatization of the stutter-invariant fragment of the linear time \(\mu\)-calculus
• Verification, Model Checking, and Abstract Interpretation
• scientific article; zbMATH DE number 7155168 (Why is no real title available?)
• Coinduction in Flow: The Later Modality in Fibrations
• Two ways to common knowledge
• Satisfiability of linear time mu-calculus on finite traces
• Certifying proofs for SAT-based model checking
• Constructive completeness for the linear-time \(\mu \)-calculus
• Cyclic hypersequent system for transitive closure logic
• Local validity for circular proofs in linear logic with fixed points
• The proof theory of common knowledge
• Loop-check specification for a sequent calculus of temporal logic
• Probabilistic logics based on Riesz spaces
• On the proof theory of the modal mu-calculus
• From linear time to branching time
• Non-well-founded deduction for induction and coinduction
• Cyclic arithmetic is equivalent to Peano arithmetic
• Towards completeness via proof search in the linear time \(\mu\)-calculus: the case of Büchi inclusions
• Cyclic implicit complexity
• Bouncing threads for circular and non-wellfounded proofs. Towards compositionality with circular proofs
• A focus system for the alternation-free \(\mu \)-calculus
• Circular (Yet Sound) Proofs in Propositional Logic
• Ramsey-based inclusion checking for visibly pushdown automata
• Intuitionistic linear-time \(\mu\)-calculus
• A linear perspective on cut-elimination for non-wellfounded sequent calculi with least and greatest fixed-points
• Ill-founded proof systems for intuitionistic linear-time temporal logic
• scientific article; zbMATH DE number 2102740 (Why is no real title available?)

This page was built for publication: A Proof System for the Linear Time μ-Calculus

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