## 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 (h^{L} and
h^{U})

The heuristics h^{L} and h^{U} 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 *t _{1}*,
...,

*t*with the property that

_{k}*t*interferes with

*t*,

_{1}*t*interferes with

_{1}*t*, ..., and

_{2}*t*interferes with

_{k}*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.