Downward pattern refinement for timed automata

Model checking [4] is an automated approach for the verification of concurrent systems. For a given mathematical model \(\mathcal {M}\) of a system and a given property \(\varphi \), the objective of model checking is to prove that \(\mathcal {M}\) satisfies \(\varphi \), i. e., \(\mathcal {M}\models \varphi \). To prove this, common model checking algorithms perform a search in the state space that is induced by \(\mathcal {M}\), and check whether the induced state space satisfies \(\varphi \).

Complementary to proving that a mathematical model satisfies a property, an important practical aspect of model checking is bug finding, i. e., to detect reachable error states in faulty systems where \(\mathcal {M}\not \models \varphi \). This is important because during the development of systems, bugs do often occur, and therefore, effective and efficient approaches for bug finding are required. In addition, to be able to debug a system effectively, it is important to have short or preferably shortest possible error traces because short error traces are easier to understand than longer ones.

Directed model checking is a variant of model checking that is specifically optimized to find short error traces in faulty systems. Directed model checking has recently found much attention in different variants and contexts [9, 12, 14, 19, 22, 23, 30, 32, 34‐37]. For a given model \(\mathcal {M}\) of a system, the main idea is to focus the search on those parts of the state space of \(\mathcal {M}\) that appear to be promising to contain a reachable error state. The required information to guide the search accordingly is obtained from a distance heuristic. For each encountered state, distance heuristics estimate the distance to a nearest error state, where states with lower estimated error distance are preferably explored. Distance heuristics are usually based on abstractions of the original system and computed fully automatically. As shorter error traces are easier to understand than longer ones, ultimately shortest possible error traces are desired to effectively debug the system. Shortest possible error traces can be found with admissible distance heuristics, i. e., heuristics that never overestimate the real error distance, together with the A\(^*\) search algorithm [15, 16].

An important class of admissible distance heuristics is the class of pattern database heuristics. Pattern databases (PDBs) have originally been introduced in the area of Artificial Intelligence [5, 10]. More recently, PDBs have also been applied for directed model checking [23, 30]. To compute a PDB for a given system, a subset of the automata and variables of the original system (the so-called pattern) is selected, which determines a corresponding abstraction of the original system. The resulting PDB is defined as a data structure that contains the abstract state space of this abstraction together with the abstract error distances. Pattern databases can be used as a distance heuristic by estimating the error distance for a concrete state with the abstract error distance of the corresponding abstract state in the PDB. Obviously, the most crucial part in the design of a pattern database heuristic is the choice of the pattern, which determines the heuristic’s behavior and therefore the overall quality of the resulting heuristic. Ultimately, one seeks for patterns that are as small as possible (to be able to handle large systems) and that yield abstractions that are as “similar” to the original system as possible to appropriately reflect the original system behavior.

In recent years, directed model checking has particularly found increasing attention for finding bugs in concurrent systems of timed automata. The theory of timed automata [1] provides a formalism to model timed systems, which frequently occur in practice as embedded systems. In particular, timed systems often represent safety critical applications such as airbags or traffic light control systems. Obviously, especially for such safety critical systems, automated techniques are desired that help the engineer to systematically debug the system. However, model checking and specifically directed model checking becomes more difficult for such systems because of the clock variables that are real-valued and obey a special semantics. Although it is well-known that reachability is decidable for a certain class of timed automata (e. g., [3]), clocks generally cause an additional exponential blow-up of the state space that needs to be effectively addressed in order to make model checking approaches scalable for practically relevant timed automata systems.

In this paper, we present downward pattern refinement, a systematic approach to the pattern selection problem for concurrent systems of timed automata. We first present a general framework for pattern database heuristics in the context of timed automata, and particularly show that the resulting pattern database heuristic is consistent, which is a stronger property than admissibility and offers desirable properties that simplify the search algorithm [28]. Afterward, we present our downward pattern refinement approach as a mechanism for the pattern selection problem. The presentation of downward pattern refinement consists of two parts. In the first part, we present the underlying theory by identifying suitable criteria to estimate the quality of abstractions. For this purpose, we develop suitable criteria to estimate the similarity of systems. In the second part, based on these criteria, we present a pattern selection algorithm based on successively abstracting the original system as long as the resulting system remains similar according to these criteria (i. e., as long as only little spurious behavior is introduced). We have implemented downward pattern refinement and the corresponding architecture for pattern databases into our model checking tool Mcta [25, 36]. We demonstrate that downward pattern refinement can result in small patterns that still lead to very informed pattern database heuristics. This yields a powerful approach that is able to handle large problems that could not be solved optimally before. In particular, we show that the resulting pattern database heuristic recognizes many dead end states. Correctly identifying dead end states is useful to reduce the search effort significantly, since such states can be excluded from the search process without losing completeness. This even allows us to efficiently verify correct systems with abstraction-based directed model checking techniques.

