Stefan Edelkamp

Viktor Schuppan

Dragan Bošnački

Anton Wijs

Ansgar Fehnker

Husain Aljazzar

Survey on Directed Model Checking

This article surveys and gives historical accounts to the algorithmic essentials of directed model checking, a promising bug-hunting technique to mitigate the state explosion problem. In the enumeration process, successor selection is prioritized. We discuss existing guidance and methods to automatically generate them by exploiting system abstractions. We extend the algorithms to feature partial-order reduction and show how liveness problems can be adapted by lifting the search space. For deterministic, finite domains we instantiate the algorithms to directed symbolic, external and distributed search. For real-time domains we discuss the adaption of the algorithms to timed automata and for probabilistic domains we show the application to counterexample generation. Last but not least, we explain how directed model checking helps to accelerate finding solutions to scheduling problems.

⋆ The course of writing the article was initiated by forming a working group at the Dagstuhl seminar on Directed Model Checking that took place in April 2006.

Concepts and Notation

State-Space Model We assume a state-space model M to include S as the set of states, T as the set of transitions, and I ⊆ S as the set of initial states. The

Introduction

The presence of a vast number of computing devices in our environment imposes a challenge for designers to produce reliable software and hardware. Testing if a system works as intended becomes increasingly difficult. Formal verification aims to overcome this problem. The process of fully-automatic verification is referred to as model checking [START_REF] Clarke | Model Checking[END_REF][START_REF] Holzmann | The Spin Model Checker: Primer and Reference Manual[END_REF]. Given a formal model of a system and a property specification in some form of temporal logic [START_REF] Emerson | Temporal and modal logic[END_REF], the task is to validate, whether the specification is satisfied. If not, a model checker returns a counterexample for the system's flawed behavior, helping the designer to debug the model.

The major disadvantage of model checking is that it scales poorly. For a complete verification every state has to be looked at. Among the techniques to overcome the state-explosion problem, directed model checking has been established as one of the key technologies. It lessens the burden to find short counterexamples for design bugs quickly. Driven by the success of directed state-space exploration in artificial intelligence, model checking algorithms exploit the property specifications to orient the search towards their falsification.

In this paper we provide an overview of directed model checking with a focus on algorithmic aspects. Section 2 presents the development of directed model checking. In Sect. 3 we introduce notation and basic concepts. Section 4 covers directed model checking algorithms for safety and Sect. 5 extends the discussion to ω-regular properties. The implications of directed model checking on partial-order reduction are explained in Sect. 6. Section 7 shows application of directed model checking in external (disk-based) settings, for real-time systems, for generation of probabilistic counterexamples, and for scheduling problems.

History of Directed Model Checking

Elements of Directed Search in Jan Hajek's Approver Some basic ideas of directed model checking have been present since the very first days of the automated verification of concurrent systems. For instance, Approver, which was probably the first tool for the automated verification of communication protocols, used a directed search of the state space. Approver, from Algorithmic and Proven PROtocol VERifier, was written in the second half of the 70's [START_REF] Hajek | Self-synchronization and blocking in data transfer protocols[END_REF][START_REF] Hajek | Automatically verified data transfer protocols[END_REF][START_REF] Hajek | [END_REF] by Jan Hajek from the Eindhoven University of Technology (at that time Technische Hogeschool Eindhoven). In fact the tool was capable of dealing with a broader class of concurrent systems than the classical communication protocols, like, for instance, mutual exclusion algorithms.

One of the most elaborate parts of Approver were the techniques for fast bug finding. Instead of a depth-or breadth-first search of the state space, that have been usually applied in model checkers, Approver used a general search algorithm based on priority queue. For efficiency this queue was implemented as a heap. Each element of the queue contained a pointer to the state vector in the hash table and a priority field. The records were ordered and selected based on this priority field. The value of the priority field was computed according to the priority function that corresponded to the global invariant that was verified. Directed search was used for the verification of safety properties.

Validation with Guided Search Yang and Dill [113] wrote a seminal paper on the validation with guided search of the state space. The SpotLight system already applied the basic AI search algorithm A* [START_REF] Pearl | Heuristics[END_REF] to combat the state explosion problem. A general search strategy, called the target enlargement analysis, computed nodes around the goal by applying some pre-images starting from the target description before starting the forward search, similar to perimeter search [START_REF] Dillenburg | Perimeter search[END_REF].

Symbolic Directed Model Checking A first study of symbolic directed model checking algorithm simulating the A* exploration in the symbolic µ-calculus model checker µcke [START_REF] Biere | µcke -efficient µ-calculus model checking[END_REF] has been given by Reffel and Edelkamp [START_REF] Reffel | Error detection with directed symbolic model checking[END_REF]. As an input, the proposed BDDA* algorithm assumes a heuristic estimate function in form of a BDD and operates on uniform cost graphs with integer-valued heuristic relations H. This relation partitions the state space in regions of the same heuristic estimates and exploits the succinctness of BDDs to store large state sets. The algorithm simulates the working of a bucket-based priority queue [START_REF] Dial | Shortest-path forest with topological ordering[END_REF]. Instead of selecting only one element with best f = g + h value (where g is a measure of the cost to reach that element from the initial states and h is an estimation of the cost to reach the target), the BDDA* algorithms selects all elements with minimal f -value and expands them in common. The successors are computed in form of a symbolic image operation and evaluated using BDD arithmetics. The resulting f -ordered state sets are put back into the queue. Later on, different authors have extended the framework of symbolic heuristic search, for example SetA* [START_REF] Jensen | SetA*: An efficient BDD-based heuristic search algorithm[END_REF] introduces partitioned heuristics, ADDA* [START_REF] Hansen | Symbolic heuristic search using decision diagrams[END_REF] employed ADDs instead of BDDs, and in SA*, [START_REF] Qian | Heuristic search algorithms based on symbolic data structures[END_REF] studied the strength of symbolic estimates.

While they can represent some sets compactly, BDDs still often grow too large for reachability analysis to complete. Getting an element of DFS into the default BFS exploration mode can help to alleviate that problem. When the BDD holding the current search frontier becomes too large, high-density reachability analysis [START_REF] Ravi | High-density reachability analysis[END_REF] prunes away states that require relatively more BDD nodes to represent than the other states, i.e., to increase the ratio of states per BDD node. When the search frontier becomes empty the whole set of states reached so far is used in the next image computation [START_REF] Ravi | High-density reachability analysis[END_REF] to bring the states back in that have been pruned away. As this step frequently exhausts the available resources, [START_REF] Ravi | Efficient fixpoint computation for invariant checking[END_REF] suggests some alternatives, e.g., storing the pruned states in a separate BDD.

In [START_REF] Ravi | Hints to accelerate symbolic traversal[END_REF] user-supplied hints are used to restrict the transition relation such that parts of the state space are avoided at first that are presumed to lead to a blowup and only added towards the end of the traversal. This limits the effect that in a sequence of BDD operations such as computing the reachable set of states the intermediate BDDs are often much bigger than the end result. Experimental results show improved performance for both false and true properties.

Fraer et al. present an algorithm for reachability that employs frontier splitting to keep BDDs small and selects the part of the frontier to be expanded next based on BDD size [START_REF] Fraer | Prioritized traversal: Efficient reachability analysis for verification and falsification[END_REF].

