Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of GraphSearch.
Concept
Kripke structure (model checking)
Summary
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, used in model checking 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.
Let AP be a set of atomic propositions, i.e. boolean-valued expressions formed from variables, constants and predicate symbols. Clarke et al. 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 ρ = s1, s2, s3, ... such that for each i > 0, R(si, si+1) holds.
The word on the path ρ is the 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.
Let the set of atomic propositions AP = .
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 = .
I = .
R = .
L = .
About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.