Let us have a look at the relationship of directed model checking with abstraction-based distance heuristics to counter-example guided abstraction refinement (CEGAR). In contrast to CEGAR (which aims at computing accurate abstractions for proving or refuting a property), distance heuristics like PDBs can be computed based on abstractions that are not (yet) fine enough to entirely prove or refute the property—this is because for directed model checking, abstractions are used as the basis for a distance heuristic to guide the search. Accurate abstractions are expected to yield accurate search guidance, whereas coarse abstractions will possibly lead to rather uninformed search behavior. Overall, there is a relationship between the accuracy of the abstraction and the search behavior with the resulting distance heuristic. We will come back to this point later.

The remainder of the paper is organized as follows. In Sect. 2, we introduce the necessary background that is needed for this work, including the concepts of timed automata, directed model checking and pattern databases. Section 3 provides a generic framework for pattern databases when applied to timed automata. Based on these results, we present the theoretical basis for downward pattern refinement in Sect. 4. Based on this basis, we propose a corresponding pattern selection algorithm in Sect. 5. Our approach is evaluated within our Mcta model checker on large real-time benchmarks that stem from an industrial case study. The results show that our approach is able to outperform related approaches, including the state-of-the-art tool Uppaal [2, 26]. Finally, we conclude the paper and give a short outlook on future work.

We present the preliminaries that are needed for this work. These include the computational model in Sect. 2.1 and a detailed introduction to directed model checking in Sect. 2.2. Furthermore, we describe the general approach for pattern database heuristics in Sect. 2.3.

In Sect. 2.3, we have introduced the general framework that is commonly used for the construction of pattern database heuristics. However, for networks of timed automata, the problem about the mapping from a state \(s\) to a corresponding abstract state remained. In this section, we provide the formal basis to address and to solve this problem. We remark that, although this problem is related to other approaches as well that deal with pattern databases in the context of timed automata, the formal framework and theoretical results that we are going to present in this section have not been stated elsewhere so far.