Explicit-State Directed Model Checking Edelkamp, Leue, and Lluch-Lafuente [START_REF] Edelkamp | Directed explicit-state model checking in the validation of communication protocols[END_REF] coined the term directed model checking and implemented a guided variant of the explicit-state model checker SPIN [START_REF] Holzmann | The Spin Model Checker: Primer and Reference Manual[END_REF]. In HSF-SPIN, safety violation checking is handled by replacing standard search by A*. Besides some deadlock -specific estimates, two generic estimates are supported. For liveness properties an improved nested-DFS algorithm based on the classification of the automata representation of the property in strongly-connected components has been proposed. Later on, partial-order reduction was added [START_REF] Edelkamp | Partial order reduction and trail improvement in directed model checking[END_REF]. Directed model checking has also been applied to guide the search process to obtain a better counterexample for the same error. This is particularly useful if, e.g. due to memory constraints, suboptimal search algorithms were used to obtain a first counterexample [START_REF] Lluch-Lafuente | Directed Search for the Verification of Communication Protocols[END_REF]. set S is often not known a priory, but generated on-the-fly. States are mapped to a set of atomic propositions AP true in that state by a labeling function L : S → 2 AP . The set of transitions T induces a transition relation T on triples (s, t, s ′ ) where t leads from s to s ′ . We use the shorthand notation s t → s ′ . When analyzing safety properties we additionally assume a set of bad states B ⊆ S.

Cost algebras Cost algebras [START_REF] Edelkamp | Cost-algebraic heuristic search[END_REF] generalize edge weights to more general cost structures. A cost algebra is defined as A, ×, , 0, 1 , such that A, ×, 1 , is a monoid, is a total order, 0 = ⊓A and 1 = ⊔A, and A is isotone1 . Intuitively, A is the domain set of cost values, × is the operation used to cumulate values and ⊔ is the operation used to select the best (the least) amongst values. Consider for example, the following instances of cost algebras: IR + ∪ {+∞}, +, ≤, +∞, 0 (optimization), IR + ∪ {+∞}, min, ≥, 0, +∞ (max/min), [0, 1], •, ≥, 0, 1 (probabilistic), or [0, 1], min, ≥, 0, 1 (fuzzy). Not all algebras are isotone, e.g. take [START_REF] Abdeddaïm | Scheduling With Timed Automata[END_REF]. However, the reader may easily verify that the related cost structure implied by (a, c)

