This article describes Kripke structures as used in model checking. For a more general description, see Kripke semantics.
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.[citation needed]
Let AP be a set of atomic propositions, i.e. boolean expressions over variables, constants and predicate symbols. Clarke et al.[3] define a Kripke structure over AP as a 4-tupleM = (S, I, R, L) consisting of
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 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, R(si, si+1) holds. The word on the path ρ is a 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 (say, having only one initial state i ∈ I) may be identified with a Moore machine with a singleton input alphabet, and with the output function being its labeling function.[4]
Example
An example of Kripke structure
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.[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
Wikimedia Commons has media related to Kripke models.
^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.
^Clarke, Edmund M., Jr; Grumberg, Orna; Peled, Doron (December 1999). Model Checking. Cyber Physical Systems Series. MIT Press. p. 14. ISBN9780262032704.
^Klaus Schneider (2004). Verification of reactive systems: formal methods and algorithms. Springer. p. 45. ISBN978-3-540-00296-3.
kripke, structure, model, checking, this, article, describes, kripke, structures, used, model, checking, more, general, description, kripke, semantics, kripke, structure, variation, transition, system, originally, proposed, saul, kripke, used, model, checking,. This article describes Kripke structures as used in model checking For a more general description see Kripke semantics 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 citation needed Contents 1 Formal definition 2 Example 3 Relation to other notions 4 See also 5 ReferencesFormal definition EditLet AP be a set of atomic propositions i e boolean expressions over variables constants and predicate symbols Clarke et al 3 define a Kripke structure over AP as 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 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 r s1 s2 s3 such that for each i gt 0 R si si 1 holds The word on the path r is a sequence of sets of the atomic propositions w L s1 L s2 L s3 which is an w word over alphabet 2AP With this definition a Kripke structure say having only one initial state i I may be identified with a Moore machine with a singleton input alphabet and with the output function being its labeling function 4 Example Edit An example of Kripke structure 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 r 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 r M can produce execution words belonging to the language p q q p w p q q w Relation to other notions EditAlthough 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 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 m calculus 6 See also Edit Wikimedia Commons has media related to Kripke models Temporal logic Model checking Kripke semantics Linear temporal logic Computation tree logicReferences Edit 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 Clarke Edmund M Jr Grumberg Orna Peled Doron December 1999 Model Checking Cyber Physical Systems Series MIT Press p 14 ISBN 9780262032704 Klaus Schneider 2004 Verification of reactive systems formal methods and algorithms Springer p 45 ISBN 978 3 540 00296 3 Christel Baier Joost Pieter Katoen 2008 Principles of model checking The MIT Press pp 20 21 and 94 95 ISBN 978 0 262 02649 9 Clarke et al p 98 Retrieved from https en wikipedia org w index php title Kripke structure model checking amp oldid 1068734877, wikipedia, wiki, book, books, library,
