Multi-valued model checking games (Q414899): Difference between revisions
From MaRDI portal
Created a new Item |
ReferenceBot (talk | contribs) Changed an Item |
||
(4 intermediate revisions by 4 users not shown) | |||
Property / review text | |||
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. The 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. | |||
Property / review text: 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. The 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. / rank | |||
Normal rank | |||
Property / reviewed by | |||
Property / reviewed by: Christel Baier / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 68Q60 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 91A80 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03B70 / rank | |||
Normal rank | |||
Property / zbMATH DE Number | |||
Property / zbMATH DE Number: 6033502 / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
model checking | |||
Property / zbMATH Keywords: model checking / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
mu-calculus | |||
Property / zbMATH Keywords: mu-calculus / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
multi-valued semantics | |||
Property / zbMATH Keywords: multi-valued semantics / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
game-based setting | |||
Property / zbMATH Keywords: game-based setting / rank | |||
Normal rank | |||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1016/j.jcss.2011.05.003 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W2037024461 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Automated Technology for Verification and Analysis / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4818796 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A game-based framework for CTL counterexamples and 3-valued abstraction-refinement / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Verification, Model Checking, and Abstract Interpretation / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q2754106 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4804892 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: CONCUR 2003 - Concurrency Theory / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Automata, Languages and Programming / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4818743 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Computer Aided Verification / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4531751 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Data structures for symbolic multi-valued model-checking / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Local model checking in the modal mu-calculus / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: An automata-theoretic approach to branching-time model checking / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4938419 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A lattice-theoretical fixpoint theorem and its applications / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Quantitative solution of omega-regular games380872 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4692885 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q2763694 / rank | |||
Normal rank | |||
links / mardi / name | links / mardi / name | ||
Latest revision as of 05:16, 5 July 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Multi-valued model checking games |
scientific article |
Statements
Multi-valued model checking games (English)
0 references
11 May 2012
0 references
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. The 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.
0 references
model checking
0 references
mu-calculus
0 references
multi-valued semantics
0 references
game-based setting
0 references