A ⊆ IR × IR with (a, c) × (b, d) = (min{a, b}, c + d) and (a, c) (b, d) if a > b or c < d if a = b. We have (4, 2) × (3, 1) = (3, 3) ≻ (3, 2) = (3, 1) × (3, 1) but (4, 2) ≺ (3,
× (b, d) = (a + b, min{c, d}) is isotone. For a path p = (s 0 t0 → s 1 t1 → . . . t k-2 → s k-1 t k-1 → s k ) we define the cumulated cost c(p) as c(t 0 ) × c(t 1 ) × . . . × c(t k-1 )
. As there can be many paths between two states s and s ′ , with δ(s, s ′ ) we refer to the cost of an optimal one. We will also use the shorthand notation δ(s, X) for the optimum of δ(s, s ′ ) for any s ′ in X.

Heuristics Cost-algebraic heuristics h map S to A. We assume that h(e) = 1 for each bad state e ∈ B saying that there is no cost estimated for reaching an error when having encountered it. A heuristic function h : S → A is admissible, if for all s ∈ S we have h(s) δ(s, B), and consistent, if for each s, s ′ ∈ S and t ∈ T s.t. s t → s ′ , we have h(s) c(t) × h(s ′ ). If h is consistent, then it is admissible. The formula-based heuristic H f used is recursively defined on the (safety) property specification. Let v be a Boolean variable, a some constant value in A, and g and h logical predicates. The recursive definition of H f is as follows.

f H f (s) H f (s) f H f (s) H f (s) true 1 0 ¬g Hg(s) Hg(s) false 0 1 g ∨ h ⊔{Hg(s), H h (s)} H f (s) × Hg(s) v if v then 1 else a if v then a else 1 g ∧ h Hg(s) × H h (s) ⊔{Hg(s), H h (s)}
In the definition of H g∧h and H g∨h , the use of × suggests that g and h are independent, which may not be true. When choosing ⊓{H(g), H(f )} instead, (under some additional conditions on the value of a), the formula-based heuristic is consistent. The main reason is that the greatest of two consistent estimates is consistent, while the cumulation might not even be admissible.

The finite state machine (FSM) distance heuristic is based on projecting the system state to the program counter. The abstract state spaces are analyzed prior to the search to capture the shortest path distances of all local states to the set of dangerous states. The distances are cumulated for each running process. More formally, we assume that the global state space is generated based on the asynchronous compositions of processes p i , i ∈ {1, . . . , n}. In other words, each global system state is partitioned into n local states. The state of a local process p i is called its program counter, i ∈ {1, . . . , n}, pc i for short. The FSM distance heuristic is defined as

H m (s, s ′ ) = × n i=1 δ i (pc i (s), pc i (s ′ ))
, where δ i (pc i (s), pc i (s ′ )) denotes the least-cost path from pc i (s) to pc i (s ′ ) in the automaton representation of p i . The values for δ i are computed prior to the search. The FSM distance heuristic assumes that both states s and s ′ are known to the exploration module. It has mainly been used in trail-directed search. As the product of different processes is asynchronous, it is not difficult to see [START_REF] Edelkamp | Partial order reduction and trail improvement in directed model checking[END_REF] that the FSM distance is consistent.

One option to derive a heuristic automatically is to take the optimal cost from the current state to the error in an abstract space derived by any homomorphic abstraction as an admissible estimate, where a homomorphic abstraction is an over-approximation, for which each path in the concrete space induces a corresponding path in the abstract [START_REF] Clarke | Model checking and abstraction[END_REF][START_REF] Kurshan | Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach[END_REF]. Abstractions may contract states into one and merge edges accordingly. More precisely, if we contract states s 1 and s 2 and there are transitions s 1

t1 → s 3 , s 2 t2 → s 3 or transitions s 3 t1 → s 1 , s 3 t2 → s 2 ,
we merge t 1 and t 2 to t 3 with c(t 3 ) = c(t 1 ) ⊔ c(t 2 ). Self-loops usually do not contribute to an optimal solution and can be omitted. It is not difficult to see that such abstraction heuristics are consistent. Unfortunately, re-computing the heuristic estimate from scratch cannot speed-up the search [105]. A solution is to completely evaluate the abstract space prior to the search in the concrete space.

For a model M with abstraction M, an abstraction database [START_REF] Qian | Guided invariant model checking based on abstraction and symbolic pattern databases[END_REF][START_REF] Edelkamp | Abstraction in directed model checking[END_REF] is a lookup table indexed by ŝ ∈ Ŝ containing the shortest distance from ŝ to B. The size of an abstraction database is the number of states in Ŝ. For undirected graphs with uniform edge weights (usually equal to 1) it is easiest to create an abstraction database by conducting a breadth-first search in backward direction, starting at B. This assumes that for each (abstract) transition t we can devise an inverse (abstract) transition t -1 such that ŝ t → ŝ′ iff ŝ′ t -1 → ŝ. To construct an abstraction database for weighted and directed graphs, the shortest path exploration in abstract space uses inverse transitions and Dijkstra's algorithm. If inverse operators are not available, we reverse the state space graph as generated in a forward chaining search. With each state ŝ′ we attach the list of all predecessor states ŝ. In case a bad state is encountered, the traversal is not terminated but the abstract bad states are collected in a (priority) queue. Next, backward traversal is invoked on the inverse of the state space graph, starting with the queued set of abstract bad states. The shortest path distances to the abstract bad states are stored with each state in a hash table. For a better time-space trade-off it is possible to fully traverse the abstract state space symbolically, yielding symbolic abstraction databases [START_REF] Edelkamp | Symbolic pattern databases in heuristic search planning[END_REF].

Procedure ModelCheck

Input: Model M = (S, T , I, L), set of bad states B, cost algebra A Output: true if property is satisfied or counterexample if not 1 Closed ← ∅; Open ← I 2 while (Open = ∅) 3 S ← SelectA(Open) 4 Open ← Open \ S; Closed ← Closed ∪ S 5 if (S ∩ B = ∅) return GeneratePath(S ∩ B) 6 Succ ← {s ′ | s ∈ S, (s, t, s ′ ) ∈ T } 7 Succ ← Succ \ Closed; Open ← Open ∪ Succ 8 return true Fig. 2. General Model Checking Algorithm.
Abstraction directed model checking [START_REF] Qian | Formal Symbolic Verification Using Heuristic Search and Abstraction Techniques[END_REF] combines model checking based on abstraction [START_REF] Clarke | Model checking and abstraction[END_REF][START_REF] Kurshan | Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach[END_REF][START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] and directed model checking as follows. An initial model checking run is performed on the abstract model. If the property holds, then the model checker returns true. If not, in a directed model checking attempt, the same abstraction is used to guide the search in the concrete state space to falsify the property. If the property does not hold there, a counterexample is returned; if it does, the property has been verified (see Fig. 1). If the abstraction (heuristic) turns out to be too coarse, it is possible to iterate the process with a refined abstraction.

Directed Model Checking Algorithms

Standard Forward Reachability A pseudo-code implementation of a forward reachability model checking algorithm (for safety properties) based on sets is provided in Fig. 2. In Line 1 the structures are initialized while Lines 2-7 perform the search for an error in a loop. If terminated without finding an error, Line 8 returns that the property is verified due to a complete exploration. Line 3 is a generic selection mechanism that determines the search traversal policy. Line 4 moves the selected set from Open to Closed, while Line 5 detects and handles bad states. Line 6 generates the successor set from which Line 7 eliminates duplicates. It also inserts the remaining elements into the search frontier.

In Select A we can incorporate any specialized selection strategy. For BFS, we select the states with smallest depth, while for DFS we select the one(s) with the largest depth. For Dijkstra-like search we select one element with the least cost. Let C be the cost relation that relates a state to a cost-algebraic value. In such case, Select A (Open) returns some s ′ in Open with (s ′ , a) ∈ C and for all s in Open with (s, b) ∈ C we have a b. In the explicit-state version one candidate is selected, while in the set-based version all states are selected.

Forward Reachability with Costs

The algorithm in Fig. 2 does not say anything about updating the cost relation C, which is modified during the execution of the algorithms. At invocation time, we have (s, 1) ∈ C for all s ∈ I, and (s, 0) ∈ C for all s / ∈ I. Whenever we reach a new state s ′ from s via transition t we perform cost relaxation, i.e., if

a × c(t) ≺ b with (s, a) ∈ C and (s ′ , b) ∈ C we update C ← C \ {(s ′ , b)} ∪ {(s ′ , a × c(t))}.
Strictly speaking, full initialization of the cost relation is not possible for the on-the-fly analysis of the system. Therefore, cost values are stored together with the states in the list Open and Closed.

The update of relation C depends on the search algorithm. We call a state settled, if (s, a) ∈ C and a = δ(I, s). Moreover, a cost relation is called monotone, if for (s, a) ∈ C and (s ′ , b) ∈ C and (s, t, s ′ ) ∈ T , we have a b.

The selection strategy in Dijkstra's algorithm only considers settled states and monotone cost relations [START_REF] Dijkstra | A note on two problems in connection with graphs[END_REF]. If it is not monotone, different approaches have been suggested. The main observation is that a cost update has to be executed more than once for a transition. It can be shown that BFS settles at least one unsettled state on an optimal path π * in the Open list, such that after |π * | iterations of ModelCheck without re-initializing C the bad state on π * is settled [START_REF] Bellman | On a routing problem[END_REF]. In k-best first search [START_REF] Felner | Improving Search Techniques and using them in Different Environments[END_REF] we select the k least-cost elements from Open and compute their set of successors in common. The algorithm is complete but the counterexample might not be optimal. k-beam search [START_REF] Bisiani | Beam search[END_REF] additionally prunes away all states from Open that are not among the k best ones. In this case, completeness is sacrificed to search for errors in larger models. By iteratively performing k-beam search with larger k we get iterative-broadening [START_REF] Ginsberg | Iterative broadening[END_REF], by which we gain back completeness.

Guided Forward Reachability All exploration variants of the general model checking algorithm that we have seen so far are blind in the sense, that they do not incorporate any guidance towards a quicker falsification of the property. Directed model checking algorithms reorder the states to be expanded in order to accelerate error-detection in the case of choosing a different selection strategy.

The estimated cost of a counterexample at a given state s is the accumulation of the costs of reaching s and the heuristic estimate for reaching a bad state starting from s. This implies a = δ(I, e). Therefore, A* with H(B, 1) returns the cost-optimal counterexample. Optimality is only granted, if the goal check is performed at the expanded state. BFS is an exception, which terminates at a generated goal.

For inconsistent heuristics, it can happen that a better path to an already expanded state is encountered during the search process. For such case a reopening strategy has been proposed [START_REF] Pearl | Heuristics[END_REF]. It moves states from the set of already expanded states Closed back to the search frontier Open. Although in theory an exponential increase in the number of expanded nodes may happen, re-opening produces optimal counterexamples for admissible heuristics and works well in practice. The underlying problem of searching with non-consistent heuristics is equivalent to the search with non-monotone paths in a problem graph.

Bounded Forward Reachability In Fig. 3 we display a cost-bounded variant of the general model checking algorithm. It extends the algorithm in Fig. 2 by an additional pruning condition in Line 8. The algorithm includes cost threshold U as an additional parameter. In the guided form shown here, it is based on the relations C and H, as introduced above. There are various reasons for introducing parameter U . An upper bound prevents the algorithm from searching too deep e.g. when using depth-first selection strategies. Any generated counterexample has a quality not worse than U . If U = δ(I, B) then up to tie-breaking and the choice of H the optimal number of states are expanded [START_REF] Dechter | The optimality of A* revisited[END_REF]. The reason is that any optimal exploration strategy has to explore all states with costs smaller than δ(I, B). In some cases U = δ(I, B) is already known, the only task is to generate a counterexample matching it. If U is not known, one may adjust U interactively. Automated strategies are iterative-deepening [START_REF] Korf | Depth-first iterative-deepening: An optimal admissible tree search[END_REF] (increasing U by the smallest amount possible), branch-and-bound [START_REF] Kumar | Branch-and-bound search[END_REF] (decreasing U to the largest value smaller than the latest cost value obtained), or refined threshold determination [107] (an exponential or binary search compromise between the two). In memory-limited A* search [START_REF] Russell | Efficient memory-bounded search methods[END_REF], full duplicate elimination in the Closedlist is sacrificed in order to gain space. U can control the memory needs. If the cost-updates do not preserve monotonicity, the cost values of some states in Closed are not optimal on the first visit and some nodes may remain unsettled.

According to the selection mechanism in Select A we arrive at different branchand-bound strategies. Depth-bounded depth-first search imposes an upper bound on the solution depth, to prevent the algorithms from searching too deep. As our algorithm, it takes U as an additional input parameter. Admissible depth-first search guarantees to find an error of cost smaller than the given threshold. Open ← Open \ S;

Closed ← Closed ∪ S 5 if (S ∩ B = ∅) then return GeneratePath(S ∩ B) 7 Succ ← {s ′ | s ∈ S, (s, t, s ′ ) ∈ T }; Succ ← Succ \ Closed 8 Succ ← Succ \ {s ∈ Succ | ∃a, b ∈ A.C(s, a) ∧ H(s, b)∧ U ≺ a × b} 9
Open ← Open ∪ Succ 10 return true Fig. 3. Cost-Bounded Model Checking Algorithm.

For cost-optimal depth-bounded search with duplicate detection there is a potential pitfall [START_REF] Edelkamp | Partial order reduction and trail improvement in directed model checking[END_REF]. It is apparent in depth-first depth-bounded search but applies to many cost-bounded variants. The problem is that a cached duplicate may not be reached with optimal cost on the first visit such that on the second visit it is stored with suboptimal cost. Even worse, if the successor of a such cached duplicate has a bad state outside the cost threshold as a successor then this error might not be detected even if its cost are below the cost threshold. A possible solution is to re-open a state if reached with better costs.

Sparse Memory Forward Reachability

In model checking practice, the limitation of (main) memory is likely to be the most challenging problem. Set Closed is mainly kept to prevent exploring states twice and it tends to take up most space. In Fig. 4 we show a pseudo-code implementation of frontier search that has shown significant improvements in solving action planning and sequence alignment problems [START_REF] Korf | Frontier search[END_REF]. The assumption here is that not the entire set of states needs to be stored completely for detecting an error. How many layers are sufficient for full duplicate detection in general is dependent on a property of the search graph called locality. For uniform weighted problem graphs, it is defined as the maximum max{δ(I, s)δ(I, s ′ )} + 1 of all states s, s ′ , with s ′ being a successor of s. It determines the thickness of the boundary slice of the graph needed to prevent duplicates to occur in the search.

One observation for state selection is that breadth-first branch-and-bound frontier search often results in a smaller search frontier than best-first branchand-bound frontier search. In AI literature, the according search strategy is called breadth-first heuristic search [114]. In beam-stack-search this strategy has been extended to feature partial state selection [115]. For such memory-limited frontier search, (divide-and-conquer) solution reconstruction is needed, for which certain relay layers are additionally stored in main memory. Open ← Open \ S 7

if

(S ∩ B = ∅) then return GeneratePath(S ∩ B) 8 Succ ← Succ ∪ {s ′ | s ∈ S, (s, t, s ′ ) ∈ T } 9 Succ ← Succ \ S L k=0 Closed(k) 10 Succ ← Succ \ {s ∈ Succ | ∃a, b ∈ A.C(s, a) ∧ H(s, b) ∧ U ≺ a × b} 11 for each k = L, . . . , 1 Closed(k) ← Closed(k -1) 12 return true

ω-regular Properties

The exposition has so far been restricted to checking reachability of a set of states. We now show how the machinery can be used to check ω-regular properties, which properly include propositional LTL [START_REF] Emerson | Temporal and modal logic[END_REF].

We assume that the reader is familiar with the automaton-based approach to model checking of ω-regular properties [106]. We extend our state space model with a Büchi fairness constraint F ⊆ S to M = (S, T , I, L, F) and restrict the discussion below to the search of a fair lasso-shaped path in M. See also [START_REF] Holzmann | The Spin Model Checker: Primer and Reference Manual[END_REF][START_REF] Clarke | Model Checking[END_REF].

Nested Depth-First Search The most popular algorithm to search for fair lassoshaped paths in explicit-state model checking is probably nested depth-first search [START_REF] Courcoubetis | Memory efficient algorithms for the verification of temporal properties[END_REF][START_REF] Holzmann | On nested depth first search[END_REF]. A first DFS finds all reachable states. When backtracking from a fair state it starts a second DFS that tries to close a fair cycle by hitting a state on the stack of the first DFS. When that happens, a counterexample can be reconstructed easily from both search stacks. States are marked as visited by either DFS, hence, each state is visited at most twice. Marking can be done with just two bits per state, which is the main reason for the frequent use of this algorithm in explicit-state model checking. On the downside, starting the second DFS in post order tends to produce long counterexamples.

In the inner search it's obvious that the search should be directed to some state in the stack of the outer search. Potential heuristics for this case include the Hamming and the FSM distance heuristic [START_REF] Edelkamp | Partial order reduction and trail improvement in directed model checking[END_REF]. In the outer search it's less clear what a promising direction should look like. Clearly, the likelihood of finding a fair cycle should be high. If the state space of M is the synchronous product of smaller state spaces M 1 , M 2 , . . ., some M i can be analyzed beforehand to obtain approximate information on whether a state s = (s 1 , s 2 , . . .) in M can be part of a strongly connected component with a fair cycle at all. Only if all s i are part of an SCC that includes a fair path in M i then s can be part of an SCC with a fair path itself. Hence, if any s i is known not to be in such SCC then the search should be directed to the edge of the current SCC [START_REF] Edelkamp | Directed explicit-state model checking in the validation of communication protocols[END_REF].

Liveness Checking as Safety Checking Transforming a liveness checking problem into a safety checking problem immediately makes the algorithms in Sect. 4 available for all ω-regular properties. Here, we consider the state-recording translation that reformulates the problem of finding a fair lasso as a reachability problem [START_REF] Biere | Liveness checking as safety checking[END_REF][START_REF] Schuppan | Efficient reduction of finite state model checking to reachability analysis[END_REF][START_REF] Schuppan | Liveness checking as safety checking for infinite state spaces[END_REF][START_REF] Schuppan | Liveness Checking as Safety Checking to Find Shortest Counterexamples to Linear Time Properties[END_REF]. The translation extends the original model with a copy for each state variable and a number of flags. It splits the search for a fair lasso into 3 steps: (1) non-deterministically guess and record a loop start in a copy of the set of state variables, (2) search a fair state and record its occurrence in a flag, and (3) return to the guessed and recorded loop start. Shortest fair lassos can be found when breadth-first search or A* [START_REF] Pearl | Heuristics[END_REF] are used. 2 Although the reformulation roughly squares the size of the state space, performance of BDD-based symbolic model checking is improved for some examples [START_REF] Schuppan | Efficient reduction of finite state model checking to reachability analysis[END_REF][START_REF] Schuppan | Liveness Checking as Safety Checking to Find Shortest Counterexamples to Linear Time Properties[END_REF]. The method has been applied to SAT-based interpolation [START_REF] Mcmillan | Interpolation and SAT-based model checking[END_REF], to external distributed explicitstate directed model checking [START_REF] Edelkamp | Large-scale directed model checking LTL[END_REF], and, independently, to regular model checking [START_REF] Bouajjani | Abstract regular model checking[END_REF].

The heuristics should distinguish whether a loop start has been guessed or not. If not (step 1), we are effectively in the outer part of a nested search and should seek for promising loop starts. Once a state has been saved, a fair state (step 2) and, after that (step 3), the loop start are preferred targets. Applicable heuristics in all phases include Hamming and FSM distance heuristics [START_REF] Edelkamp | Directed explicit-state model checking in the validation of communication protocols[END_REF][START_REF] Edelkamp | Partial order reduction and trail improvement in directed model checking[END_REF].

Other Algorithms Similar to the case of safety properties trail improvement can also be used for lasso-shaped counterexamples [START_REF] Edelkamp | Partial order reduction and trail improvement in directed model checking[END_REF][START_REF] Lluch-Lafuente | Directed Search for the Verification of Communication Protocols[END_REF]. Assume, that a lassoshaped counterexample π = π stem • π ω loop to some ω-regular property is given. Directed model checking with Hamming or FSM distance heuristics is then used to shorten π as follows. Let s l be the first state of π loop . In a first step a potentially shorter trail π ′ stem from the initial states to s l is generated. Then a fair cycle π ′ loop starting and ending in s l is produced. Backtracking is used to guarantee fairness of π ′ loop . As a further optimization, s l can be replaced with any state s ′ l that is equivalent to s l in the sense that the sequence of transitions that leads from s l to s l in π ′ loop also lead from s ′ l to s ′ l and hits a fair state in between. Standard algorithms in BDD-based model checking, which are typically variants of the Emerson-Lei algorithm [START_REF] Emerson | Efficient model checking in fragments of the propositional mu-calculus (extended abstract)[END_REF], perform a nested fixed point computation, which makes application of heuristics difficult. The idea of using hints has been extended to nested fixed points [START_REF] Bloem | Efficient decision procedures for model checking of linear time logic properties[END_REF], though with less success than in [START_REF] Ravi | Hints to accelerate symbolic traversal[END_REF]. CTL is covered in [START_REF] Bloem | Symbolic guided search for CTL model checking[END_REF]. In the context of an SCC enumeration algorithm a prioritization was used based on the distance of states to the origin and on the number of fairness constraints they fulfill to select a state as the starting point for further SCC decomposition [108]. The approach by [START_REF] Fraer | Prioritized traversal: Efficient reachability analysis for verification and falsification[END_REF] extends to other least fixed point computations.

Partial Order Reduction

Partial order reduction (POR) [104, [START_REF] Godefroid | Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State Space[END_REF][START_REF] Peled | Combining partial order reductions with on-the-fly model-checking[END_REF] is one of the most important statespace reduction techniques in explicit state model checking. In this section we discuss how POR can be combined with directed model checking. The only essential difference with POR for standard model checking (for instance, as presented in [START_REF] Clarke | Model Checking[END_REF]) is in the condition called the cycle proviso. Intuitively, this condition prevents ignoring parts of the system (state space) because of closing cycles during the search. The classical versions of the cycle proviso in standard model checking are closely dependent on the search order -usually DFS [START_REF] Godefroid | Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State Space[END_REF] or BFS [START_REF] Alur | Partial-order reduction in symbolic state-space exploration[END_REF]. Because of that they are not applicable in directed model checking. The proviso that we use to make POR compatible with directed model checking is inspired by the general search order proviso presented in [START_REF] Bošnački | Partial-order reduction for general state exploring algorithms[END_REF]. In the rest of the section we introduce some basic terminology along the lines of [START_REF] Alur | Partial-order reduction in symbolic state-space exploration[END_REF] and state the new version of the cycle proviso for safety and liveness properties.

Let M = (S, T , I, L, F) be a model of the state space as introduced in Section 5. To improve readability, we write s t → M s ′ for (s, t, s ′ ) ∈ T . When the model M is clear from the context we omit it. Further, we assume that the transition relation is deterministic in the sense that for each transition t ∈ T and each state s ∈ S there exists at most one s ′ ∈ S such that s t → s ′ . Thus, each transition can be seen as a partial function t : S → S which is defined if s ′ exists. We also say that s ′ is a successor of s. A transition t ∈ T is said to be M-enabled in state s ∈ S iff t(s) is defined. The set of all transitions t ∈ T enabled in state s ∈ S is denoted enabled M (s).

The basic idea of state space reduction is to restrict the part of the state space of a concurrent system that is explored during verification in such a way that all properties of interest are preserved. To this end we define a function r which assigns to each state s a set of transitions r(s). During the on-the-fly construction for each state s already included in the state set S r of the reduced model M r , we add its successors obtained via transitions in r(s). We start with an S r that includes only the initial states I of the original model M. Those states become also the initial states I r of the reduced model M r . Then we iterate the above described extension of S r (M r ) until a fixed point is reached. The construction of the reduced model is captured in the following definition:

For any reduction function r : S → 2 T , we define the (partial-order) reduction of M = (S, T , I, L, F) with respect to r as the smallest model M r = (S r , T r , I r , L r , F r ) satisfying the following conditions: S r ⊆ S, I r = I; and for every s, s ′ ∈ S r and t ∈ r(s) if s t → M s ′ then s t → Mr s ′ . We say that property φ is preserved by the reduction iff M |= φ ⇔ M r |= φ. Depending on the properties that a reduction must preserve, we define additional restrictions on r. These sets of restrictions are well known in the POR theory (see [START_REF] Alur | Partial-order reduction in symbolic state-space exploration[END_REF][START_REF] Clarke | Model Checking[END_REF]).

Let M be a model with a reduction function r that is persistent in the sense of [START_REF] Alur | Partial-order reduction in symbolic state-space exploration[END_REF][START_REF] Godefroid | Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State Space[END_REF] and let us first consider POR without DMC. The POR variation of the general model checking algorithm (GMCAPOR) is obtained by replacing in the algorithm in Fig. 2 the assignment Succ ← {s ′ | s ∈ S, (s, t, s ′ ) ∈ T } with Succ ← {s ′ | s ∈ S, (s, t, s ′ ) ∈ T ∧ t ∈ r(s)} where r(s) satisfies -besides the well-known conditions C0a, C0b, C1 (see, e.g., [START_REF] Bošnački | Partial-order reduction for general state exploring algorithms[END_REF]) -the condition -C2c: For each s ∈ S r there exists a transition t ∈ r(s) such that s ′ = t(s) and s ′ ∈ Closed. Otherwise r(s) = enabled M (s).

Thus, we require that at least one new state which is explored via an action in r(s) must not be in Closed. Otherwise the reduced set r(s) must include all transitions which are enabled in s. The intuition behind C2c is that each transition t which is not in r(s), i.e., it is temporarily ignored in s, will be considered in at least one successor s ′ of s. Since s ′ is not in Closed, it must be either in Open or a new unexplored state which will be put in Open. Thus, s ′ will be considered in some later iteration of the algorithm. Condition C1 ensures that t remains enabled also in s ′ . It could happen that t is ignored in s ′ too, but condition C2c will again ensure that it is considered later in some of its successors. As the set S r is finite one can show that this ignoring cannot go forever and the action will be eventually included in some r(s ′′ ) for some state s ′′ that is reachable in M r from s ′ and therefore also from s.

Similarly as in [START_REF] Bošnački | Partial-order reduction for general state exploring algorithms[END_REF], one can show that condition C2c implies the general ignoring prevention condition given by Lemma 2.2 of [START_REF] Alur | Partial-order reduction in symbolic state-space exploration[END_REF]. Although a stronger condition usually implies less reduction, in practice the advantage of C2c over Lemma 2.2 of [START_REF] Alur | Partial-order reduction in symbolic state-space exploration[END_REF] is that the former can be efficiently checked based only on local information, i.e., considering only state s and its successors. The correctness of the GMCAPOR algorithm does not depend on the order in which states are removed from Open, i.e., it is independent of the selection strategy implemented by Select A . Therefore, the correctness of the combination of POR with the directed model checking algorithm follows immediately. By requiring that S is a singleton we obtain the explicit state version of the general (directed) state exploring algorithm with POR in [START_REF] Bošnački | Partial-order reduction for general state exploring algorithms[END_REF], while by putting S = Open we get the POR algorithm for symbolic (breadth-first) search in [START_REF] Alur | Partial-order reduction in symbolic state-space exploration[END_REF].

To preserve liveness properties (LT L -X , CT L * -X ) with GMCAPOR one has to ensure that function r satisfies the liveness variant of the transition ignoring condition which requires that along each cycle c in the reduced model in at least one state s of c it holds r(s) = enabled M (s). Intuitively, this condition ensures that a transition cannot be indefinitely postponed along c since it will be eventually included in r(s). The drawback of this condition is that it is defined globally on the reduced state space. Like for safety properties, we give a stronger condition that might produce less reduction but it is locally checkable in an efficient manner:

-C2cl: For each s ∈ S r for all transitions t ∈ r(s) such that s ′ = t(s) it holds s ′ ∈ Closed. Otherwise r(s) = enabled M (s).

Applications

To explore complex systems, the above algorithms have to be adapted.

Procedure DiscreteDirectedModelCheck

Input: Model M = (S, T , I, L), set of bad states B, estimate sets Hj, 0 ≤ j ≤ max h Output: true if property is satisfied or counterexample if not 1 for each i = 1, . . . , L for each j = 0, . . . , max h 2 Open(-i, j) ← ∅ 3

for each j = 0, . . . , max h 4

Open(0, j) ← I ∩ Hj

5 fmin ← min{j ≥ 0 | Open(0, j) = ∅} 6 while (fmin = ∞) 7 gmin ← min{i | Open(i, fmin -i) = ∅} 8 while (gmin ≤ fmin) 9
Min ← Open(gmin, fmingmin)

10 Min ← Min\ S L k=1 Open(gmin -k, fmin -gmin) 11 if (Min ∩ B = ∅) then return GeneratePath(Min ∩ B) 12 Succ ← {s ′ | s ∈ Min, (s, t, s ′ ) ∈ T } 13
for each j = fmingmin -1, . . . , max h 14

Open(gmin + 1, j) ← Open(gmin + 1, j) ∪ (Succ ∩ Hj)

15 gmin ← gmin + 1 16 fmin ← min({i + j > fmin | Open(i, j) = ∅} ∪ {∞})
Fig. 5. Directed Model Checking Algorithm for Uniform Costs.

Discrete Model Checking Discrete edge costs are very common in model checking practice. In fact, most problem graphs considered are uniform, i.e., every edge has cost 1. As in this case the heuristic evaluation function estimates the remaining path length to the error, it is bounded by an upper-bound max h on the optimal counterexample length. This allows to split the relation H into sets of states H j , j = 0, . . . , max h , that share the same heuristic value, In Fig. 5 we have depicted the matrix implementation of the general directed model checking algorithm for uniform costs. Before expanding a state set (a.k.a. bucket) from the matrix, we eliminate possible duplicates by state set subtraction. Next we check for bad states, generate the successor set and distribute it according to the heuristic relation. For the sake of simplicity, we have assumed consistent estimates, for which each state is expanded at most once. For admissible but non-consistent estimates, we have to re-expand buckets and enlarge the range of j to [0, . . . , max h ].

For disk-based (graph) search [START_REF] Sanders | Algorithms for Memory Hierarchies[END_REF], the changes to the algorithm Discrete-DirectedModelCheck are moderate. For detecting duplicates in one bucket, it is sorted beforehand, and, instead of intersecting two sets internally, we scan the corresponding files (assuming they are already sorted). In external frontier search relay layers are not needed; the exploration fully resides on disk. There is one subtle problem: predecessor pointers are not available on disk. This is resolved by saving the predecessor together with every state, by scanning with decreasing depth the stored files, and by looking for matching predecessors. Any reached node that is a predecessor of the current node is its predecessor on an optimal solution path. This results in an I/O complexity that corresponds to a linear scan of at most all nodes visited.

To organize the communication between the processors in a parallel environment a working queue is maintained on disk [START_REF] Edelkamp | Large-scale directed model checking LTL[END_REF]. The working queue contains the requests for exploring parts of a (g, h) bucket together with the part of the file that has to be considered. As processors may have different computational power and processes can dynamically join and leave the exploration, the number of state space parts does not necessarily have to match the number of processors.

Real-Time Model Checking Timed automata (TA) extend finite labelled transition systems with real-valued variables called clocks to capture delays and timing constraints. Directed model checking for TAs was developed parallel to directed model checking for finite systems, and was coined guided model checking [START_REF] Behrmann | Efficient guiding towards cost-optimality in uppaal[END_REF]. These techniques have been successfully applied to several case studies and were implemented in the directed model checker for timed automata MCTA [START_REF] Kupferschmid | Uppaal/dmc-abstraction-based heuristics for directed model checking[END_REF][START_REF] Kupferschmid | Faster than Uppaal? In CAV[END_REF] and added to the existing model checker UPPAAL [START_REF] Behrmann | Efficient guiding towards cost-optimality in uppaal[END_REF][START_REF] Dierks | Time, abstraction and heuristics -automatic verification and planning of timed systems using abstraction and heuristics[END_REF][START_REF] Rasmussen | Resource-optimal scheduling using priced timed automata[END_REF].

TA distinguish between delay and discrete edge transitions. Delay transitions increment all clock variables with the same amount, while the finite part of the state remains unchanged. Discrete edge transitions may change the finite part of the state and reset clock variables to zero. Guards and invariant conditions over clock variables are defined using clock constraints Ψ (Cl), defined by

ψ := x ✁ c | x -y ✁ c | ψ ∧ ψ | ¬ ψ with x, y ∈ Cl, c ∈ Z Z,
and ✁ ∈ {<, ≤}. This restriction to simple constraints on clocks, and constraints on differences between clocks is used in [START_REF] Alur | A theory of timed automata[END_REF] to show that model checking TAs is decidable.

Common model checkers use symbolic semantics based on zones. A zone Z is a maximal set of clock valuations satisfying a constraint from Ψ (Cl). A symbolic state s is a pair (l, Z) of a location and a zone. Symbolic state s = (l, Z) represents a subset of

s ′ = (l ′ , Z ′ ), denoted s ⊆ s ′ , if l = l ′ and v |= Z ⇒ v |= Z ′ .
Necessary operations can be effectively realized, using a canonical representation of zones as weighted graph, known as Difference Bound Matrices [START_REF] Bengtsson | Timed automata: Semantics, algorithms and tools[END_REF].

Due to the nature of delay, it is possible to reach any reachable state by an alternation of delays and edge transitions (by inserting zero delays or merging successive delays). The length of a counterexample can and is in practice expressed in the number of discrete edge transitions. Cost and heuristic are typically defined over cost algebra A = (IN 0 ∪ ∞, +, ≤, ∞, 0). If the goal is to minimize the length of the error trace, we assume for the cost that c(t) = 0 for delay transitions, and c(t) = 1 otherwise. The forward reachability algorithm presented in Fig. 2 can then be extended, as depicted in Fig. 6, to deal with TAs. We assume that set of bad states B is a pair of a location and zone (l b , Z b ).

A consequence of the zone-semantics is that a symbolic state s ′ may represent a subset of another symbolic state s. Model checking algorithms for TAs differ therefore in one important aspect from the general algorithm in Fig. 2. Rather than checking for equality between sets of states, they typically check for set inclusion. If symbolic state s ∈ Closed, then we can discard exploration of any subset s ′ of s. Duplicate detection in Line 8 in Fig. 6 reflects the deletion of subsets. Similarly, a symbolic state will not be added to Open if it is the subset of some symbolic state in Open.

Although guided model checking as presented in [START_REF] Behrmann | Efficient guiding towards cost-optimality in uppaal[END_REF] was aimed at cost optimal reachability, it also explored briefly heuristics for simple reachability. automata-theoretic abstractions [START_REF] Kupferschmid | Uppaal/dmc-abstraction-based heuristics for directed model checking[END_REF][START_REF] Kupferschmid | Adapting an AI planning heuristic for directed model checking[END_REF]. The monotonicity relaxation assumes that once a value of a variable is attained, it may keep this value forever. The semantics of a transition system under the monotonicity relaxation is set based, and the successors increase monotonously with respect to set inclusion. The automatatheoretic abstraction repeatedly replaces a pair of automata with an abstraction of their product. The size of these abstraction is limited by a given N ; to reach this bound bisimilar states and states with a large heuristic value are merged. This ensures that close to the error state, the abstraction is nevertheless accurate. For given benchmarks both heuristics reduced time and memory requirements, and furthermore found shorter error traces than Uppaal's random DFS [START_REF] Kupferschmid | Uppaal/dmc-abstraction-based heuristics for directed model checking[END_REF][START_REF] Kupferschmid | Faster than Uppaal? In CAV[END_REF].

Stochastic Model Checking integrates quantitative dependability analysis with model checking. In this context, systems are usually described as Markov models.

The mostly used models are discrete-time Markov chains (DTMCs), continuoustime Markov chains (CTMCs) and Markov Decision Processes (MDPs) [102]. These models can be considered as a labelled transition system extended by transition probabilities. More concretely, in each state a probability distribution describes the probability of firing a particular transition as the next step of the system. Dependability requirements on such models are usually formulated in a stochastic temporal logic like PCTL [START_REF] Hansson | A logic for reasoning about time and reliability[END_REF] in the discrete-time case or CSL [START_REF] Aziz | Model-checking continuous-time Markov chains[END_REF][START_REF] Baier | Model-checking algorithms for continuous-time Markov chains[END_REF] in the continuous-time case. Model checking of PCTL or CSL formulae relies mainly on numerical methods to solve linear equation systems [102,[START_REF] Hansson | A logic for reasoning about time and reliability[END_REF][START_REF] Aziz | Model-checking continuous-time Markov chains[END_REF][START_REF] Baier | Model-checking algorithms for continuous-time Markov chains[END_REF]. A weakness of these methods is their inability to provide counterexamples. This problem has been studied in the literature for a particular type of dependability properties, namely probabilistic reachability, [START_REF] Aljazzar | Counterexamples for timed probabilistic reachability[END_REF][START_REF] Aljazzar | Extended directed search for probabilistic timed reachability[END_REF][START_REF] Han | Counterexamples in probabilistic model checking[END_REF][START_REF] Han | Providing evidence of likely being on time: Counterexample generation for ctmc model checking[END_REF][START_REF] Aljazzar | Counterexamples for model checking of markov decision processes[END_REF]. A probabilistic reachability property is a claim that the probability to run into a bad state, i.e., a state from B, does not exceed a particular probability bound p. Such a property is violated in the case that the accumulated probability of all offending paths, i.e., paths from an initial state to a state in B, is higher than p. A counterexample in this context is then a set of offending paths such that its accumulated probability is higher than p. Since paths with high probability represent high probable system executions, we expect the human user to be more interested in counterexamples which include most probable offending paths.

In [START_REF] Aljazzar | Counterexamples for timed probabilistic reachability[END_REF][START_REF] Aljazzar | Extended directed search for probabilistic timed reachability[END_REF], an approach based on directed model checking has been proposed to address this problem. The basic idea of that approach is to select the most probable offending path. This can be done by using the algorithm in Fig. 3 combined with the probabilistic cost algebra [0, 1], •, ≥, 0, 1 . The cost of a transition is its probability. This means that the cost of a path, i.e., the product of the costs of each transition along the path, is just the probability of that path. This setting results in selecting the offending path with the maximal probability. In [START_REF] Aljazzar | Counterexamples for timed probabilistic reachability[END_REF][START_REF] Aljazzar | Extended directed search for probabilistic timed reachability[END_REF] the basic algorithm is extended to construct a whole counterexample by not only selecting one most probable offending path but a sufficient set of such paths. Since counterexamples in this context can contain a large number of paths, analysing them is a chellange for a human user. In [START_REF] Aljazzar | Debugging of dependability models using interactive visualization of counterexamples[END_REF], a method based on interactive visualization is proposed which makes analysing complex counterexamples easier.

Search for Schedules

The following is an overview of techniques to approach scheduling problems.

[112] provides a more detailed discussion, comparing the tools Spin, Cadp and Uppaal Cora. In recent years, model checkers have been applied to solving combinatorial optimization problems. In particular, scheduling problems have been considered often, e.g. [START_REF] Abdeddaïm | Scheduling With Timed Automata[END_REF][START_REF] Behrmann | Efficient guiding towards cost-optimality in uppaal[END_REF][START_REF] Behrmann | Optimal scheduling using priced timed automata[END_REF][START_REF] Bozga | Scheduling Acyclic Branching Programs on Parallel Machines[END_REF][START_REF] Brinksma | Verification and Optimization of a PLC Control Schedule[END_REF][START_REF] Fehnker | Scheduling a Steel Plant with Timed Automata[END_REF][START_REF] Ruys | Optimal scheduling using Branch-and-Bound with SPIN 4.0[END_REF]103,110,111,112]. The approach here is to interpret the problem as a reachability problem, where the question is, in a system where transitions have costs, what the minimal necessary cost is to reach a state in B, where B ⊆ S is a set of goal states (i.e. 'good' states where a complete schedule for the given problem has been achieved). A trace providing this minimal cost then represents a schedule for the problem at hand.

A scheduling problem is about processing a certain number of entities, e.g. products. The processing is usually done by a one or more resource, which can perform tasks, provided, that the accompanying constraints are met. Furthermore, each task has an execution time ( [START_REF] Bozga | Scheduling Acyclic Branching Programs on Parallel Machines[END_REF] consider uncertain execution times). A certain goal should be reached, usually having completely processed a finite batch of entities. The question asked in scheduling is not mainly if this goal can be reached, but how efficiently. Using model checking tools, we are able to deal with complex industrial problems. We model tasks as transitions, meaning that performing task t i in an execution appears as s i ti --→ s i+1 in a state space model M, where s i and s i+1 are two states in the trace corresponding with the execution. In such state spaces, we can observe the following.

A function progress: S → N can be constructed, which accesses the state variables, using the specification of M, and quantifies the progress made to reaching some predetermined goal, e.g. having completely processed a given batch of entities. In general, say we have c 0 , c end ∈ N, ∀s ∈ S.c 0 ≤ progress(s) ≤ c end and progress(I) = c 0 , i.e. c 0 is the initial (no) progress and c end represents having reached the goal. Tasks may also lead a schedule further away from the goal.

For most scheduling problems, e.g. [START_REF] Abdeddaïm | Scheduling With Timed Automata[END_REF][START_REF] Behrmann | Efficient guiding towards cost-optimality in uppaal[END_REF][START_REF] Behrmann | Optimal scheduling using priced timed automata[END_REF][START_REF] Brinksma | Verification and Optimization of a PLC Control Schedule[END_REF][START_REF] Fehnker | Scheduling a Steel Plant with Timed Automata[END_REF][START_REF] Ruys | Optimal scheduling using Branch-and-Bound with SPIN 4.0[END_REF]112], typically B = {s ∈ S | progress(s) = c end }. One technique is to iteratively search M using a set of formulas, written in a temporal logic, such as LTL or µ-calculus. Placed in the context of DMC, cost-bounded model checking algorithm (Fig. 3) can be used to search M for a schedule, cheaper than the provided cost upper bound U .

Using this approach, one can iteratively search for increasingly good schedules. This has been done e.g. in Spin [START_REF] Ruys | Optimal scheduling using Branch-and-Bound with SPIN 4.0[END_REF] and Cadp [112]. In the latter case, costs are modelled in µCRL by means of additional actions. Iterative searching can be very inefficient, though, depending on the number of iterations needed. Depth-first branch-and-bound is based on the iterative search. Here, the upper bound in the formula is updated on-the-fly. The benefit of using this technique is that M only needs to be searched once, although it can still take a lot of resources. In Spin 4.0, this technique can be used by using C primitives [START_REF] Ruys | Optimal scheduling using Branch-and-Bound with SPIN 4.0[END_REF]. An update section in the model, written in C, is fired each time a counterexample is found, which updates the (hidden) minimal cost variable, changing the property to check.

In state spaces of the most basic scheduling problems, a liveness property φ that always a state e ∈ B can be reached holds. In other words, every schedule, i.e. trace, eventually leads to a successful finish. This fact means that DMC algorithms which aggressively prune and are therefore usually less effective for functional model checking can be very useful for finding schedules. Examples of such algorithms are nearest neighbour heuristic, which follows a single trace based on cumulated costs, and beam search [START_REF] Lowerre | The HARPY speech recognition system[END_REF][START_REF] Rubin | The ARGOS Image Understanding System[END_REF], which follows up to β traces, using cumulated costs and estimations. In functional model checking, if such searches do not return a counterexample, it is no guarantee that the property holds. In 'basic' scheduling, the worst we get are near-optimal solutions. In a more general setting, we consider the presence of unsuccessful termination, i.e. deadlocks e for which progress(e) = c end . See e.g. [103,111] Beam search (BS) has been applied to a whole range of scheduling problems [START_REF] Della Croce | A recovering beam search algorithm for the onemachine dynamic total completion time scheduling problem[END_REF][START_REF] Sabuncuoglu | Job shop scheduling with beam search[END_REF]100,103,111,112]. Two variants of BS are considered most classic: detailed and priority BS. Both versions use a beam width, to indicate the maximum number of states which may be expanded in each level of M. Detailed BS uses an evaluation function f (s) = a × b, where C(s, a) and H(s, b), to select up to β states. In priority BS adapted for general state spaces [103], outgoing transitions of each state are ordered by means of a priority function prio : T → Z. The beam width is represented by β = α l , where α is the maximum number of outgoing transitions explored per state in the first l levels of the search. In subsequent levels, only one transition is explored per state. One extension of BS is called flexible BS [103,112], where the beam width is not strongly fixed. In flexible detailed BS, tie-breaking is avoided in cases where there are not clearly β best states, and all competent candidates are explored. In arbitrary state space structures, this can improve the search a lot, since selections beyond the influence of the guiding function are avoided [103,110,111,112]. Another extension is a combination of Dijkstra's search and BS. The advantage of this extension over regular BS is that once a goal state has been found, the search can safely terminate [112].

