State Space Exploration

Author: Wieger Wesselink

Graph Exploration

State space exploration is an instance of graph exploration. Consider a directed graph and take a node s_0. We assume there is a function successors that returns the successor nodes of a vertex. An abstract algorithm for exploring the graph starting from vertex s_0 is

Algorithm: Graph exploration

\begin{algorithmic}[1] \Procedure{ExploreGraph}{$s_0$} \State $todo := \{ s_0 \}$ \State $discovered := \{ s_0 \}$ \While{$todo \neq \emptyset$} \State $\textbf{choose}\ s \in todo$ \State $todo := todo \setminus \{s\}$ \State $discovered := discovered \cup \{s\}$ \For{$s' \in successors(s)$} \If{$s' \notin discovered$} \State $discovered := discovered \cup \{s' \}$ \State $todo := todo \cup \{ s' \}$ \EndIf \EndFor \EndWhile \EndProcedure \end{algorithmic}

Event points

There are many different applications of state space exploration. The Boost Graph Library [Siek02] uses a clever idea to separate such applications from the exploration itself. It is done by distinguishing event points in the algorithm that the user can respond to by means of callback functions. For our purposes we select the following events:

Table 74 Event points

\textsf{discover\_state}

is invoked when a state is encountered for the first time

\textsf{examine\_transition}

is invoked on every transition

\textsf{start\_state}

is invoked on a state right before its outgoing transitions are being explored

\textsf{finish\_state}

is invoked on a state after all of its outgoing transitions have been explored

The events are named in terms of states and transitions instead of vertices and edges, since this is closer to our application domain. The exploration algorithm with event points included looks like this:

Algorithm: Graph exploration with event points

\begin{algorithmic}[1] \Procedure{ExploreGraph}{$s_0, \textsf{discover\_state}, \textsf{examine\_transition}, \textsf{start\_state}, \textsf{finish\_state}$} \State $todo := \{ s_0 \}$ \State $discovered := \{ s_0 \}$ \State \colorbox{lightgray}{$\textsf{discover\_state}(s_0)$} \While{$todo \neq \emptyset$} \State $\textbf{choose}\ s \in todo$ \State $todo := todo \setminus \{s\}$ \State \colorbox{lightgray}{$\textsf{start\_state}(s)$} \State $discovered := discovered \cup \{s\}$ \For{$s' \in successors(s)$} \If{$s' \notin discovered$} \State $discovered := discovered \cup \{s' \}$ \State \colorbox{lightgray}{$\textsf{discover\_state}(s')$} \State $todo := todo \cup \{ s' \}$ \EndIf \State \colorbox{lightgray}{$\textsf{examine\_transition}(s, a, s')$} \EndFor \State \colorbox{lightgray}{$\textsf{finish\_state}(s)$} \EndWhile \EndProcedure \end{algorithmic}

Applications

Many applications can be easily expressed in terms of the given event points.

Deadlock checking

With deadlock checking we are looking for states that have no outgoing transitions. By introducing one boolean variable \textsf{has\_transitions} we can implement deadlock checking as follows. The callback functions are printed as comments in gray.

Algorithm: Deadlock checking implemented using event points

\begin{algorithmic}[1] \Procedure{FindDeadlock}{$s_0, \textsf{discover\_state}, \textsf{examine\_transition}, \textsf{start\_state}, \textsf{finish\_state}$} \State \Comment{\colorbox{lightgray}{bool has\_transitions}} \State $todo := \{ s_0 \}$ \State $discovered := \{ s_0 \}$ \State $\textsf{discover\_state}(s_0)$ \While{$todo \neq \emptyset$} \State $\textbf{choose}\ s \in todo$ \State $todo := todo \setminus \{s\}$ \State $\textsf{start\_state}(s)$ \Comment{\colorbox{lightgray}{has\_transitions := false}} \State $discovered := discovered \cup \{s\}$ \For{$s' \in successors(s)$} \If{$s' \notin discovered$} \State $discovered := discovered \cup \{s' \}$ \State $\textsf{discover\_state}(s')$ \State $todo := todo \cup \{ s' \}$ \EndIf \State $\textsf{examine\_transition}(s, a, s')$ \Comment{\colorbox{lightgray}{has\_transitions := true}} \EndFor \State $\textsf{finish\_state}(s)$ \Comment{\colorbox{lightgray}{if (!has\_transitions) report\_deadlock(s)}} \EndWhile \EndProcedure \end{algorithmic}

