Reactive Systems

Reactive systems are systems that interact with their environment and evolve over an infinite time horizon. This chapter presents a natural model for them: Kripke structure.

Directed Graphs

A directed graph, or graph, is pair \((V,E)\) where:

  • \(V\) is a finite set of nodes
  • \(E \subseteq V \times V\) is a set of edges

If \((s,d) \in E\), then \(s\) and \(d\) are the source and the destination of \((s,d)\), respectively. The edge \((s,d) \in E\) is said to go from :math:`s` to :math:`d`. If \(e \in E\) goes either from \(s\) to \(d\) or from \(d\) to \(s\), then \(e\) is an edge between \(d\) and \(s\). By extension, an edge \(e \in E\) goes from \(V_1 \subseteq S\) to \(V_2 \subseteq S\) if there exists a pair of nodes \((v_1,v_2) \in V_1 \times V_2\) such that \((v_1,v_2) \in E\). Analogously, \(e \in E\) is between \(V_1\) and \(V_2\) if it is either from \(V_1\) to \(V_2\) or from \(V_2\) to \(V_1\).

The reversed graph of a graph \((V,E)\) is the graph \((V,E')\) where \(E'={(d,s) | (s,d) \in E}\).

A subgraph of a graph \((V,E)\) is a graph \((V',E')\) such that \(V' \subseteq V\) and \(E' \subseteq E \cap (V' \times V')\). A subgraph \((V',E')\) of \((V,E)\) is a proper subgraph if either \(V'\subsetneq V\) or \(E'\subsetneq E\). A subgraph \(G\) of \((V,E)\) respects a set of nodes \(V' \subseteq V\) if \(G=(V',E \cap (V' \times V'))\).

A sequence, either finite or infinite, \(\pi=v_0 v_1 \ldots\) is a path for the graph \((V,E)\) if \((v_i,v_{i+1}) \in E\) for all \(v_i\) and \(v_{i+1}\) in \(\pi\). The lenght of a path \(\pi\), denoted by \(|\pi|\), is the size of the sequence.

It is easy to see that if \(\pi=v_0 \ldots v_n\) and \(\pi'=w_0 \ldots\) are two paths for \((V,E)\) such that \((v_n,w_0) \in E\), then \(\pi\cdot\pi'=v_0 \ldots v_n w_0 \ldots\) is path for \((V,E)\).

Let \(\pi\), \(\pi'\), and \(\pi''\) be three paths such that \(\pi=\pi'\cdot\pi''\). Then, \(\pi'\) is a prefix of \(\pi\) and \(\pi''\) is a suffix of \(\pi\). We write \(\pi_i\) to denote the suffix of \(\pi\) for which \(\pi=\pi' \cdot \pi_i\) and \(|\pi'|=i\) for some \(\pi'\).

If \(v_0 v_1 \ldots v_n\) is a prefix for some path \(\pi\) of a graph \((V,E)\), then we say that either \(\pi\) starts from \(v_0\) and reaches \(v_n\) or, equivantely, \(v_n\) is reachable from \(v_0\) in \((V,E)\).

Every subgraph \((V',E')\) of \(G\) such that:

  1. \(v\) is reachable from \(v'\) for all pairs \(v,v' \in V'\) and
  2. is not proper subgraph of any subgraph of \(G\) that satisfies 1.

is a strongly connected component of \(G\). It is easy to see that the the sets of nodes of each strongly connected component of a graph \((V,E)\) is a partition of \(V\). A strongly connected component \((V',E')\) is trivial if \(|V'|=1\) and \(|E'|=0\).

Directed Acyclic Graphs and Trees

A directed acyclic graph or DAG is a directed graph whose strongly connected components are all trivial.

A graph \((V,E)\) is disconnected if there exists a \(V' \subseteq V\) such that there are no edges between \(V'\) and \(V\setminus V'\). If a graph is not disconnected, then is connected.

A directed tree is a connected DAG \((V,E)\) whose subgraphs of the form \((V,E')\), where \(E' \subsetneq E\), are disconnected.

Kripke Structures

A Kripke structure is a directed graph, equipped with a set of initial nodes, such that every node is source of some edge and it is labeled by a set of atomic propositions [CGP00]. The nodes of Kripke structure are called states.

A Kripke structure is a tuple \((S,S_0,R,L)\) such that:

  • \(S\) is a finite set of states
  • \(S_0\subseteq S\) is a set of initial states
  • \(R\subseteq S\times S\) is a set of transitions such that for all \(s \in S\) there exists a \((s,s') \in R\) for some \(s' \in S\)
  • \(L:S \rightarrow 2^{AP}\) maps each state into a set of atomic propositions

Sometime, the set of initial states is omitted. In such cases, \(S\) and \(S_0\) coincide.

A computation of a Kripke structure \((S,S_0,R,L)\) is an infinite path of \((S,R)\) that starts from some \(s \in S_0\).