Other settings which still largely remain to be investigated are multi-cost problems [START_REF] Behrmann | Optimal scheduling using priced timed automata[END_REF]110], infinite scheduling problems with or without nondeterministic product input, where the main difficulty is to determine what we are looking for, e.g. a single cycle, and what actually constitutes a 'best' schedule, and parallel scheduling problems where concurrent executions of tasks cannot be represented in an interleaved fashion ([112] contains an example dealing with this).

Conclusion

In the survey we have illustrated the algorithmic essentials of direct model checking, a recently proposed bug-finding paradigm for mitigating the state explosion problem. We have shown that it applies in a wide number of verification areas, and pointed to recent advances in AI search. Algorithms were presented in a general set-theoretic manner and instantiated to specific needs.

Meanwhile, directed model checking has become major branch of the techniques to cope with very large state spaces. The survey thus fills the gap left open by directed model checking not being mentioned in the most visible books like "Model Checking" [START_REF] Clarke | Model Checking[END_REF] and surveys like "25 Years of Model Checking" [START_REF]25 Years of Model Checking -History, Achievements, Perspectives[END_REF].

The currently envisioned future of directed model checking includes the design of refined heuristics [START_REF] Helmert | Flexible abstraction heuristics in optimal sequential planning[END_REF][START_REF] Helmert | Unifying the causal graph and additive heuristic[END_REF], relevance analysis to detect helpful and useless transitions [109], local search alternatives such as randomized guided search [START_REF] Rungta | Generating counter-examples through randomized guided search[END_REF]. large-scale disk-based search with refined delayed duplicate elimination strategies [START_REF] Barnat | Revisiting resistance speeds up I/O-efficient LTL model checking[END_REF][START_REF] Lamborn | Layered duplicate detection in external-memory model checking[END_REF][START_REF] Evangelista | Dynamic delayed duplicate detection for external memory model checking[END_REF], semi-external search incorporating space-efficient perfect hash function for a better time-space trade-off [START_REF] Edelkamp | Semi-external LTL model checking[END_REF][START_REF] Edelkamp | Flash-efficient LTL model checking with minimal counterexamples[END_REF], exploiting edges of current hardware technology such as addressing flash memory instead of magnetic devices [START_REF] Ajwani | Characterizing the performance of flash memory storage devices and its impact on algorithm design[END_REF][START_REF] Barnat | Can flash memory help in model checking?[END_REF][START_REF] Edelkamp | Flash-efficient LTL model checking with minimal counterexamples[END_REF], and parallel computation, especially the integration of multi-core processing [START_REF] Holzmann | The design of a multicore extension of the SPIN model checker[END_REF] and GPU computation [START_REF] Edelkamp | Model checking via delayed duplicate detection on the GPU[END_REF].