Search strategies

Exploration can be done with different search strategies. We describe three of them: breadth-first, depth-first and highway. They mainly differ in the order in which the elements of the todo set are processed. In breadth-first search nodes at the present depth are explored before nodes at a higher depth. In depth-first search the highest-depth nodes are explored first. Highway search is a variant that uses a breadth-first search, but it only explores a part of the state space.

In all three cases the todo list is stored in a double ended queue. We use the slicing operator to denote parts of a list. For example, A[m:n] corresponds to the sublist A[m, \ldots, n-1].

Cycle detection

For cycle detection the event points in Event points are insufficient. In [Siek02] the following recursive depth first algorithm is given:

Algorithm: Recursive cycle detection algorithm as specified in Boost

\begin{algorithmic}[1] \Procedure{boost\_dfs\_recursive}{$u$} \State $color[u] := gray$ \State $\textsf{discover\_vertex}(u)$ \For{$(a,v) \in out\_edges(u)$} \State $\textsf{examine\_edge}(a, v)$ \If{$color[v] = white$} \State $\textsf{tree\_edge}(a, v)$ \State \Call{dfs\_recursive}{$v$} \ElsIf{$color[v] = gray$} \State $\textsf{back\_edge}(a, v)$ \Else \State $\textsf{forward\_or\_cross\_edge}(a, v)$ \EndIf \State $color[u] := black$ \State $\textsf{finish\_vertex}(u)$ \EndFor \EndProcedure \end{algorithmic}

The code in Boost uses an iterative version:

Algorithm: Iterative cycle detection algorithm as implemented in Boost

\begin{algorithmic}[1] \Procedure{boost\_dfs\_iterative}{$u$} \State $color[u] := gray$ \State $\textsf{discover\_vertex}(u)$ \State $stack := [(u, out\_edges(u))]$ \While{$|stack| > 0$} \State $u, E := stack.pop\_back()$ \While{$|E| > 0$} \State $a, v := E[0]$ \State $\textsf{examine\_edge}(u, a, v)$ \If{$color[v] = white$} \State $\textsf{tree\_edge}(u, a, v)$ \State $stack.push\_back(u, E[1:])$ \State $u := v$ \State $color[u] := gray$ \State $\textsf{discover\_vertex}(u)$ \State $E := out\_edges(u)$ \Else \If{$color[v] = gray$} \State $\textsf{back\_edge}(u, a, v)$ \Else \State $\textsf{forward\_or\_cross\_edge}(u, a, v)$ \EndIf \State $E := E[1:]$ \EndIf \EndWhile \State $color[u] := black$ \State $\textsf{finish\_vertex}(u)$ \EndWhile \EndProcedure \end{algorithmic}

For our purposes we rewrite this as:

Algorithm: Recursive cycle detection

\begin{algorithmic}[1] \Procedure{dfs\_recursive}{$s_0, gray$} \State $gray := gray \cup \{ s_0 \}$ \State $discovered := \{ s_0 \}$ \State $\textsf{discover\_state}(s_0)$ \For{$(a, s_1) \in out\_edges(s_0)$} \State $\textsf{examine\_edge}(s_0, a, s_1)$ \If{$s_1 \notin discovered$} \State $\textsf{tree\_edge}(s_0, a, s_1)$ \State $discovered := discovered \cup \{ s_1 \}$ \State \Call{dfs\_recursive}{$s_1, gray$} \ElsIf{$s_1 \in todo$} \State $\textsf{back\_edge}(s_0, a, s_1)$ \Else \State $\textsf{forward\_or\_cross\_edge}(s_0, a, s_1)$ \EndIf \State $gray := gray \setminus \{ s_0 \}$ \State $\textsf{finish\_state}(s_0)$ \EndFor \EndProcedure \end{algorithmic}

