A Proof System for the Linear Time μ-Calculus

DOI10.1007/11944836_26zbMath1163.03308OpenAlexW1568149704MaRDI QIDQ5385992

Christian Dax, Martin Lange, Martin Hofmann

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

Logic in computer science (03B70) 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) Complexity of proofs (03F20)

Related Items (18)

Ramsey-Based Inclusion Checking for Visibly Pushdown Automata ⋮ Size-Change Termination and Satisfiability for Linear-Time Temporal Logics ⋮ A focus system for the alternation-free \(\mu \)-calculus ⋮ Unnamed Item ⋮ Two Ways to Common Knowledge ⋮ Unnamed Item ⋮ Cyclic hypersequent system for transitive closure logic ⋮ Circular (Yet Sound) Proofs in Propositional Logic ⋮ Cyclic Arithmetic Is Equivalent to Peano Arithmetic ⋮ Loop-type sequent calculi for temporal logic ⋮ The Proof Theory of Common Knowledge ⋮ Coinduction in Flow: The Later Modality in Fibrations ⋮ Unnamed Item ⋮ On the proof theory of the modal mu-calculus ⋮ Satisfiability of Linear Time Mu-Calculus on Finite Traces ⋮ 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

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