Kripke structure (model checking)

Last updated August 21, 2024

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 ]}

Formal definition

Let $AP$ 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 $AP$ as 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$ such that $R$ is left-total, i.e., $\foralls \in S \existss' \in S$ such that $(s,s') \in R$ .
a labeling (or interpretation) function $L : S \to 2 AP$ .

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 \in 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 $ρ = s 1, s 2, s 3, ...$ such that for each $i > 0$ , $R (s i, s i +1)$ holds. The word on the path $ρ$ is the sequence of sets of the atomic propositions $w = L (s 1), L (s 2), L (s 3), ...$ , which is an ω-word over alphabet $2 AP$ .

With this definition, a Kripke structure (say, having only one initial state $i \in I)$ 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 $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 = {s 1, s 2, s 3}$ .
$I = {s 1}$ .
$R = {(s 1, s 2), (s 2, s 1) (s 2, s 3), (s 3, s 3)}$ .
$L = {(s 1, {p, q}), (s 2, {q}), (s 3, {p})}$ .

$M$ may produce a path $ρ = s 1, s 2, s 1, s 2, s 3, s 3, s 3, ...$ 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}) ω \cup ({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 \times Act \times 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]

Related Research Articles

In logic, temporal logic is any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time. It is sometimes also used to refer to tense logic, a modal logic-based system of temporal logic introduced by Arthur Prior in the late 1950s, with important contributions by Hans Kamp. It has been further developed by computer scientists, notably Amir Pnueli, and logicians.

Modal logic is a kind of logic used to represent statements about necessity and possibility. It plays a major role in philosophy and related fields as a tool for understanding concepts such as knowledge, obligation, and causation. For instance, in epistemic modal logic, the formula $can be used to represent the statement that is known. In deontic modal logic, that same formula can represent that is a moral obligation. Modal logic considers the inferences that modal statements give rise to. For instance, most epistemic modal logics treat the formula as a tautology, representing the principle that only true statements can count as knowledge. However, this formula is not a tautology in deontic modal logic, since what ought to be true can be false.$

In logic, linear temporal logic or linear-time temporal logic (LTL) is a modal temporal logic with modalities referring to time. In LTL, one can encode formulae about the future of paths, e.g., a condition will eventually be true, a condition will be true until another fact becomes true, etc. It is a fragment of the more complex CTL*, which additionally allows branching time and quantifiers. LTL is sometimes called propositional temporal logic, abbreviated PTL. In terms of expressive power, linear temporal logic (LTL) is a fragment of first-order logic.

In mathematical logic, a superintuitionistic logic is a propositional logic extending intuitionistic logic. Classical logic is the strongest consistent superintuitionistic logic; thus, consistent superintuitionistic logics are called intermediate logics.

Computation tree logic (CTL) is a branching-time logic, meaning that its model of time is a tree-like structure in which the future is not determined; there are different paths in the future, any one of which might be an actual path that is realized. It is used in formal verification of software or hardware artifacts, typically by software applications known as model checkers, which determine if a given artifact possesses safety or liveness properties. For example, CTL can specify that when some initial condition is satisfied, then all possible executions of a program avoid some undesirable condition. In this example, the safety property could be verified by a model checker that explores all possible transitions out of program states satisfying the initial condition and ensures that all such executions satisfy the property. Computation tree logic belongs to a class of temporal logics that includes linear temporal logic (LTL). Although there are properties expressible only in CTL and properties expressible only in LTL, all properties expressible in either logic can also be expressed in CTL*.

Kripke semantics is a formal semantics for non-classical logic systems created in the late 1950s and early 1960s by Saul Kripke and André Joyal. It was first conceived for modal logics, and later adapted to intuitionistic logic and other non-classical systems. The development of Kripke semantics was a breakthrough in the theory of non-classical logics, because the model theory of such logics was almost non-existent before Kripke.

Common knowledge is a special kind of knowledge for a group of agents. There is common knowledge of p in a group of agents G when all the agents in G know p, they all know that they know p, they all know that they all know that they know p, and so on ad infinitum. It can be denoted as $.$

In mathematical logic, Craig's interpolation theorem is a result about the relationship between different logical theories. Roughly stated, the theorem says that if a formula φ implies a formula ψ, and the two have at least one atomic variable symbol in common, then there is a formula ρ, called an interpolant, such that every non-logical symbol in ρ occurs both in φ and ψ, φ implies ρ, and ρ implies ψ. The theorem was first proved for first-order logic by William Craig in 1957. Variants of the theorem hold for other logics, such as propositional logic. A stronger form of Craig's interpolation theorem for first-order logic was proved by Roger Lyndon in 1959; the overall result is sometimes called the Craig–Lyndon theorem.

In theoretical computer science, the modal μ-calculus is an extension of propositional modal logic by adding the least fixed point operator μ and the greatest fixed point operator ν, thus a fixed-point logic.

CTL* is a superset of computational tree logic (CTL) and linear temporal logic (LTL). It freely combines path quantifiers and temporal operators. Like CTL, CTL* is a branching-time logic. The formal semantics of CTL* formulae are defined with respect to a given Kripke structure.

In logic, a modal companion of a superintuitionistic (intermediate) logic L is a normal modal logic that interprets L by a certain canonical translation, described below. Modal companions share various properties of the original intermediate logic, which enables to study intermediate logics using tools developed for modal logic.

In theoretical computer science, a transition system is a concept used in the study of computation. It is used to describe the potential behavior of discrete systems. It consists of states and transitions between states, which may be labeled with labels chosen from a set; the same label may appear on more than one transition. If the label set is a singleton, the system is essentially unlabeled, and a simpler definition that omits the labels is possible.

An interpretation is an assignment of meaning to the symbols of a formal language. Many formal languages used in mathematics, logic, and theoretical computer science are defined in solely syntactic terms, and as such do not have any meaning until they are given some interpretation. The general study of interpretations of formal languages is called formal semantics.

In automata theory, a branch of theoretical computer science, an ω-automaton is a variation of a finite automaton that runs on infinite, rather than finite, strings as input. Since ω-automata do not stop, they have a variety of acceptance conditions rather than simply a set of accepting states.

In automata theory, a semi-deterministic Büchi automaton is a special type of Büchi automaton. In such an automaton, the set of states can be partitioned into two subsets: one subset forms a deterministic automaton and also contains all the accepting states.

In formal verification, finite state model checking needs to find a Büchi automaton (BA) equivalent to a given linear temporal logic (LTL) formula, i.e., such that the LTL formula and the BA recognize the same ω-language. There are algorithms that translate an LTL formula to a BA. This transformation is normally done in two steps. The first step produces a generalized Büchi automaton (GBA) from a LTL formula. The second step translates this GBA into a BA, which involves a relatively easy construction. Since LTL is strictly less expressive than BA, the reverse construction is not always possible.

Inquisitive semantics is a framework in logic and natural language semantics. In inquisitive semantics, the semantic content of a sentence captures both the information that the sentence conveys and the issue that it raises. The framework provides a foundation for the linguistic analysis of statements and questions. It was originally developed by Ivano Ciardelli, Jeroen Groenendijk, Salvador Mascarenhas, and Floris Roelofsen.

In model checking, a branch of computer science, linear time properties are used to describe requirements of a model of a computer system. Example properties include "the vending machine does not dispense a drink until money has been entered" or "the computer program eventually terminates". Fairness properties can be used to rule out unrealistic paths of a model. For instance, in a model of two traffic lights, the liveness property "both traffic lights are green infinitely often" may only be true under the unconditional fairness constraint "each traffic light changes colour infinitely often".

Counterexample-guided abstraction refinement (CEGAR) is a technique for symbolic model checking. It is also applied in modal logic tableau calculi algorithms to optimise their efficiency.

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.
↑ Clarke, Edmund M. Jr; Grumberg, Orna; Peled, Doron (December 1999). Model Checking. Cyber Physical Systems Series. MIT Press. p. 14. ISBN 978-0-262-03270-4.
↑ 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

This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.

[1] Kripke, Saul, 1963, "Semantical Considerations on Modal Logic," Acta Philosophica Fennica, 16: 83-94

[2] 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.

[Clarke1999-3] Clarke, Edmund M. Jr; Grumberg, Orna; Peled, Doron (December 1999). Model Checking. Cyber Physical Systems Series. MIT Press. p. 14. ISBN 978-0-262-03270-4.

[Schneider2004-4] Klaus Schneider (2004). Verification of reactive systems: formal methods and algorithms. Springer. p. 45. ISBN 978-3-540-00296-3.

[BaierKatoen2008-5] 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.

[6] Clarke et al. p. 98

[1]

[2]

[3]

[4]

[5]

[6]