Algorithm: Iterative cycle detection

\begin{algorithmic}[1] \Procedure{dfs\_iterative}{$s_0$} \State $todo := [(s_0, out\_edges(s_0))]$ \State $discovered := \{ s_0 \}$ \State $\textsf{discover\_state}(s_0)$ \While{$|todo| > 0$} \State $s, E := todo.back()$ \While{$|E| > 0$} \State $a, s_1 := E.pop\_front()$ \State $\textsf{examine\_edge}(s_0, a, s_1)$ \If{$s_1 \notin discovered$} \State $\textsf{tree\_edge}(s_0, a, s_1)$ \State $discovered := discovered \cup \{ s_1 \}$ \State $\textsf{discover\_state}(s_1)$ \State $todo.back() := (s, E)$ \State $todo := todo \concat [(s_1, out\_edges(s_1))]$ \State $s, E := todo.back()$ \ElsIf{$s_1 \in todo$} \State $\textsf{back\_edge}(s_0, a, s_1)$ \Else \State $\textsf{forward\_or\_cross\_edge}(s_0, a, s_1)$ \EndIf \EndWhile \State $\textsf{finish\_state}(s)$ \EndWhile \EndProcedure \end{algorithmic}

Whenever the \textsf{back\_edge} event is triggered, a cycle is found.

Untimed state space exploration

Consider the following untimed linear process specification P, with initial state d_0.

\begin{array}{l} P(d)= \sum\limits_{i\in I}\sum\limits_{e_i}c_i(d, e_i)\rightarrow a_i(f_i(d,e_i)) \cdot P(g_i(d,e_i)) \end{array}

This linear process is a symbolic representation of a state space, or labeled transition system (LTS). The previously described graph exploration algorithms can be applied to explore a state space. Let rewr be a rewriter. An algorithm for untimed state space exploration is

Algorithm: Untimed LPS exploration

\begin{algorithmic}[1] \Procedure{ExploreLPS}{$P(d), d_0, rewr, \textsf{discover\_state}, \textsf{examine\_transition}, \textsf{start\_state}, \textsf{finish\_state}$} \State $s_0 := rewr(d_0, \emptylist)$ \State $todo := \{ s_0 \}$ \State $discovered := \{ s_0 \}$ \State $\textsf{discover\_state}(s_0)$ \While{$todo \neq \emptyset$} \State $\textbf{choose}\ s \in todo$ \State $todo := todo \setminus \{s\}$ \State $discovered := discovered \cup \{s\}$ \State $\textsf{start\_state}(s)$ \For{$i \in I$} \State $condition := rewr(c_i(d, e_i), [d := s])$ \If{$condition = false$} \State \textbf{continue} \EndIf \State $E := \{ e \mid rewr(condition, [e_i := e]) = true \}$ \For{$e \in E$} \State $a := a_i(rewr(f_i(d,e_i), [d:=s,e_i:=e]))$ \State $s' := rewr(g_i(d,e_i), [d:=s,e_i:=e])$ \If{$s' \notin discovered$} \State $todo := todo \cup \{ s' \}$ \State $discovered := discovered \cup \{s'\}$ \State $\textsf{discover\_state}(s')$ \EndIf \State $\textsf{examine\_transition}(s, a, s')$ \EndFor \EndFor \State $\textsf{finish\_state}(s)$ \EndWhile \EndProcedure \end{algorithmic}

The set E is computed using the Enumerate algorithm. This computation may be expensive. Hence the condition c(d,e_i) is first rewritten, since if it evaluates to false the computation of E can be skipped.

Timed state space exploration

Consider the following timed linear process specification P, with initial state d_0.

