Kripke structure
Encyclopedia
A Kripke structure is a type of nondeterministic finite state machine
proposed by Saul Kripke
, used in model checking
to represent the behavior of a system.
It is a simple abstract machine (a mathematical object)
to capture an idea of a computing machine,
without adding unnecessary complexities.
It is basically a graph
whose nodes represent the reachable states of the system and whose edges represent state transitions. A labeling function maps each node to a set of properties that hold in the corresponding state. Temporal logic
s are traditionally interpreted in terms of Kripke structures.
, i.e. boolean expressions over variables, constants and predicate symbols. Clarke et al. define a Kripke structure over AP is a 4-tuple M = (S, I, R, L) consisting of
Since R 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 L defines for each state s ∈ S the set L(s) of all atomic propositions that are valid in s.
A path of the structure M is a sequence of states ρ = s1,s2,s3,... such that for each i > 0, si+1 = R(si).
The word on the path ρ is sequence of sets of the atomic propositions
w=L(s1),L(s2),L(s3),...,
which is an ω-word over alphabet 2AP.
With this definition, a Kripke structure may be identified with a Moore machine
with a singleton input alphabet, and with the output function being its labeling function.
p and q can model arbitrary boolean properties of the system that the kripke structure is
modelling.
The figure at right illustrates a kripke structure M=(S, I, R, L),
where
M may produce a path ρ = s1,s2,s1,s2,s3,s3,s3,... and w = {p,q},{q},{p,q},{q},{p},{p},{p},... is the execution word over the path ρ.
M can produce execution words belonging to the language ({p,q}{q})*({p})ω∪({p,q}{q})ω.
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.
Nondeterministic finite state machine
In the automata theory, a nondeterministic finite state machine or nondeterministic finite automaton is a finite state machine where from each state and a given input symbol the automaton may jump into several possible next states...
proposed by Saul Kripke
Saul Kripke
Saul Aaron Kripke is an American philosopher and logician. He is a professor emeritus at Princeton and teaches as a Distinguished Professor of Philosophy at the CUNY Graduate Center...
, used in model checking
Model checking
In computer science, model checking refers to the following problem:Given a model of a system, test automatically whether this model meets a given specification....
to represent the behavior of a system.
It is a simple abstract machine (a mathematical object)
to capture an idea of a computing machine,
without adding unnecessary complexities.
It is basically a graph
Graph (mathematics)
In mathematics, a graph is an abstract representation of a set of objects where some pairs of the objects are connected by links. The interconnected objects are represented by mathematical abstractions called vertices, and the links that connect some pairs of vertices are called edges...
whose nodes represent the reachable states of the system and whose edges represent state transitions. A labeling function maps each node to a set of properties that hold in the corresponding state. Temporal logic
Temporal logic
In logic, the term temporal logic is used to describe any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time. In a temporal logic we can then express statements like "I am always hungry", "I will eventually be hungry", or "I will be hungry...
s are traditionally interpreted in terms of Kripke structures.
Formal definition
Let AP be a set of atomic propositionsPropositional calculus
In mathematical logic, a propositional calculus or logic is a formal system in which formulas of a formal language may be interpreted as representing propositions. A system of inference rules and axioms allows certain formulas to be derived, called theorems; which may be interpreted as true...
, i.e. boolean expressions over variables, constants and predicate symbols. Clarke et al. define a Kripke structure over AP is a 4-tuple M = (S, I, R, L) consisting of
- a finite set of states S.
- a set of initial states I ⊆ S.
- a transition relation R ⊆ S × S such that R is left-total, i.e., ∀s ∈ S ∃s' ∈ S such that (s,s') ∈ R.
- a labeling (or interpretation) function L: S → 2AP.
Since R is left-total, it is always possible to construct an infinite path through the Kripke structure. A deadlock
Deadlock
A deadlock is a situation where in two or more competing actions are each waiting for the other to finish, and thus neither ever does. It is often seen in a paradox like the "chicken or the egg"...
state can be modeled by a single outgoing edge back to itself.
The labeling function L defines for each state s ∈ S the set L(s) of all atomic propositions that are valid in s.
A path of the structure M is a sequence of states ρ = s1,s2,s3,... such that for each i > 0, si+1 = R(si).
The word on the path ρ is sequence of sets of the atomic propositions
w=L(s1),L(s2),L(s3),...,
which is an ω-word over alphabet 2AP.
With this definition, a Kripke structure may be identified with a Moore machine
Moore machine
In the theory of computation, a Moore machine is a finite-state machine, whose output values are determined solely by its current state.-Name:The Moore machine is named after Edward F...
with a singleton input alphabet, and with the output function being its labeling function.
Example
Let the set of atomic propositions AP = {p,q}.p and q can model arbitrary boolean properties of the system that the kripke structure is
modelling.
The figure at right illustrates a kripke structure M=(S, I, R, L),
where
- S = {s1,s2,s3}.
- I = {s1}.
- R = {(s1,s2),(s2,s1)(s2,s3),(s3,s3)}.
- L = { (s1, {p,q}), (s2, {q}), (s3, {p}) }.
M may produce a path ρ = s1,s2,s1,s2,s3,s3,s3,... and w = {p,q},{q},{p,q},{q},{p},{p},{p},... is the execution word over the path ρ.
M can produce execution words belonging to the language ({p,q}{q})*({p})ω∪({p,q}{q})ω.
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 Act of actions, and the transition relation is defined as a subset of S × Act × S, which they additionally extend to include a set of atomic propositions and a labeling function for the states as well (L as defined above.) In this approach, the binary relation obtained by abstracting away the action labels is called a state graph.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.
See also
- Temporal logicTemporal logicIn logic, the term temporal logic is used to describe any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time. In a temporal logic we can then express statements like "I am always hungry", "I will eventually be hungry", or "I will be hungry...
- Model checkingModel checkingIn computer science, model checking refers to the following problem:Given a model of a system, test automatically whether this model meets a given specification....
- Kripke semanticsKripke semanticsKripke semantics is a formal semantics for non-classical logic systems created in the late 1950s and early 1960s by Saul Kripke. It was first made for modal logics, and later adapted to intuitionistic logic and other non-classical systems...
- Linear temporal logicLinear temporal logicIn logic, Linear temporal logic is a modal temporal logic with modalities referring to time. In LTL, one can encode formulae about the future of paths such as that a condition will eventually be true, that a condition will be true until another fact becomes true, etc. It is a fragment of the more...
- Computation tree logic