Games for the -calculus
DOI10.1016/0304-3975(95)00136-0zbMATH Open0872.03017OpenAlexW2467982476MaRDI QIDQ671352FDOQ671352
Authors: Igor Walukiewicz, Damian Niwiński 
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
Recommendations
regular treesMartin's determinacy theoremmodel of a formulamodel theorem for the \(\mu\)-calculuspropositional \(\mu\)-calculusrelation of a formulatestifying incorrectness of a program specification
2-person games (91A05) Modal logic (including the logic of norms) (03B45) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)
Cites Work
- Borel determinacy
- Propositional dynamic logic of regular programs
- CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus
- Results on the propositional \(\mu\)-calculus
- Title not available (Why is that?)
- On model checking for the \(\mu\)-calculus and its fragments
- Descriptive set theory
- 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
- Modal logics for communicating systems
- Title not available (Why is that?)
Cited In (42)
- Permutation games for the weakly aconjunctive \(\mu \)-calculus
- Uniform interpolation from cyclic proofs: the case of modal mu-calculus
- Bounded game-theoretic semantics for modal mu-calculus
- Completeness for the modal \(\mu\)-calculus: separating the combinatorics from the dynamics
- Verification, Model Checking, and Abstract Interpretation
- \(\mu\)-levels of interpolation
- From GTC to \textsc{Reset}: generating reset proof systems from cyclic proof systems
- Title not available (Why is that?)
- Game aspect of program verification
- Unambiguous Büchi Is Weak
- Lyndon Interpolation for Modal $$\mu $$-Calculus
- Coinduction in Flow: The Later Modality in Fibrations
- Coalgebraic satisfiability checking for arithmetic \(\mu\)-calculi
- Two ways to common knowledge
- Cyclic hypersequent system for transitive closure logic
- Certification for \(\mu \)-calculus with winning strategies
- \(\aleph_1\) and the modal \(\mu\)-calculus
- The proof theory of common knowledge
- On the proof theory of the modal mu-calculus
- Title not available (Why is that?)
- Title not available (Why is that?)
- Abstract cyclic proofs
- Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs
- Cyclic arithmetic is equivalent to Peano arithmetic
- Syntactic cut-elimination for a fragment of the modal mu-calculus
- Abstract cyclic proofs
- The variable hierarchy for the games \(\mu \)-calculus
- Cyclic implicit complexity
- On global induction mechanisms in aμ-calculus with explicit approximations
- Free \(\mu\)-lattices
- Unambiguity in automata theory
- EXPTIME Tableaux for the Coalgebraic μ-Calculus
- A focus system for the alternation-free \(\mu \)-calculus
- Circular (Yet Sound) Proofs in Propositional Logic
- Pushdown processes: Games and model-checking
- Subcalculus for set functions and cores of TU games.
- Ill-founded proof systems for intuitionistic linear-time temporal logic
- Proof systems for the modal \(\mu \)-calculus obtained by determinizing automata
- Cyclic proofs, hypersequents, and transitive closure logic
- Ambiguous classes in \(\mu\)-calculi hierarchies
- Focus-style proofs for the two-way alternation-free \(\mu \)-calculus
- NP reasoning in the monotone \(\mu\)-calculus
This page was built for publication: Games for the \(\mu\)-calculus
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q671352)