\begin{array}{l} P(d)= \sum\limits_{i\in I}\sum\limits_{e_i}c_i(d, e_i)\rightarrow a_i(f_i(d,e_i)) \mbox{\colorbox{lightgray}{$\at{t_i(d,e_i)}$}} \cdot P(g_i(d,e_i)). \end{array}

Note that the time tag t_i(d,e_i) is optional. If it is omitted, the corresponding action may happen at an arbitrary time. In timed state space exploration, care is taken that on every trace the time tags are increasing. In order to achieve that, a time stamp is recorded for each state in the state space. We use the notation t \aftertime s to denote the state s with associated time stamp t. An algorithm for timed state space exploration is

Algorithm: Timed LPS exploration

\begin{algorithmic}[1] \Procedure{ExploreLPSTimed}{$P(d), d_0, rewr, \textsf{discover\_state}, \textsf{examine\_transition}, \textsf{start\_state}, \textsf{finish\_state}$} \State $s_0 := rewr(d_0, \emptylist)$ \State $todo := \{ \hlmath{0 \aftertime s_0} \}$ \State $discovered := \{ \hlmath{0 \aftertime s_0} \}$ \State $\textsf{discover\_state}(0 \aftertime s_0)$ \While{$todo \neq \emptyset$} \State $\textbf{choose}\ \hlmath{t \aftertime s} \in todo$ \State $todo := todo \setminus \{ \hlmath{t \aftertime s} \}$ \State $discovered := discovered \cup \{ \hlmath{t \aftertime s} \}$ \State $\textsf{start\_state}(t \aftertime s)$ \For{$i \in I$} \State $condition := rewr(c_i(d, e_i), [d := s])$ \If{$condition = false$} \State \textbf{continue} \EndIf \State $E := \{ e \mid rewr(condition, [e_i := e]) = true \}$ \For{$e \in E$} \State \colorbox{lightgray}{$t' := rewr(t_i(d,e_i), [d:=s,e_i:=e])$} \If{$\hlmath{t' \leq t}$} \State \textbf{continue} \EndIf \State $a := a_i(rewr(f_i(d,e_i), [d:=s,e_i:=e]))$ \State $s' := rewr(g_i(d,e_i), [d:=s,e_i:=e])$ \If{$\hlmath{t' \aftertime s'} \notin discovered$} \State $todo := todo \cup \{ \hlmath{t' \aftertime s'} \}$ \State $discovered := discovered \cup \{ \hlmath{t' \aftertime s'} \}$ \State $\textsf{discover\_state}(t' \aftertime s')$ \EndIf \State $\textsf{examine\_transition}(t \aftertime s, a\at{t'}, t' \aftertime s')$ \EndFor \EndFor \State $\textsf{finish\_state}(t \aftertime s)$ \EndWhile \EndProcedure \end{algorithmic}

Stochastic state space exploration

Consider the following stochastic linear process specification P, with initial state \frac{p(h)}{h} \cdot P(g(h)).

\begin{array}{l} P(d)= \sum\limits_{i\in I}\sum\limits_{e_i}c_i(d, e_i)\rightarrow a_i(f_i(d,e_i)) \mbox{\colorbox{lightgray}{$\dfrac{p_i(d,e_i,h_i)}{h_i}$}} \cdot P(g_i(d,e_i,h_i)), \end{array}

where p and p_i are stochastic distributions. We define a stochastic state as a set \{(q_1, s_1), \ldots, (q_m, s_m)\} with q_j,\ j = 1 \ldots m a sequence of non-zero probabilities that sum up to 1, and s_j,\ j = 1 \ldots m a sequence of states. The function \textsc{ComputeStochasticState} is used to compute a stochastic state from its symbolic representation.

Algorithm: Computation of a stochastic state