Fig. 1 .

 1 Fig. 1. Abstraction Directed Model Checking.

  For the latter we assume a static estimate relation H(s, b) that associates a state s with its estimate b ∈ A. A* selects elements with least estimated counterexample costs. In other words, Select A (Open) returns some s in Open with (s, a) ∈ C and (s, b) ∈ H such that for all s ′ in Open with (s ′ , a ′ ) ∈ C and (s ′ , b ′ ) ∈ H we have a × b a ′ × b ′ . The initialization and the cost updates to the cost relation C remain unchanged. For consistent heuristics the selection strategy of A* only considers settled states. More precisely, at each extraction of a state s with (s, a) ∈ C and (s, b) ∈ H from the Open-List we have a = δ(I, s) × b. At a bad state e ∈ B b is trivial, as H(e, 1).

  Procedure CostBoundedDirectedModelCheck Input: Model M = (S, T , I, L), set of bad states B, cost algebra A = A, ×, , 0, 1 , bound on cost U , cost relation C, estimate relation H Output: true if property satisfied on U cost-bounded paths or counterexample 1 Closed ← ∅; Open ← I 2 while (Open = ∅) 3 S ← SelectA(Open) 4

  Model M = (S, T , I, L), set of bad states B, cost algebra A = A, ×, , 0, 1 , bound on cost U , locality L, cost relation C, estimate relation H Output: true if property satisfied on U cost-bounded paths or counterexample 1 Succ ← I; for each k = 1, . . . , L Closed(k) ← ∅ 2 while (Succ = ∅) 3 Closed(0) ← Open ← Succ; Succ ← ∅ 4 while (Open = ∅) 5 S ← SelectA(Open) 6

