Multi-valued model checking games
The game-based approach offers a very elegant way for establishing properties of systems modeled by Kripke structures. The paper extends the game-based framework of \(\mu\)-calculus model checking to the multi-valued setting. Structures in the multi-valued semantics are Kripke structures defined over a lattice. The meaning of a \(\mu\)-calculus formula in a state \(s\) of the Kripke structure is an element of the lattice, called the value of the formula in \(s\). The task of the multi-valued model checking problem is then to compute the value of a given formula in a given state. This problem has many applications in verification, such as handling abstract or partial models, analyzing systems in the presence of inconsistent views, and performing temporal logic query checking.NEWLINENEWLINEThe paper defines a new game for the multi-valued model checking problem of the full \(\mu\)-calculus, and demonstrates how to derive from it a direct model checking algorithm for its alternation-free fragment. The algorithm handles the multi-valued structure without any reduction. The paper discusses properties of the new game. It also shows that the usual resemblance between the automata-based and the game-based approach does not hold in the multi-valued setting and how it can be regained by changing the nature of the game.
- A game-based framework for CTL counterexamples and 3-valued abstraction-refinement
- A game-based framework for CTL counterexamples and 3-valued abstraction-refinement.
- A lattice-theoretical fixpoint theorem and its applications
- An automata-theoretic approach to branching-time model checking
- Automata, Languages and Programming
- Automated Technology for Verification and Analysis
- Data structures for symbolic multi-valued model-checking
- scientific article; zbMATH DE number 1670794 (Why is no real title available?)
- scientific article; zbMATH DE number 1693039 (Why is no real title available?)
- scientific article; zbMATH DE number 1744958 (Why is no real title available?)
- scientific article; zbMATH DE number 194916 (Why is no real title available?)
- scientific article; zbMATH DE number 1903350 (Why is no real title available?)
- scientific article; zbMATH DE number 2104629 (Why is no real title available?)
- scientific article; zbMATH DE number 2102712 (Why is no real title available?)
- scientific article; zbMATH DE number 1405445 (Why is no real title available?)
- Local model checking in the modal mu-calculus
- Multi-valued model checking via classical model checking.
- Quantitative solution of -regular games
- Verification, Model Checking, and Abstract Interpretation
- Simulation for lattice-valued doubly labeled transition systems
- Modal transition system encoding of featured transition systems
- Automata games for multiple-model checking
- Latticed Simulation Relations and Games
- Latticed simulation relations and games
- Don't know for multi-valued systems
- scientific article; zbMATH DE number 1405445 (Why is no real title available?)
- Multi-valued verification of strategic ability
- Model checking fuzzy computation tree logic
- Automata, Languages and Programming
- Logic Programming
- Automated Technology for Verification and Analysis
- Verification, Model Checking, and Abstract Interpretation
- Model checking computation tree logic over finite lattices
- Product line process theory
This page was built for publication: Multi-valued model checking games
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q414899)
