Module ReachabilityTree


module ReachabilityTree: sig .. end
Reachability Trees.

This module provides an implementation for abstract reachability trees. Such trees are at the core of lazy abstraction refinement approaches (some references are given below). The functor implemented in this module takes as arguments a model (see the Model module) and a printable type of marks.

A reachability tree is a directed rooted tree where each vertex is labeled by a location and by a region, and each edge is labeled by a transition of the model's automaton. As an exception to the latter rule, the edges from the root to its children are labeled by initial regions. Labels of edges remain constant after creation, and the same applies to vertex locations. However, the regions labeling vertices may evolve, typically due to refinement.

The root of a reachability tree is a virtual vertex, that, essentially, binds the subtrees associated with each initial symbolic state into a single tree. In particular, the root has no associated location nor region. In the following, all considered vertices are distinct from the root (i.e., the root is not a vertex).

To be useful, a reachability tree usually must respect some “correctness” conditions, such as:

  • for every edge (u, v) labeled by a transition t, the location of u is the source of t, the location of v is the target of t, and the region of v contains the post image of the region of u w.r.t. the command of t.
  • for each vertex u that is not a leaf (i.e., u has a child), there exists, for each transition t with source equal to the location of u, a child v of u such that the edge (u, v) is labeled by t.

Remark. This module does not enforce any “correctness” condition on the reachability trees.

Termination of tree-based algorithms often rely on cover properties. To this end, a covering relation is associated to each tree. More details are given below regarding covering relations. In addition, vertices are decored with additional attributes that are typically needed by tree-based model-checking algorithms.


See also



Covering Relations

The vertex covering information is given by a relation, written ◅, that is interpreted as follows: v ◅ w means “v is covered by w” or, equivalently, “w covers v”.

A pair (v, w) in ◅ is called a covering pair. When v ◅ w, we say that v is a coveree of w, and that w is a coverer of v. A vertex v is called covered when it has a coverer (i.e., there exists w such that v ◅ w).

In the reachability tree constructed by a model-checking algorithm, vertices that are covered should be “discarded”, and in particular they should not be expanded (since their descendants shall be explored from their coverers). However, due to refinement, a vertex may become covered after expansion of (part of) its subtree. In such a case, descendants of the covered vertex should, essentially, inherit this coveredness. To prevent confusion between direct covering and inherited covering, a different term is used here for the inherited version.

Recall that an ancestor of a vertex u is any vertex on the branch from the root to u (in particular, u is an ancestor of u). Given a vertex u, the subtree rooted in u contains all vertices for which u is an ancestor.

A vertex u is called active when none of its ancestors is covered. Conversely, u is called inactive when it has an ancestor that is covered. Observe that the set of active vertices forms a prefix of the tree.

All of the above only introduced vocabulary associated with a given covering relation, which is, a priori, an arbitrary binary relation over vertices. But as for reachability trees, to be useful, a covering relation usually must respect some “correctness” conditions, such as:

  • if v ◅ w, then v and w have the same location, and the region of v is contained in the region of w.
  • if u is an ancestor of v, then u cannot be covered by v.
  • if w covers some vertex, then w is active.

Remark. This module does not enforce any “correctness” condition on the covering relations.

module Make: 
functor (A : Model.S) ->
functor (Mark : Util.Print.PRINTABLE_TYPE) -> sig .. end