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

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

Recommendations

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

Cited in

(36)

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

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)