The mu-calculus and Model Checking
From MaRDI portal
Publication:3176384
DOI10.1007/978-3-319-10575-8_26zbMath1392.68236OpenAlexW2804589645MaRDI QIDQ3176384
Julian Bradfield, Igor Walukiewicz
Publication date: 20 July 2018
Published in: Handbook of Model Checking (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-10575-8_26
Modal logic (including the logic of norms) (03B45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Related Items
Family-Based SPL Model Checking Using Parity Games with Variability ⋮ Abstraction and Abstraction Refinement ⋮ Combining Model Checking and Deduction ⋮ Graph Games and Reactive Synthesis ⋮ $\aleph_1$ and the modal $\mu$-calculus ⋮ Equivalence of probabilistic \(\mu\)-calculus and p-automata ⋮ Unnamed Item ⋮ Simulating and model checking membrane systems using strategies in Maude ⋮ Metalevel transformation of strategies ⋮ Knowledge forgetting in propositional \(\mu\)-calculus ⋮ Universal algorithms for parity games and nested fixpoints ⋮ The alternation hierarchy of the \(\mu \)-calculus over weakly transitive frames ⋮ Computing sufficient and necessary conditions in CTL: a forgetting approach ⋮ Unnamed Item ⋮ Temporal refinements for guarded recursive types ⋮ Strategies, model checking and branching-time properties in Maude ⋮ Unnamed Item ⋮ Situation calculus for controller synthesis in manufacturing systems with first-order state representation ⋮ Bounded game-theoretic semantics for modal mu-calculus
Uses Software
Cites Work
- Decidability of Second-Order Theories and Automata on Infinite Trees
- Back and forth between guarded and modal logics
- On model checking for the \(\mu\)-calculus and its fragments
- On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Deciding the winner in parity games is in \(\mathrm{UP}\cap\mathrm{co-UP}\)
- On the frequency of the transfer paradox
- Parity games on undirected graphs
- Timed modal logics for real-time systems. Specification, verification and control
- Finite model theory and its applications.
- Elements of finite model theory.
- Results on the propositional \(\mu\)-calculus
- A combinatorial strongly subexponential strategy improvement algorithm for mean payoff games
- Alternating automata on infinite trees
- A linear algorithm to solve fixed-point equations on transition systems
- An automata theoretic decision procedure for the propositional mu- calculus
- The complexity of stochastic games
- Elementary induction on abstract structures
- Borel determinacy
- Finiteness is mu-ineffable
- Propositional dynamic logic of regular programs
- Modal languages and bounded fragments of predicate logic
- The modal mu-calculus alternation hierarchy is strict
- Infinite games on finitely coloured graphs with applications to automata on infinite trees
- Coalgebraic logic
- Infinite games played on finite graphs
- Model checking and boolean graphs
- CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus
- Symbolic model checking for real-time systems
- Fast and simple nested fixpoints
- An improved algorithm for the evaluation of fixpoint expressions
- Game logic is strong enough for parity games
- Monadic second-order logic on tree-like structures
- A linear-time model-checking algorithm for the alternation-free modal mu- calculus
- Guarded fixed point logics and the monadic theory of countable trees.
- Completeness of Kozen's axiomatisation of the propositional \(\mu\)-calculus.
- Automata, logics, and infinite games. A guide to current research
- Quantitative solution of omega-regular games
- Entanglement and the complexity of directed graphs
- Model checking games for the quantitative \(\mu \)-calculus
- Automata and fixed point logic: a coalgebraic perspective
- Characterizing EF and EX tree logics
- The variable hierarchy of the \(\mu\)-calculus is strict
- On the equivalence of game and denotational semantics for the probabilistic mu-calculus
- Wreath Products of Forest Algebras, with Applications to Tree Logics
- Regular tree languages definable in FO and in FO mod
- The Modal μ-Calculus Caught Off Guard
- Piecewise testable tree languages
- Automata Theory and Model Checking
- Interpolation and Model Checking
- Graph Games and Reactive Synthesis
- An Exponential Lower Bound for the Latest Deterministic Strategy Iteration Algorithms
- A decidable characterization of locally testable tree languages
- A Deterministic Subexponential Algorithm for Solving Parity Games
- Alternating-time temporal logic
- Deciding Equivalence of Finite Tree Automata
- The Complexity of Enriched Mu-Calculi
- An Optimal Strategy Improvement Algorithm for Solving Parity and Payoff Games
- Automata for the modal μ-calculus and related results
- The Büchi Complementation Saga
- Clique-Width and Parity Games
- A Tight Lower Bound for Determinization of Transition Labeled Büchi Automata
- Propositional dynamic logic of looping and converse is elementarily decidable
- The Complexity of Tree Automata and Logics of Programs
- An Extension of Muchnik's Theorem
- Theμ-calculus alternation-depth hierarchy is strict on binary trees
- Logical questions concerning the μ-calculus: Interpolation, Lyndon and Łoś-Tarski
- FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
- Types and higher-order recursion schemes for verification of higher-order programs
- Inflationary fixed points in modal logic
- On modal -calculus over reflexive symmetric graphs
- Büchi Complementation Made Tight
- From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata
- Perfect Information Stochastic Priority Games
- Mathematical Foundations of Computer Science 2003
- Church’s Problem and a Tour through Automata Theory
- Solving Parity Games in Big Steps
- On Nonterminating Stochastic Games