\begin{algorithmic}[1] \Procedure{ComputeStochasticState}{$h, p, g, rewr, \sigma$} \State $result := \emptyset$ \State $H := \{ (h',q) \mid q = rewr(p, \sigma[h := h']) \wedge q > 0 \}$ \For{$(h', q) \in H$} \State $s := rewr(g, \sigma[h := h'])$ \State $result := result \cup \{ (q, s) \}$ \EndFor \State \Return $result$ \EndProcedure \end{algorithmic}

The set H is computed using the Enumerate algorithm.

An algorithm for stochastic state space exploration is

Algorithm: Stochastic LPS exploration

\begin{algorithmic}[1] \Procedure{ExploreLPSStochastic}{$P(d), \frac{p(h)}{h} \cdot P(g(h)), rewr, \textsf{discover\_state}, \textsf{examine\_transition}, \textsf{start\_state}, \textsf{finish\_state}, \textsf{discover\_initial\_state}$} \State \colorbox{lightgray}{$\hat{s_0} := \textsc{ComputeStochasticState}(h, p(h), g(h), rewr, \emptylist)$} \State \colorbox{lightgray}{$S := \{ s_i \mid (q_i, s_i) \in \hat{s_0} \}$} \State \colorbox{lightgray}{$\textsf{discover\_initial\_state}(\hat{s_0})$} \For{\colorbox{lightgray}{$s \in S$}} \State $todo := todo \cup \{ s \}$ \State $discovered := discovered \cup \{ s \}$ \State $\textsf{discover\_state}(s)$ \EndFor \While{$todo \neq \emptyset$} \State $\textbf{choose}\ s \in todo$ \State $todo := todo \setminus \{s\}$ \State $discovered := discovered \cup \{s\}$ \State $\textsf{start\_state}(s)$ \For{$i \in I$} \State $condition := rewr(c_i(d, e_i), [d := s])$ \If{$condition = false$} \State \textbf{continue} \EndIf \State $E := \{ e \mid rewr(condition, [e_i := e]) = true \}$ \For{$e \in E$} \State $a := a_i(rewr(f_i(d,e_i), [d:=s,e_i:=e]))$ \State \colorbox{lightgray}{$\hat{s'} := \textsc{ComputeStochasticState}(h_i, p_i(d,e_i,h_i), g_i(d,e_i,h_i), rewr, [d:=s, e_i:=e])$} \State \colorbox{lightgray}{$S' := \{ s_i \mid (q_i, s_i) \in \hat{s'} \}$} \For{\colorbox{lightgray}{$s' \in S'$}} \If{$s' \notin discovered$} \State $todo := todo \cup \{ s' \}$ \State $discovered := discovered \cup \{s'\}$ \State $\textsf{discover\_state}(s')$ \EndIf \EndFor \State $\textsf{examine\_transition}(s, a,$ \colorbox{lightgray}{$\hat{s'}$}$)$ \EndFor \EndFor \State $\textsf{finish\_state}(s)$ \EndWhile \EndProcedure \end{algorithmic}

Caching

The computation of the set of solutions E in \textsc{ExploreLPS} is expensive. Therefore it may be a good idea to cache these solutions. Caching can be done locally (i.e. using a separate cache for each summand), or globally. This leads to the following variants of the algorithm. We assume that FV is a function that computes free variables of an expression. Let \mathcal{D} be the set of process parameters (i.e. the elements of d).

Local caching

In the local caching algorithm for each summand i a mapping C_i is maintained. The cache key is comprised of the actual values of the process parameters that appear in the condition c_i(d, e_i).

Algorithm: LPS exploration with local caching

\begin{algorithmic}[1] \Procedure{ExploreLPSLocallyCached}{$P(d), d_0, rewr, \textsf{discover\_state}, \textsf{examine\_transition}, \textsf{start\_state}, \textsf{finish\_state}$} \State $s_0 := rewr(d_0, \emptylist)$ \State $todo := \{ s_0 \}$ \State $discovered := \{ s_0 \}$ \State $\textsf{discover\_state}(s_0)$ \For{\colorbox{lightgray}{$i \in I$}} \State \colorbox{lightgray}{$C_i := \emptymap$} \State \colorbox{lightgray}{$\gamma_i := FV(c_i(d, e_i)) \cap \mathcal{D}$} \EndFor \While{$todo \neq \emptyset$} \State $\textbf{choose}\ s \in todo$ \State $todo := todo \setminus \{s\}$ \State $discovered := discovered \cup \{s\}$ \State $\textsf{start\_state}(s)$ \For{$i \in I$} \State \colorbox{lightgray}{$key := \gamma_i[d:=s]$} \If{\colorbox{lightgray}{$key \in keys(C_i)$}} \State \colorbox{lightgray}{$E := C_i[key]$} \Else \State \colorbox{lightgray}{$E := \{ e \mid rewr(c_i(d, e_i), [d:=s,e_i:=e]) = true \}$} \State \colorbox{lightgray}{$C_i := C_i \cup \{(key, E)\}$} \EndIf \For{$e \in E$} \State $a := a_i(rewr(f_i(d,e_i), [d:=s,e_i:=e]))$ \State $s' := rewr(g_i(d,e_i), [d:=s,e_i:=e])$ \If{$s' \notin discovered$} \State $todo := todo \cup \{ s' \}$ \State $discovered := discovered \cup \{s'\}$ \State $\textsf{discover\_state}(s')$ \EndIf \State $\textsf{examine\_transition}(s, a, s')$ \EndFor \EndFor \State $\textsf{finish\_state}(s)$ \EndWhile \EndProcedure \end{algorithmic}

