Kripke structure (model checking)
Script error: No such module "about".
A Kripke structure is a variation of the transition system, originally proposed by Saul Kripke,[1] used in model checking[2] to represent the behavior of a system. It consists of a graph whose nodes represent the reachable states of the system and whose edges represent state transitions, together with a labelling function which maps each node to a set of properties that hold in the corresponding state. Temporal logics are traditionally interpreted in terms of Kripke structures.Script error: No such module "Unsubst".
Formal definition
Let Template:Mvar be a set of atomic propositions, i.e. boolean-valued expressions formed from variables, constants and predicate symbols. Clarke et al.[3] define a Kripke structure over Template:Mvar as a 4-tuple Template:Math consisting of
- a finite set of states Template:Mvar.
- a set of initial states Template:Math.
- a transition relation Template:Math such that Template:Mvar is left-total, i.e., Template:Math such that Template:Math.
- a labeling (or interpretation) function Template:Math.
Since Template:Mvar is left-total, it is always possible to construct an infinite path through the Kripke structure. A deadlock state can be modeled by a single outgoing edge back to itself. The labeling function Template:Mvar defines for each state Template:Math the set Template:Math of all atomic propositions that are valid in Template:Mvar.
A path of the structure Template:Mvar is a sequence of states Template:Math such that for each Template:Math, Template:Math holds. The word on the path Template:Mvar is the sequence of sets of the atomic propositions Template:Math, which is an ω-word over alphabet Template:Math.
With this definition, a Kripke structure (say, having only one initial state Template:Math may be identified with a Moore machine with a singleton input alphabet, and with the output function being its labeling function.[4]
Example
Let the set of atomic propositions Template:Math. Template:Mvar and Template:Mvar can model arbitrary boolean properties of the system that the Kripke structure is modelling.
The figure at right illustrates a Kripke structure Template:Math, where
Template:Mvar may produce a path Template:Math and Template:Math is the execution word over the path Template:Mvar. Template:Mvar can produce execution words belonging to the language Template:Math.
Relation to other notions
Although this terminology is widespread in the model checking community, some textbooks on model checking do not define "Kripke structure" in this extended way (or at all in fact), but simply use the concept of a (labelled) transition system, which additionally has a set Template:Mvar of actions, and the transition relation is defined as a subset of Template:Math, which they additionally extend to include a set of atomic propositions and a labeling function for the states as well (Template:Mvar as defined above.) In this approach, the binary relation obtained by abstracting away the action labels is called a state graph.[5]
Clarke et al. redefine a Kripke structure as a set of transitions (instead of just one), which is equivalent to the labeled transitions above, when they define the semantics of modal μ-calculus.[6]
See also
References
- ↑ Kripke, Saul, 1963, "Semantical Considerations on Modal Logic," Acta Philosophica Fennica, 16: 83-94
- ↑ Clarke, Edmund M. (2008): The Birth of Model Checking. in: Grumberg, Orna and Veith, Helmut eds.: 25 Years of Model Checking, Vol. 5000: Lecture Notes in Computer Science. Springer Berlin Heidelberg, p. 1-26.
- ↑ Script error: No such module "citation/CS1".
- ↑ Script error: No such module "citation/CS1".
- ↑ Script error: No such module "citation/CS1".
- ↑ Clarke et al. p. 98