Fig. 4 .

 4 Fig. 4. Directed Frontier Search Model Checking Algorithm.

Fig. 6 .

 6 Fig. 6. General Model Checking Algorithm for Timed Automata.

  for examples in this setting. Now, the aforementioned liveness property still holds, but B = {s ∈ S | progress(s) = c end ∨ enabled M (s) = ∅}. Here, let us call the goal states G = {s ∈ S | progress(s) = c end }. The BnB technique for Spin can be adapted to this setting by incorporating a secondary check in the C code, to ensure that a goal state has been found [110]. Pruning algorithms may lead to no solution at all, depending on the ratio | G |:| B \ G | and how promising the traces leading to states in B \ G initially appear to be, based on the guiding function. Besides improving the guiding function, with beam search, we can also counter this problem by increasing β, but of course, the penalty of this is less pruning.

  Heuristics in this area have traditionally been problem dependent, but Kupferschmid et al. introduced generic heuristics based on monotonicity relaxations and Model M = (S, T , I, L), set of bad states B, cost algebra A Output: true if property is satisfied or counterexample if not Succ| ∀s ′ ∈ Closed. s s ′ } 8 Open ← {s ∈ Open| ∀s ′ ∈ Succ. s s ′ } ∪ {s ∈ Succ| ∀s ′ ∈ Open.s s ′ } 9 return true

	Procedure ModelCheck
	Input: 1 Closed ← ∅; Open ← I 2 while (Open = ∅) 3 S ← SelectA(Open) 4 Open ← Open \ S; Closed ← Closed ∪ S 5 if (S ∩ B = ∅) return GeneratePath(S ∩ B) 6 Succ ← {s ′ | s ∈ S, (s, t, s ′ ) ∈ T }
	7	Succ ← {s ∈

Isotonicity is the key property of the algebra. It states that the order relation between the costs of any two paths is preserved if both of them are either prefixed or appended by a common, third, path. It has been shown that isotonicity is both necessary and sufficient for a generalized Dijkstra's algorithm to yield optimal paths [101].

Note that finding a shortest counterexample (as opposed to only a shortest fair cycle in the product of model and property automaton) requires an appropriate translation of the property into a Büchi automaton[START_REF] Schuppan | Shortest counterexamples for symbolic model checking of LTL with past[END_REF][START_REF] Schuppan | Liveness Checking as Safety Checking to Find Shortest Counterexamples to Linear Time Properties[END_REF] or dedicated algorithms[START_REF] Kupferman | Finding shortest witnesses to the nonemptiness of automata on infinite words[END_REF].