Global caching

In the global caching algorithm one mapping C is maintained. To achieve this, the condition of the summands is added to the cache key. If many summands share the same condition, global caching may be beneficial. In practice this doesn’t seem to happen much.

Algorithm: LPS exploration with global caching

\begin{algorithmic}[1] \Procedure{ExploreLPSGloballyCached}{$P(d), d_0, rewr, \textsf{discover\_state}, \textsf{examine\_transition}, \textsf{start\_state}, \textsf{finish\_state}$} \State $todo := \{d_0\}$ \State $discovered := \emptyset$ \State \colorbox{lightgray}{$C := \emptyset$} \For{\colorbox{lightgray}{$i \in I$}} \State \colorbox{lightgray}{$\gamma_i := FV(c_i(d, e_i)) \cap \mathcal{D}$} \EndFor \While{$todo \neq \emptyset$} \State $\textbf{choose}\ s \in todo$ \State $todo := todo \setminus \{s\}$ \State $discovered := discovered \cup \{s\}$ \State $\textsf{start\_state}(s)$ \For{$i \in I$} \State \colorbox{lightgray}{$key := c_i(d,e_i) \concat \gamma_i[d:=s]$} \If{\colorbox{lightgray}{$key \in keys(C)$}} \State \colorbox{lightgray}{$T := C[key]$} \Else \State \colorbox{lightgray}{$T := \{ t \mid rewr(c_i(d, e_i), [d:=s,e_i:=t]) = true \}$} \State \colorbox{lightgray}{$C := C \cup \{(key, T)\}$} \EndIf \For{$e \in E$} \State $a := a_i(rewr(f_i(d,e_i), [d:=s,e_i:=e]))$ \State $s' := rewr(g_i(d,e_i), [d:=s,e_i:=e])$ \If{$s' \notin discovered$} \State $todo := todo \cup \{ s' \}$ \State $discovered := discovered \cup \{s'\}$ \State $\textsf{discover\_state}(s')$ \EndIf \State $\textsf{examine\_transition}(s, a, s')$ \EndFor \EndFor \State $\textsf{finish\_state}(s)$ \EndWhile \EndProcedure \end{algorithmic}

In this algorithm C is a mapping, with keys(C) = \{ k \mid \exists_{v}: (k,v) \in C \}. We use the notation C[k] to denote the unique element v such that (k,v) \in C.

Confluence Reduction

