The mu-calculus and Model Checking
From MaRDI portal
Recommendations
- scientific article; zbMATH DE number 1059247
- -calculus model checking in Maude
- On model checking for the -calculus and its fragments
- scientific article; zbMATH DE number 2186291
- Model-checking the higher-dimensional modal -calculus
- Model checking in the modal -calculus and generic solutions
- Formal Techniques for Networked and Distributed Systems - FORTE 2005
- Tableau-based model checking in the propositional mu-calculus
- Decomposition theorems and model-checking for the modal -calculus
- Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus
Cites work
- A combinatorial strongly subexponential strategy improvement algorithm for mean payoff games
- A decidable characterization of locally testable tree languages
- A Deterministic Subexponential Algorithm for Solving Parity Games
- A linear algorithm to solve fixed-point equations on transition systems
- A linear-time model-checking algorithm for the alternation-free modal mu- calculus
- A subexponential lower bound for the random facet algorithm for parity games
- A Tight Lower Bound for Determinization of Transition Labeled Büchi Automata
- Alternating automata on infinite trees
- Alternating-time temporal logic
- An automata theoretic decision procedure for the propositional mu- calculus
- An exponential lower bound for the latest deterministic strategy iteration algorithms
- An Extension of Muchnik's Theorem
- An improved algorithm for the evaluation of fixpoint expressions
- An Optimal Strategy Improvement Algorithm for Solving Parity and Payoff Games
- Automata and fixed point logic: a coalgebraic perspective
- Automata for the modal -calculus and related results
- Automata theory and model checking
- Automata, logics, and infinite games. A guide to current research
- Back and forth between guarded and modal logics
- Borel determinacy
- Büchi complementation made tight
- Characterizing EF and EX tree logics
- Church’s Problem and a Tour through Automata Theory
- Clique-Width and Parity Games
- Coalgebraic logic
- Completeness of Kozen's axiomatisation of the propositional \(\mu\)-calculus.
- CTL^* and ECTL^* as fragments of the modal -calculus
- Decidability of Second-Order Theories and Automata on Infinite Trees
- Deciding Equivalence of Finite Tree Automata
- Deciding the winner in parity games is in \(\mathrm{UP}\cap\mathrm{co-UP}\)
- Elementary induction on abstract structures
- Elements of finite model theory.
- Entanglement and the complexity of directed graphs
- Fast and simple nested fixpoints
- Finite model theory and its applications.
- Finiteness is mu-ineffable
- From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata
- FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
- Game logic is strong enough for parity games
- Graph Games and Reactive Synthesis
- Guarded fixed point logics and the monadic theory of countable trees.
- scientific article; zbMATH DE number 1670778 (Why is no real title available?)
- scientific article; zbMATH DE number 5872386 (Why is no real title available?)
- scientific article; zbMATH DE number 5872401 (Why is no real title available?)
- scientific article; zbMATH DE number 3887063 (Why is no real title available?)
- scientific article; zbMATH DE number 3885853 (Why is no real title available?)
- scientific article; zbMATH DE number 3880483 (Why is no real title available?)
- scientific article; zbMATH DE number 3880651 (Why is no real title available?)
- scientific article; zbMATH DE number 3990873 (Why is no real title available?)
- scientific article; zbMATH DE number 4041866 (Why is no real title available?)
- scientific article; zbMATH DE number 56025 (Why is no real title available?)
- scientific article; zbMATH DE number 3602653 (Why is no real title available?)
- scientific article; zbMATH DE number 1223729 (Why is no real title available?)
- scientific article; zbMATH DE number 1254648 (Why is no real title available?)
- scientific article; zbMATH DE number 1324669 (Why is no real title available?)
- scientific article; zbMATH DE number 1032009 (Why is no real title available?)
- scientific article; zbMATH DE number 1142326 (Why is no real title available?)
- scientific article; zbMATH DE number 1500523 (Why is no real title available?)
- scientific article; zbMATH DE number 1556014 (Why is no real title available?)
- scientific article; zbMATH DE number 1796122 (Why is no real title available?)
- scientific article; zbMATH DE number 1796123 (Why is no real title available?)
- scientific article; zbMATH DE number 2087432 (Why is no real title available?)
- scientific article; zbMATH DE number 1903345 (Why is no real title available?)
- scientific article; zbMATH DE number 2113976 (Why is no real title available?)
- scientific article; zbMATH DE number 1424055 (Why is no real title available?)
- scientific article; zbMATH DE number 3315203 (Why is no real title available?)
- scientific article; zbMATH DE number 3328724 (Why is no real title available?)
- scientific article; zbMATH DE number 3339435 (Why is no real title available?)
- Infinite games on finitely coloured graphs with applications to automata on infinite trees
- Infinite games played on finite graphs
- Inflationary fixed points in modal logic
- Interpolation and model checking
- Logical questions concerning the μ-calculus: Interpolation, Lyndon and Łoś-Tarski
- Mathematical Foundations of Computer Science 2003
- Modal languages and bounded fragments of predicate logic
- Modal logic
- Model checking and boolean graphs
- Model checking games for the quantitative \(\mu \)-calculus
- Monadic second-order logic on tree-like structures
- Nondeterministic controllers of nondeterministic processes
- On modal -calculus over reflexive symmetric graphs
- On model checking for the -calculus and its fragments
- On Nonterminating Stochastic Games
- On the equivalence of game and denotational semantics for the probabilistic -calculus
- On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic
- On the frequency of the transfer paradox
- Parity games on undirected graphs
- Perfect Information Stochastic Priority Games
- Piecewise testable tree languages
- Propositional dynamic logic of looping and converse is elementarily decidable
- Propositional dynamic logic of regular programs
- Quantitative solution of omega-regular games
- Regular tree languages definable in FO and in FO\(_{\mathrm{mod}}\)
- Results on the propositional \(\mu\)-calculus
- Solving Parity Games in Big Steps
- Symbolic model checking for real-time systems
- The Büchi Complementation Saga
- The Complexity of Enriched Mu-Calculi
- The complexity of stochastic games
- The Complexity of Tree Automata and Logics of Programs
- The modal -calculus caught off guard
- The modal mu-calculus alternation hierarchy is strict
- The variable hierarchy of the \(\mu\)-calculus is strict
- Theμ-calculus alternation-depth hierarchy is strict on binary trees
- Timed modal logics for real-time systems. Specification, verification and control
- Types and higher-order recursion schemes for verification of higher-order programs
- Wreath products of forest algebras, with applications to tree logics
Cited in
(48)- Mu-calculus path checking
- Situation calculus for controller synthesis in manufacturing systems with first-order state representation
- Bounded game-theoretic semantics for modal mu-calculus
- A focus system for the alternation-free \(\mu \)-calculus
- Temporal refinements for guarded recursive types
- Strategies, model checking and branching-time properties in Maude
- Equivalence of probabilistic \(\mu\)-calculus and p-automata
- Simulating and model checking membrane systems using strategies in Maude
- Metalevel transformation of strategies
- Knowledge forgetting in propositional \(\mu\)-calculus
- Using assumptions to distribute alternation free {\(\mu\)}-calculus model checking
- Canonicity results for mu-calculi: an algorithmic approach
- scientific article; zbMATH DE number 2186291 (Why is no real title available?)
- Abstraction and abstraction refinement
- Combining Model Checking and Deduction
- Graph Games and Reactive Synthesis
- Enriched MU-Calculi Module Checking
- scientific article; zbMATH DE number 1059247 (Why is no real title available?)
- _1 and the modal -calculus
- scientific article; zbMATH DE number 7136664 (Why is no real title available?)
- Simple fixpoint iteration to solve parity games
- Family-based SPL model checking using parity games with variability
- scientific article; zbMATH DE number 7559481 (Why is no real title available?)
- On model checking for the -calculus and its fragments
- 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
- Lyndon Interpolation for Modal $$\mu $$-Calculus
- Implementing a CTL model checker with \(\mu \mathcal{G}\), a language for programming graph neural networks
- Semiring provenance for Büchi games: strategy analysis with absorptive polynomials
- Complexity results for modal logic with recursion via translations and tableaux
- Systems of fixpoint equations: abstraction, games, up-to techniques and local algorithms
- Semiring provenance for Büchi games: strategy analysis with absorptive polynomials
- The best a monitor can do
- The Strahler number of a parity game
- Progress, justness and fairness in modal -calculus formulae
- Faster and smaller solutions of obliging games
- Validity of contextual formulas
- Regular games with imperfect information are not that regular
- Intuitionistic -calculus with the Lewis arrow
- Infinitary refinement types for temporal properties in Scott domains
- Real equation systems with alternating fixed-points
- Complete game logic with sabotage
- A sample-driven solving procedure for the repeated reachability of quantum continuous-time Markov chains
- Efficient iterative programs with distributed data collections
- Stochastic games with synchronization objectives
- A dichotomy theorem for ordinal ranks in MSO
- Distributed symbolic model checking for -calculus
This page was built for publication: The mu-calculus and Model Checking
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3176384)
