Component graphs as macro-dynamics

Traps

Component graphs are usually built by splitting the set of reachable states with respect to properties. Depending on the properties, we cannot guaranty that the paths exhibited in a component graph are all feasible. Indeed, a path \(C_1 \stackrel{a_1}{\longrightarrow} C_2 \stackrel{a_2}{\longrightarrow} C_3\) only means that some states of \(C_1\) lead to \(C_2\) and some states of \(C_2\) lead to \(C_3\). But it may occur that the entries of \(C_2\) reachable from \(C_1\) through \(a_1\) do not allow to reach the exits of \(C_2\) from which \(C_3\) can be reached through \(a_2\). In this case, we say that \(C_2\) has a trap: entering \(C_2\) through \(a_1\) from \(C_1\) is a trap because it does not guarantee that every exit can be reached, and thus the path through this edge \(C_1 \stackrel{a_1}{\longrightarrow} C_2\) does not allow to continue the path to \(C_3\) because this exit is actually not reachable from this entry. More precisely, every edge \(t\) towards a component \(C\) defines the subset \(C_t \subseteq C\) of states reachable through \(t\). If \(C_t\) does not include all the exits of \(C\), then it is a trap.

ecco shows these traps in several ways:

• table nodes has a column traps that lists the components from which a trap exists
• table edges has a column trap that is Boolean True when an arc leads into a trap
• when component graphs are displayed, components with traps are labelled with symbol ⬖ and trap-edges are drawn as dotted lines

ecco also provides method untrap() to split a component into its traps so they appear separated and leave no ambiguity.

Macro-dynamics

A component graph is often regarded as a presentation of the main dynamics of a system, or its macro-dynamics. However, if some node has traps, this may be misleading as this macro-dynamics shows paths that cannot be realised. As long as only direct reachability from one component to another is considered, there is no problem: if a transition exists, reachability is guaranteed (in the “some-to-some” sense). But as soon as a sequence of transitions is considered, it cannot considered as a real dynamics if it goes through a trap-edge. More precisely, this path may exist but the component graph is not an evidence of this, and the path may not exist as well. However, when a path enters a trap-component through a non-trap-edge, it is guaranteed that every exit is reachable and traps on this component have been avoided.

So, reading a component graphs requires care, and traps should be considered closely before to draw any conclusion about the macro-dynamics.

Target states

One recurring question is whether some target states, characterized by a formula \(\phi\), are reachable. It is very simple to answer this question by splitting the set of reachable states, but then more questions arise:

• How the system reaches these states?
• Can reaching these states be delayed forever?
• Can the system avoid reaching them completely?
• Can the system repeatedly reach these states?
• Can the system loose the capability to reach them?

All these questions can be answered by systematic splits. Consider a CTL property \(\phi\) that characterises target states. We may split a state-space w.r.t. \(\phi\) and \(\mathrm{EF}\phi\). This will usually yield something like:

Assuming that \(\phi\) does not hold at the initial state (otherwise, we would known it is reachable without any split), but also that it is reachable (otherwise our questions are pointless), we have an initial component at the top where \(\phi\) does not hold but \(\mathrm{EF}\phi\) does. This initial component can reach two others:

• one where \(\phi\) holds, and possibly \(\mathrm{EF}\phi\) holds also (which is the case if \(\phi\) can be repeated)
• one where neither \(\phi\) nor \(\mathrm{EF}\phi\) hold

There can be no return from this latter component because it does not allow to reach \(\phi\) while the two others components do. Very often, the top-most component will be a trap, for instance if the initial state is not reachable from a state with \(\phi\). By splitting this trap, we would get something like:

The previous top-component has been split into its part that is not reachable again (still at the top), and its part that is reachable again from \(\phi\) (at the bottom). This is the only difference between these two components with respect to our two properties.

The analysis done here is quite generic as we took very few assumptions, so it may apply to many systems. The resulting components may contain SCCs or not, deadlocks or not, etc. Some components or edges may not exist, but no others should. Still, the global idea remains the same: two properties \(\phi\) and \(\mathrm{EF}\phi\) allow to build a component graphs that already says a lot about the dynamics of the system. In particular we can observe the actions that lead from one component to another, which includes those that make \(\phi\) not reachable again (to the right component), those that enable \(\phi\) (to the left component), and those that disable it temporarily (from the left to the bottom component).

Sequences

Another recurring question, is whether a sequence of properties is observable in a systems dynamics. Splitting the state space against these properties and searching the requested sequence in the component graph is okay as long as traps can be avoided.

A safer way to check a sequence of CTL properties \(\phi_1, \phi_2, \dots\) is to check whether \(\phi_1 \land \mathrm{EF}\phi_2\) holds on some states, because these are the states where \(\phi_1\) holds and from which \(\phi_2\) is reachable. But this does not guarantees that the reached states where \(\phi_2\) holds can then allow to reach \(\phi_3\). To do so, we should check \(\phi_1 \land \mathrm{EF}(\phi_2 \land \mathrm{EF} \phi_3)\). And so on with more properties.

In general, the full sequence may no hold, and it can be tedious to check which parts of such a sequence can be realised. Moreover, this method works with CTL properties, but not with functional properties (at least it cannot be directly translated as there is no equivalent to \(\mathrm{EF}\)). ecco provides method search() to help in this analysis. This is still rough around the edges but it shall be refined in the future.