Confluence reduction (see [GP00], [Blo01] and [BP02]) is an on-the-fly state space exploration method that produces a reduced state space. For confluence reduction we assume that the set of summands I is partitioned into a set I_{regular} of ‘regular’ summands, and a set I_{confluent} of confluent \tau-summands. The confluent \tau-summands are used to determine a unique representative state that is reachable via confluent \tau steps. This is done using the graph algorithm \textsc{FindRepresentative}. This leads to the following variant of the algorithm:

Algorithm: LPS exploration with confluence reduction

\begin{algorithmic}[1] \Procedure{ExploreLPSConfluence}{$P(d), d_0, rewr, \textsf{discover\_state}, \textsf{examine\_transition}, \textsf{start\_state}, \textsf{finish\_state}$} \State $s_0 := \hlmath{\textsc{FindRepresentative}(rewr(d_0, \emptylist))}$ \State $todo := \{ s_0 \}$ \State $discovered := \{ s_0 \}$ \State $\textsf{discover\_state}(s_0)$ \While{$todo \neq \emptyset$} \State $\textbf{choose}\ s \in todo$ \State $todo := todo \setminus \{s\}$ \State $discovered := discovered \cup \{s\}$ \State $\textsf{start\_state}(s)$ \For{$i \in \hlmath{I_{regular}}$} \State $condition := rewr(c_i(d, e_i), [d := s])$ \If{$condition = false$} \State \textbf{continue} \EndIf \State $E := \{ e \mid rewr(condition, [e_i := e]) = true \}$ \For{$e \in E$} \State $a := a_i(rewr(f_i(d,e_i), [d:=s,e_i:=e]))$ \State $s' := \hlmath{\textsc{FindRepresentative}(rewr(g_i(d,e_i), [d:=s,e_i:=e]))}$ \If{$s' \notin discovered$} \State $todo := todo \cup \{ s' \}$ \State $discovered := discovered \cup \{s'\}$ \State $\textsf{discover\_state}(s')$ \EndIf \State $\textsf{examine\_transition}(s, a, s')$ \EndFor \EndFor \State $\textsf{finish\_state}(s)$ \EndWhile \EndProcedure \end{algorithmic}

As suggested in [BP02] Tarjan’s strongly connected component (SCC) algorithm (see [Tar72]) can be used to compute a unique representative.

Tarjan’s SCC algorithm

A recursive implementation of Tarjan’s strongly connected components algorithm that uses four global variables stack, low, disc and result. The helper function \textsc{StrongConnect} computes the connected component reachable from node u. In this function it is assumed that the function call \textsf{successors}(u) returns the successor states of u in a deterministic order.

Algorithm: Tarjan’s Strongly Connected Component Algorithm

Input: G=(V,E): A graph with nodes V and edges E.

Output: result: A sequence containing all strongly connected components of the graph.

\begin{algorithmic}[1] \Procedure{Tarjan}{$G$} \State $stack := \emptylist$ \State $low := \emptymap$ \Comment{the empty mapping is denoted as $\emptymap$} \State $disc := \emptymap$ \Comment{$u \in low$ means $u$ is a key of mapping $low$} \State $result := \emptylist$ \For{$u \in V$} \If{$u \notin low$} \State \Call{StrongConnect}{$u$} \EndIf \EndFor \State \Return $result$ \EndProcedure \end{algorithmic}

Algorithm: Helper function StrongConnect

Input: u: An element of V.

\begin{algorithmic}[1] \Procedure{StrongConnect}{$u$} \State $k := |disc|$ \Comment{$k$ is the discovery time assigned to node $u$} \State $disc[u] := k$ \State $low[u] := k$ \Comment{initially $low[u] = disc[u]$} \State $stack := stack \concat [u]$ \For{$v \in \textsf{successors}(u)$} \If{$v \notin low$} \State \Call{StrongConnect}{$v$} \State $low[u] := \textsf{min}(low[u], low[v])$ \ElsIf{$v \in stack$} \State $low[u] := \textsf{min}(low[u], disc[v])$ \EndIf \EndFor \If{$low[u] = disc[u]$} \Comment{an SCC has been found} \State $comp := \emptylist$ \While{\textbf{true}} \State $v := stack[|stack| - 1]$ \Comment{assign the top of the stack to $v$} \State $stack := stack[0:|stack| - 1]$ \Comment{pop an element from the stack} \State $comp := comp \concat [v]$ \If{$v = u$} \State \textbf{break} \EndIf \EndWhile \State $result := result \concat [comp]$ \EndIf \EndProcedure \end{algorithmic}

