Directed Model Checking
Mcta [5],[6] accelerates the detection of error states by using the directed model checking approach. Directed model checking is a technique that is tailored to fast detection of system states that violate a given safety property. This is achieved by influencing the order in which states are explored during the state space traversal. The order is typically determined by an abstract distance function h that estimates a state's distance to a nearest error state. There are many different strategies to explore the state space. Among others, Mcta allows the user to choose between two strategies based on two wide-spread search methods namely A* and greedy search. The first explores states s with lowest value of c(s) + h(s) first, where c(s) is the length of the path from the initial state through which s was reached. Under certain conditions on the abstract distance values, one is guaranteed a shortest error path. In the second strategy, states are explored by increasing value of h(s). Doing so, the length of the detected error path is not guaranteed to be as short as possible, but tends to explore less states in practice. In addition, Mcta also features multi-queue search algorithm, as described below.
Mcta generates the abstract distance values fully automatically for each input given by a timed automaton and a safety property. This is done by efficiently computing a rather coarse abstraction (the user can choose among several kinds of abstraction, see below) and taking the distance in the abstract state space. Mcta in addition offers the possibility to automatically recognize which transitions should be penalized during the state space traversal; this is a new technique described here.
Abstraction-based Heuristics
Heuristics based on the Monotonicity Abstraction (hL and hU)
The heuristics hL and hU are based on the monotonicity abstraction [7]. They adapt a technique from AI Planning, namely ignoring delete lists. The idea of this abstraction is based on the simplifying assumption that every state variable, once it obtained a value, keeps that value forever. I.e., the value of a variable is no longer an element, but a subset of its domain. This subset grows monotonically over transition applications - hence the name of the abstraction.
When applying the monotonicity abstraction to a system of timed automata, then each automaton will (potentially) be in several locations in a state. The system's integer variables will have several possible values in a state. So far clocks are not included in the computation of heuristic values. If we included clocks in the obvious way, every guard or invariant involving a clock would be immediately satisfied. The reason for this is that clock value sets quickly subsume all possible time points.
Pattern Database Heuristics
Pattern database (PDB) heuristics [8] are a family of abstraction-based heuristics. Originally, they were proposed for solving single-agent problems. Today they are one of the most successful approaches for creating admissible heuristics. For a given system S, a PDB heuristic is defined by a pattern P, i. e., a subset of the components of S. The pattern P can be interpreted as an abstraction of S. It is not difficult to see that this kind of abstraction is a projection, and the abstract system is an overapproximation of S. A PDB is built prior to solving the actual model checking task. For this, the entire reachable state space of the abstract system is enumerated. Every reachable abstract state is then stored together with its abstract error distance in some kind of lookup table, the so-called pattern database. Typically, these distances are computed by a breadth-first search. Note that abstract systems have to be chosen so that they are much smaller than their original counterparts and hence are much easier to solve.
When solving the original model checking task with such a PDB,
distances of concrete states are estimated as follows. A concrete
state s is mapped to its corresponding abstract state; the
heuristic estimate for s is then looked up in the PDB.
Mcta can automatically detect efficient abstractions and build the
corresponding PDB [9].
Multi-queue Search Algorithms
In the setting where more than a single distance heuristic is available to guide the search, there is the question of how to exploit this additional information. In such cases, a popular approach is to maintain multiple open queues instead of only one. Within this approach, states are pushed into different open queues according to the additional quality measure, and ordered in this queue according to the distance heuristic. The best state to explore next then is defined as the best state according to the distance heuristic in the best open queue according to the additional quality measure. For example, multi-queue approaches have been successfully applied in the area of AI planning for combining distance heuristics [10] (i. e., in this case, the additional quality measure is another distance heuristic), or for additionally evaluating transitions rather than only evaluating states [11], [12], [13]. Furthermore, in the area of model checking, similar approaches have been proposed to evaluate transitions based on iterative context bounding [14], interference contexts [15], and the notion of useless transitions [16].
Iterative Context Bounding
Iterative context bounding (ICB) has been proposed for the purpose of testing multithreaded programs [14]. Roughly speaking, ICB performs an iterative deepening search with the objective to minimize the number of context switches, i. e., the number of execution points on a trace where the scheduler forces the active thread to change.
Mcta implements this approach by considering threads as automata. Therefore, a context switch occurs if two consecutive transitions on a trace belong to two different automata. It can be combined with arbitrary distance heuristics as well as uninformed search (where the latter corresponds to the original approach).
Context-Enhanced Directed Model Checking
Context-enhanced directed model checking is a further multi-queue approach [15]. In contrast to iterative context-bounding, contexts are essentially defined based on interference of transitions, where transitions t and t' interfere if t writes a variable that is read by t', or t and t' write a common variable. Moreover, during the search, more than two open queues are maintained in general. The approach is based on preferably exploring states that are reached by transitions that interfere with previously applied transitions. More precisely, states are preferably explored if they are reached with a transition with low interference distance to the previously applied transition, where the interference distance of t and t' is defined as the smallest non-negative k such there there are transitions t1, ...,tk with the property that t interferes with t1, t1 interferes with t2, ..., and tk interferes with t'.
Useless Transitions (UT)
Useless transitions [16] are an adaptation of the useless actions approach that has been introduced in the context of AI Planning [13]. As indicated by its name, the concept of useless transitions extends directed model checking by additionally evaluating transitions, not just states. This is a general concept in the sense that useless transitions can be computed fully automatically with the given distance estimation function.
