A Kripke structure is a type of nondeterministic finite state machine used in model checking to represent the behaviour of a system. 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 logics are traditionally interpreted in terms of Kripke structures.

Let AP be a set of atomic propositions, i.e. boolean expressions over variables, constants and predicate symbols.

A Kripke structure is a 4-tuple M = (S,\; I,\; R,\; L) consisting of

  • a finite set of states S\;
  • a set of initial states I \subseteq S
  • a transition relation R \subseteq S \! \times \! S \; where \; \forall s \! \in \! S, \; \exist s^' \!\! \in \! S such that  (s,s^') \in R
  • a labeling (or interpretation) function L: S \rightarrow 2^{AP}

Since R is left-total, it is always possible to construct an infinite path through the Kripke structure. Thus a deadlock state has a single outgoing edge back to itself.

The labeling function L defines for each state sS the set L(s) of all atomic propositions that are valid in s. In the Kripke structure, the transition function should be complete,i.e each and every state should have transition.In other words there should not be any dead states in the graph.

Combining the Semantics of the Atomistic Model and the Kripke Structure with each other

If we use the notation of the Kripke structure for the Atomistic Model we get the definitions:

The atomistic model is a Kripke structure,  a 4-tuple M = (S,\; I,\; R,\; L) consisting of

  • a finite set of  states S\; implemented as symbols in the model illustrating clauses of the original clause and side effects caused by the simulation/evaluation processes.
  • a set of initial states I \subseteq S implemented as symbols of the models: either clauses or side effects.
  • a transition relation R \subseteq S \! \times \! S \; where \; \forall s \! \in \! S, \; \exist s^' \!\! \in \! S such that  (s,s^') \in R implemented as links of the symbols.
  • a labeling (or interpretation) function L: S \rightarrow 2^{AP} implemented as a command-fact in each symbol.

Summary about the correspondece

The atomistic model is downwards compatible with the Kripke structure. It leads to a conculsion (by inspection) that all functions and mathematical processes intended for the Kripke structure, e.g. model checking, can be borrowed for the use of the atomistic model. Only a simple transformation is needed.

Some links:

Advertisements