A side effect of a call \textsc{Tarjan}(u) is that result contains the connected components that have been found.

FindRepresentative

Due to properties of confluent \tau-summands, there is always only one terminal strongly connected component, i.e. a strongly connected component without outgoing edges. Furthermore, the first strongly connected component reported by Tarjan’s algorithm is always terminating. For our implementation of \textsc{FindRepresentative} we prefer to use an iterative version of Tarjan’s SCC algorithm. The reason for this is that an iterative version can be more easily interrupted once the first SCC has been found. The algorithm description in [Oqv] has been used as a model for our solution.

Algorithm: Find a unique representative node in a graph

\begin{algorithmic}[1] \Procedure{FindRepresentative}{$u$} \State $stack := \emptylist$ \State $low := \emptymap$ \State $disc := \emptymap$ \State $work := [(u, 0)]$ \While{$work \neq \emptylist$} \State $(u, i) := work[|work| - 1]$ \State $work := work[0 : |work| - 1]$ \If{$i = 0$} \State $k := |disc|$ \State $disc[u] := k$ \State $low[u] := k$ \State $stack := stack \concat [u]$ \EndIf \State $recurse := false$ \For{$j \in [i, \ldots, |successors(u)|]$} \State $v := successors(u)[j]$ \If{$v \notin disc$} \State $work := work \concat [(u, j+1)]$ \State $work := work \concat [(v, 0)]$ \State $recurse := true$ \State \textbf{break} \ElsIf{$v \in stack$} \State $low[u] := min(low[u], disc[v])$ \EndIf \EndFor \If{$recurse$} \State \textbf{continue} \EndIf \If{$low[u] = disc[u]$} \State $result := u$ \While{\textbf{true}} \State $v := stack[|stack| - 1]$ \State $stack := stack[0:|stack| - 1]$ \If{$v = u$} \State \textbf{break} \EndIf \If{$v < result$} \State $result := v$ \EndIf \EndWhile \State \Return $result$ \EndIf \If{$work \neq \emptylist$} \State $v := u$ \State $(u, z) := work[|work| - 1]$ \State $low[u] := min(low[u], low[v])$ \EndIf \EndWhile \EndProcedure \end{algorithmic}

References

[Siek02] (1,2)

Jeremy Siek, Lie-Quan Lee and Andrew Lumsdale. The Boost Graph Library: User Guide and Reference Manual. Addison-Wesley, 2002.

[EGWW09] (1,2)

Tom A. N. Engels, Jan Friso Groote, Muck van Weerdenburg and Tim A. C. Willemse. Search algorithms for automated validation. Journal of Logic and Algebraic Programming, 78(4):274–287, 2009.

[GP00]

Jan Friso Groote and Jaco van de Pol. State Space Reduction Using Partial tau-Confluence. In MFCS, LNCS 1893, pages 383–393. Springer, 2000.

[Blo01]

Stefan Blom. Partial t-confluence for Efficient State Space Generation, 2001.

[BP02] (1,2)

Stefan Blom and Jaco van de Pol. State Space Reduction by Proving Confluence. In CAV, LNCS 2404, pages 596–609. Springer, 2002.

[Tar72]

Robert Tarjan. Depth first search and linear graph algorithms. SIAM Journal on Computing, 1(2), 1972.

[Oqv]

Jesper Öqvist. Iterative Tarjan Strongly Connected Components in Python. https://llbit.se/?p=3379. Accessed 2019-03-26.