Games for the \(\mu\)-calculus

DOI10.1016/0304-3975(95)00136-0zbMath0872.03017OpenAlexW2467982476MaRDI QIDQ671352

Igor Walukiewicz, Damian Niwinski

Publication date: 27 February 1997

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(95)00136-0

zbMATH Keywords

regular treesMartin's determinacy theoremmodel of a formulamodel theorem for the \(\mu\)-calculuspropositional \(\mu\)-calculusrelation of a formulatestifying incorrectness of a program specification

Mathematics Subject Classification ID

2-person games (91A05) Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Uniform interpolation from cyclic proofs: the case of modal mu-calculus ⋮ A focus system for the alternation-free \(\mu \)-calculus ⋮ $\aleph_1$ and the modal $\mu$-calculus ⋮ Unnamed Item ⋮ Two Ways to Common Knowledge ⋮ Cyclic hypersequent system for transitive closure logic ⋮ Circular (Yet Sound) Proofs in Propositional Logic ⋮ Focus-style proofs for the two-way alternation-free \(\mu \)-calculus ⋮ Abstract cyclic proofs ⋮ Cyclic Arithmetic Is Equivalent to Peano Arithmetic ⋮ The Proof Theory of Common Knowledge ⋮ Coinduction in Flow: The Later Modality in Fibrations ⋮ Completeness for the modal \(\mu\)-calculus: separating the combinatorics from the dynamics ⋮ Ambiguous classes in \(\mu\)-calculi hierarchies ⋮ Syntactic cut-elimination for a fragment of the modal mu-calculus ⋮ Free \(\mu\)-lattices ⋮ Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs ⋮ On the proof theory of the modal mu-calculus ⋮ $$\mu $$ μ -Levels of Interpolation ⋮ Unambiguous Büchi Is Weak ⋮ On global induction mechanisms in aμ-calculus with explicit approximations ⋮ EXPTIME Tableaux for the Coalgebraic μ-Calculus ⋮ Unambiguity in Automata Theory ⋮ NP reasoning in the monotone \(\mu\)-calculus ⋮ Pushdown processes: Games and model-checking ⋮ Cyclic proofs, hypersequents, and transitive closure logic ⋮ Bounded game-theoretic semantics for modal mu-calculus

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Modal logics for communicating systems
• Results on the propositional \(\mu\)-calculus
• An automata theoretic decision procedure for the propositional mu- calculus
• An elementary proof of the completeness of PDL
• Local model checking in the modal mu-calculus
• Borel determinacy
• Propositional dynamic logic of regular programs
• CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus
• On model checking for the \(\mu\)-calculus and its fragments