For a pattern \(\mathcal {P}\) and a state \(s\), we define the set of abstract candidate states \(s^{\#}\) of the abstract system \({\mathcal {M}|}_{\mathcal {P}}\) aswhere dP \((s)\) denotes the discrete part of \(s\), i. e., a formula that expresses the valuation of \(s\) for the automata locations and integer variables, and Zone \((s)\) denotes the zone of \(s\). As we are dealing with timed automata, \( ACS (s)\) contains more than one element in general. Based on this definition, we define a pattern database heuristic for timed automata as follows.

In the following, we show that the resulting distance heuristic \(h^\mathcal {P}(s)\) is consistent. We remark that this result is also related to other approaches that deal with pattern databases and timed automata, but has not been stated elsewhere so far.

As a consequence of the above consistency result, states in the closed list of the algorithm shown in Fig. 1 do not have to be considered again in any case, as it is guaranteed that the priority value of states does not have to be updated in any case either. Furthermore, we will exploit this consistency result for our downward pattern refinement approach, which is described in the subsequent sections.

In this section, we describe the underlying theory that our pattern selection algorithm is based on. As already outlined, the selection of the pattern is crucial for the entire approach because the pattern determines the overall behavior of the resulting pattern database heuristic. Obviously, there is a tradeoff: pattern should be as small as possible (because the abstract state space of the corresponding abstraction has to be enumerated exhaustively to computed the pattern database), but should also reflect the original system as accurately as possible—in other words, the abstraction should be as “similar” to the original system as possible. An obvious question in this context is the question about similarity: What does it mean for a system to be “similar” to an abstract system? In the following, we derive precise, but computationally hard properties of similarity of abstract systems. Furthermore, we provide ways to efficiently approximate these properties in practice. These approximations lend themselves to a pattern selection algorithm, which will be described afterward in Sect. 5.

In the last section, we have provided the theoretical background for a pattern selection algorithm for timed automata: Based on the concepts provided by Definition 4 and Propositions 3,  4 and 6, we have derived tractable criteria to estimate the similarity of abstractions for the purpose of computing pattern database heuristics. Based on these criteria, we present the algorithm dprc (downward pattern refinement with clocks) in Fig. 3. The resulting pattern database heuristic is called \(h^ dprc \). Starting with a large pattern \(\mathcal {P}\), the focus of the dprc algorithm is to refine the current pattern by finding smaller patterns \(\mathcal {P'}\subseteq \mathcal {P}\) that yield pattern database heuristics \(h^{\mathcal {P'}}\) such that the resulting pattern satisfies the criteria from the last section. The algorithm is parametrized with a DMC problem, a distance heuristic \(h\) to compute relatively accurate abstractions, and a constant \(c\in \mathbb {N}\). To compute the pattern, the algorithms starts with the full pattern \(\mathcal {P}=\mathcal {M}\cup V\cup X\). If \(\mathcal {M}\) satisfies the preconditions of Proposition 4, we first remove clocks \(x\) if in every clock guard of every transition, \(x\) only occurs in simple clock constraints (line 2). Afterward, based on Proposition 6, we remove automata and integer variables that are safe in \(\mathcal {M}\) (line 3). Subsequently, motivated by Proposition 3, we try to find out the length \(d(s_0|_\mathcal {P},{\mathcal {M}|}_{\mathcal {P}})\) of a shortest error trace within \(c\) seconds in the resulting abstraction \({\mathcal {M}|}_{\mathcal {P}}\) (line 4). Therefore, we apply search in this abstraction (i. e., the algorithm given in Fig. 1). If it is possible to find such a shortest error trace, we check for every clock variable \(x\) if removing \(x\) yields a largely as informed distance heuristic as \(h^\mathcal {P}\); more precisely, we check if \(d(s_0|_\mathcal {P},{\mathcal {M}|}_{\mathcal {P}}) = d(s_0|_{\mathcal {P}\setminus \{x\}}, \mathcal {M}|_{\mathcal {P}\setminus \{x\}})\), and remove \(x\) from \(\mathcal {P}\) if this is the case (line 4–5). If it is not possible to identify \(d(s_0|_\mathcal {P},{\mathcal {M}|}_{\mathcal {P}})\) within \(c\) seconds, then we remove automata and variables that yield relatively accurate abstractions according to \(h\) (line 7–10) in order to get a smaller abstraction. In the resulting abstraction, we try again to find a shortest error trace within \(c\) seconds and remove the corresponding clock variables (line 11–13).

Directed model checking has found increasing attention in the last years. A survey on this topic is provided by Edelkamp et al. [14]. In particular, directed model checking has been applied to timed systems.

The most related approach to this work is probably the “Russian Doll” abstraction that has been proposed by Kupferschmid et al. [23]. In this approach, the pattern selection problem is addressed by computing an abstract error trace \(\pi \) using the so-called monotonicity abstraction [22], and then collecting all variables that occur in \(\pi \) for the pattern. The underlying idea is that variables that occur in the abstract error trace \(\pi \) are likely to be important for the abstract system as well. In contrast to our work, Kupferschmid et al. do not iteratively refine the pattern. A further approach based on pattern databases has been proposed by Qian and Nymeyer [30]. Starting with the variables that occur in the property \(\varphi \), Qian and Nymeyer select a pattern by using a cone-of-influence analysis up to a certain depth. The underlying assumption of this approach is that variables that are “closer” to \(\varphi \) in this sense are more important for the PDB, which is intuitively true for the variables that do occur in \(\varphi \). Moreover, pattern database heuristics have also been proposed in the more general setting of predicate abstraction by Smaus and Hoffmann [32]. More precisely, Smaus and Hoffmann use predicate abstraction (rather than projection abstractions) to generate the abstract state space. The pattern selection problem generalizes to the question, which predicates should be used for the abstraction. Smaus and Hoffmann propose to use abstraction refinement for this purpose.

In addition, PDB heuristics play an important role in the area of AI planning. For planning, PDB heuristics have been introduced by Edelkamp [10]. In addition, Haslum et al. [17] have provided a powerful algorithm for selecting pattern collections based on a search in the pattern space.

A further abstraction-based, but non-PDB approach called distance preserving abstractions has been proposed by Dräger et al. [8, 9]. For a concurrent system of timed automata, distance preserving abstractions are computed by successively computing the cross-product of two automata. This process is interleaved by merging states in the resulting abstraction to avoid the state explosion problem, where the merging is performed until a certain threshold provided by the user is no longer exceeded. This procedure is repeated until only one automaton is left, which represents the final abstraction. Distance heuristics based on distance preserving abstractions have been generalized to the area of automated planning by Helmert et al. [18]. In the planning community, such distance heuristics are called merge-and-shrink heuristics.

Apart from abstraction-based distance heuristics like PDB heuristics and the distance preserving abstraction heuristic, approaches based on other simplifications of the original system have been proposed. One of these approaches is based on the above-mentioned monotonicity abstraction proposed for directed model checking by Kupferschmid et al. [22]. First, let us remark that despite the name, the monotonicity abstraction is not an abstraction in the sense we described so far, but rather a relaxation of the original system semantics with the following underlying idea: System variables keep track of the values achieved so far, and transitions are applicable if there is a combination of so far achieved values such that the guards are satisfied. Starting in the current state \(s\), distance heuristics based on this approach iteratively apply all transitions that are applicable under this relaxed semantics until an error state or a fixed point is reached. Kupferschmid et al. propose the two distance heuristics \(h^ L \) and \(h^ U \) that exploit this principle in different ways. We remark that clock variables are ignored because their values trivialize rather quickly under this abstraction. More precisely, as soon as a location is reached with no invariant for clock \(x\) that restricts its values, the value range of \(x\) is equal to all nonnegative real values. A further distance heuristic based on analyzing the causal dependencies of the given system is proposed by Wehrle and Helmert [34]. This causal graph heuristic computes an approximation of the number of steps that are needed to achieve the faulty values of the variables that occur in the error property. For the computation, the corresponding steps that are needed to achieve the required values of the transitions’ preconditions are taken into account recursively. Again, the clock variables are ignored by the causal graph heuristic. A further simplification of the causal graph heuristic is proposed by Edelkamp et al. [12]. In this approach, the graph distance of automata that occur in the error property are considered, whereas other variables and synchronization behavior is ignored completely.

In addition, external search has been applied for model checking real-time systems. In this context, Edelkamp and Jabbar [11] have proposed three external search algorithms for priced timed automata, which they have implemented in the Uppaal Cora model checker.

In this section, we provide an experimental analysis of downward pattern refinement which we have implemented in the Mcta model checker. This model checker is described in more detail in Sect. 7.1. Furthermore, the benchmarks are described in Sect. 7.2. Finally, the experimental setup and results are presented in Sect. 7.3.

We have presented downward pattern refinement, a systematic approach to the pattern selection problem in the context of pattern database heuristics for concurrent systems of timed automata. Therefore, we have first provided the necessary theoretical framework for pattern databases and timed automata in general, and a formal basis for measuring the similarity of abstractions in particular. These theoretical results have been put into practice by the downward pattern refinement algorithm, which has shown superior performance compared to other directed model checking approaches as well as Uppaal on challenging real-time benchmarks of industrial size. In particular, as admissible distance heuristics like \(h^ dprc \) admit pruning power, we have been able to efficiently verify correct systems with directed model checking. This is particularly interesting because directed model checking has originally been proposed to efficiently guide the search to error states, rather than for proving correctness.

While the result of being able to efficiently proving correctness has been rather a side effect so far, it points us to interesting questions for future research. In particular, we observe the close relationship of computing accurate abstractions for verification (i. e., for proving correctness) and for falsification (i. e., for finding error states). As already outlined, a well-established technique to compute abstractions for the former case is counter-example-guided abstraction refinement (CEGAR). CEGAR has already been applied to compute distance heuristics for directed model checking [32] and for domain-independent planning [31]. However, apart from computing accurate distance functions for guiding the search, CEGAR has not yet been investigated for computing distance heuristics with the additional purpose of efficiently proving system correctness. In this context, an important research problem will be to investigate principled approaches for determining to which extent CEGAR should be performed in order to obtain accurate abstractions.