Minimal-Time Synthesis for Parametric Timed Automata

Timed Automata (TA) [2] extend finite automata with clocks, for instance to model real-time systems. Timed automata allow for reasoning about temporal properties of the designed system. In addition to reachability problems, it is possible to compute for TAs the minimal or maximal time required to reach a specific goal location. Such a result is valuable in practice, as it can describe the response time of a system or it may indicate when a component failure occurs.

It may not always be possible to describe a real-time system with a TA. There are often uncertainties in the timing constraints, for instance how long it takes between sending and receiving a message. Optimising specific timing delays to improve the overall throughput of the system may also be considered, as shown in Example 1. Such uncertainties can however be modelled using a parametric timed automaton (PTA) [3]. A PTA adds parameters, or unknown constants, to the TA formalism. By examining the reachability of a goal location, the parameters get constrained and we can observe which parameter valuations preserve the reachability of the goal location.

This process, also called parameter synthesis, is definitely useful for analysing reachability properties of a system. However, this technique does disregard timing aspects to some extent. Given the parameter constraints, it is no longer possible to give clear boundaries on the time to reach the goal, as this may depend on the parameter valuations. We focus on the parameter synthesis problem while reaching the goal location in minimal time, as demonstrated in Example 1.

Note that in other instances, the time to reach a goal location may be an interval, describing the lower- and upper-bound on the time. This can be achieved in the example by changing the travel time from train 1 to be between 95 and 105, by guarding the outgoing transitions from locations \(\texttt {A}'\), \(\texttt {B}'\), \(\texttt {C}'\) and \(\texttt {D}'\) with \(95 \le x_1 \le 105\) (instead of \(x_1 = 100\)). We focus on the lower-bound global time, meaning that we look at the minimal total time passed in the system, which may differ from the clock values as the clocks can be reset.

In this paper, we address the following problems:

For all stated problems we provide algorithms to solve them and empirically compare them with a set of benchmark experiments for PTAs, obtained from [5]. Interestingly, compared to standard reachability and synthesis, minimal-time reachability and synthesis is in general computed faster as fewer states have to be considered in the exploration. We also look at the computability and intractability of the problems for PTAs and L/U-PTAs (PTAs for which each parameter only appears as a lower- or upper-bound).

Related work. The earliest work on minimal-time reachability for timed automata was by Courcoubetis and Yannakis [17], who first addressed the problem of computing lower and upper bounds. Several algorithms have been developed since to improve performance [22, 24, 25], by e. g. using parallelism. Related problems have been studied, such as minimal-time reachability for weighted timed automata [4], minimal-cost reachability in priced timed automata [12], and job scheduling for timed automata [1].

Concerning parametric timed automata, to the best of our knowledge, the minimal-time reachability problem was not tackled in the past. The reachability-emptiness problem (“the emptiness of the parameter valuation set for which a given set of locations is reachable”) is undecidable [3], with various settings considered, notably a single clock compared to parameters [21] or a single rational-valued or integer-valued parameter [14, 21] (see [6] for a survey). Only severely limiting the number of clocks (e. g. [3, 11, 14, 16]), and often restricting to integer-valued parameters, can bring some decidability. Emptiness for the subclass of L/U-PTAs is also decidable [13]. Minimizing a parameter can however be considered done in the setting of upper-bound PTAs (PTAs in which the clocks are only restricted from above): the exact synthesis of integer valuations for which a location is reachable can be done [15], and therefore the minimum valuation of a parameter can be obtained.

We assume a set \(\mathbb {X}= \{ x_1, \dots , x_{|\mathbb {X}|}\} \) of clocks, i. e. real-valued variables that evolve at the same rate. A clock valuation is \(\nu _\mathbb {X}: \mathbb {X}\rightarrow {\mathbb {R}}_{\ge 0}\). We write \(\mathbf {0}\) for the clock valuation assigning 0 to all clocks. Given \(d \in {\mathbb {R}}_{\ge 0}\), \(\nu _\mathbb {X}+ d\) is the valuation s.t. \((\nu _\mathbb {X}+ d)(x) = \nu _\mathbb {X}(x) + d\), for all \(x\in \mathbb {X}\). Given \(R\subseteq \mathbb {X}\), we define the reset of a valuation \(\nu _\mathbb {X}\), denoted by \([\nu _\mathbb {X}]_{R}\), as follows: \([\nu _\mathbb {X}]_{R}(x) = 0\) if \(x\in R\), and \([\nu _\mathbb {X}]_{R}(x)=\nu _\mathbb {X}(x)\) otherwise.

We assume a set \(\mathbb {P}= \{ p_1, \dots , p_{|\mathbb {P}|}\} \) of parameters. A parameter valuation \(\nu _\mathbb {P}\) is \(\nu _\mathbb {P}: \mathbb {P}\rightarrow {\mathbb Q}_{+}\). We denote \({\bowtie } \in \{<, \le , =, \ge , >\}\), \({\triangleleft } \in \{<, \le \}\), and \({\triangleright \!} \in \{>, \ge \}\). A guard \(g\) is a constraint over \(\mathbb {X}\cup \mathbb {P}\) defined by a conjunction of inequalities of the form \(x\bowtie d\) or \(x\bowtie p\), with \(x\in \mathbb {X}\), \(d \in {\mathbb N}\) and \(p\in \mathbb {P}\). Given a guard \(g\), we write \(\nu _\mathbb {X}\models \nu _\mathbb {P}(g)\) if the expression obtained by replacing each clock \(x\in C\) appearing in \(g\) by \(\nu _\mathbb {X}(x)\) and each parameter \(p\in \mathbb {P}\) appearing in \(g\) by \(\nu _\mathbb {P}(p)\) evaluates to true.

We give \(\textsf {MinParamSynth}(\mathcal {A}, T, p)\) in Algorithm 1. It maintains a set \(\mathbf {W}\) of waiting symbolic states, a set \(\mathbf {P}\) of passed states, a current optimum \( Opt \) and the associated optimal valuations \(K\). While \(\mathbf {W}\) is not empty, a state is picked in line 6. If it is a target state (i. e. \(\ell \in T\)) then the projection of its constraint onto \(p\) is computed, and the minimum is inferred (line 10). If that projection improves the known optimum, then the associated parameter valuations \(K\) are completely replaced by the one obtained from the current state (i. e. the projection of \(C\) onto \(\mathbb {P}\)). Otherwise, if \(C{\downarrow _{\{p\}}}\) is equal to the known optimum (line 14), then we add (using disjunction) the associated valuations. Finally, if the current state is not a target state and has not been visited before, then we compute its successors and add them to \(\mathbf {W}\) in lines 17 and 18.

Note that if \(\mathbf {W}\) is implemented as a FIFO list with “pick” the first element, then this algorithm is a classical BFS procedure.

Also note that if we replace lines 10–15 with the statement \(K\leftarrow K\vee C{\downarrow _{\mathbb {P}}}\) (i. e. adding the parameter valuations to \(K\) every time the algorithm reaches a target location), we obtain the standard synthesis algorithm \(\textsf {EFSynth}\) from e. g.  [20], that synthesizes all parameter valuations for which a set of locations is reachable.

Algorithm 1 is a semi-algorithm; if it terminates with result \(K\), then \(K\) is a solution for the \(\textsf {MinParamSynth}\) problem. Correctness follows from the fact that the algorithm explores the entire parametric zone graph, except for successors of target states (from [19, 20] we have that successors of a symbolic state can only restrict the parameter constraint, hence we cannot improve). Furthermore, the minimum is tracked and updated whenever a target state is reached.

We show that synthesis can effectively be achieved for PTAs with a single clock, a decidable subclass.

For minimal-time reachability and synthesis, we assume that the PTA contains a global clock \(x_{ global }\) that is never reset. Otherwise, we extend the PTA by simply adding a ‘dummy’ clock \(x_{ global }\) without any associated guards, invariants or resets.

We give \(\textsf {MinTimeSynth}(\mathcal {A}, T, x_{ global })\) in Algorithm 2. We maintain a priority queue \(\mathbf {Q}\) of waiting symbolic states and order these by their minimal time (for the initial state this is 0). We further maintain a set \(\mathbf {P}\) of passed states, a current time optimum \(T_{ opt }\) (initially \(\infty \)), and the associated optimal valuations \(K\). We first explain the synthesis algorithm and then the reachability variant.

Minimal-time reachability synthesis. While \(\mathbf {Q}\) is not empty, the state with the lowest associated minimal time \(t\) is popped from the head of the queue (line 6). If this time \(t\) is larger than \(T_{ opt }\) (line 8), then this also holds for all remaining states in \(\mathbf {Q}\). Also all successor states from \(\mathbf {s}\) (or successors of any state from \(\mathbf {Q}\)) cannot have a better minimal time, thus we can end the algorithm.

Otherwise, if \(\mathbf {s}\) is a target state, we assume that \(t\nless T_{ opt }\) and thus \(t=T_{ opt }\) (we guarantee this property when pushing states to the queue). Before adding the parameter valuations to \(K\) in line 10, we intersect the constraint with \(x_{ global }= t\) in case the clock value depends on parameters, e. g. if \(C\) is \(x_{ global }= p\).⁴

If \(\mathbf {s}\) is not a target state, then we consider its successors in lines 12–18. We ignore states that have been visited before (line 13), and compute the minimal time of \(\mathbf {s}'\) in line 14. We compare \(t'\) with \(T_{ opt }\) in line 15. All successor states for which \(t'\) exceeds \(T_{ opt }\) are ignored, as they cannot improve the result.

If \(\mathbf {s}'\) is a target state and \(t' < T_{ opt }\), then we update \(T_{ opt }\). Finally, the successor state is pushed to the priority queue in line 18. Note that we preserve the property that \(t\nless T_{ opt }\) for the states in \(\mathbf {Q}\).

Minimal-time reachability. When we are interested in just a single parameter valuation, we may end the algorithm early. The algorithm can be terminated as soon as it reaches line 10. We can assert at this point that \(T_{ opt }\) will not decrease any further, since all remaining unexplored states have a minimal time that is larger than or equal to \(T_{ opt }\).

Algorithm 2 is a semi-algorithm; if it terminates with result \(( T_{ opt }, K)\), then \(K\) is a solution for the \(\textsf {MinTimeSynth}\) problem. Correctness follows from the fact that the algorithm explores exactly all symbolic states in the parametric zone graph that can be reached in at most \(T_{ opt }\) time, except for successors of target states. Note (again) that successors of a symbolic state can only restrict the parameter constraint. Furthermore, \(T_{ opt }\) is checked and updated for every encountered successor to ensure that the first time a target state is popped from the priority queue \(\mathbf {Q}\), it is reached in \(T_{ opt }\) time (after which \(T_{ opt }\) never changes).

We implemented all our algorithms in the IMITATOR tool [9] and compared their performance with the standard (non-minimization) \(\textsf {EFSynth}\) parameter synthesis algorithm from [20]. For the experiments, we are interested in analysing the performance (in the form of computation time) of each algorithm, and comparing that with the performance of standard synthesis.

Benchmark models. We collected PTA models and properties from the IMITATOR benchmarks library [5] which contains numerous benchmark models from scientific and industrial domains. We selected all models with reachability properties and extended these to include: (1) a new clock variable that represents the global time \(x_{ global }\), i. e. a clock that does not reset, and (2) a new parameter \(p_{ global }\) along with the linear term \(x_{ global }= p_{ global }\) for every transition that targets a goal location, to ensure that when minimizing \(p_{ global }\) we effectively minimize \(x_{ global }\). In total we have 68 models, and for every experiment we used the extended model that includes both the global time clock \(x_{ global }\) and the corresponding parameter \(p_{ global }\).

Subsumption. For each algorithm that we consider, it is possible to reduce the search space with the following two reduction techniques:

State inclusion is a relatively inexpensive computational task and preliminary results showed that it caused the algorithm to perform equally fast or faster than without the check. Checking for merging is however a computationally expensive procedure and thus should not be performed for every newly found state. For all BFS-based algorithms (standard synthesis and minimal-parameter synthesis) we merge every BFS layer. For the minimal-time synthesis algorithm, we empirically studied various merging heuristics and found that merging every ten iterations of the algorithm yielded the best results. We assume that both the inclusion and merging state-space reductions are used in all experiments (all computation times include the overhead the reductions), unless otherwise mentioned.

Run configurations. For the experiments we used the following configurations:Experimental setup. We performed all our experiments on an Core\(^\textsc {tm}\) i7-4710MQ processor with 2.50 GHz and 7.4GiB memory, using a single thread. The six run configurations were executed on each benchmark model, with a timeout of 3600 s. All our models, results, and information on how to reproduce the results are available on https://​github.​com/​utwente-fmt/​OptTime-TACAS19.

Results. The results of our experiments are displayed in Fig. 4.

\(\textsf {MTSynth}\) vs \(\textsf {EFSynth}\). We observe that for most of the models \(\textsf {MTSynth}\) clearly outperforms \(\textsf {EFSynth}\). This is to be expected since all states that take more than the minimal time can be ignored. Note that the experiments that appear on a vertical line between \(0.1s< x < 1s\) are a scaled-up variant of the same model, indicating that this scaling does not affect minimal-time synthesis. Finally, the model plotted at (1346, 52) does not heavily modify the clocks. As a consequence, \(\textsf {MTSynth}\) has to explore most of the state space while continuously having to extract the time constraints, making it inefficient.

\(\textsf {MPSynth}\) vs \(\textsf {EFSynth}\). We can see that \(\textsf {MPSynth}\) performs more similar to \(\textsf {EFSynth}\) than \(\textsf {MTSynth}\), which is to be expected as the algorithms differ less. Still, \(\textsf {MPSynth}\) significantly outperforms \(\textsf {EFSynth}\). This is also because fewer states have to be explored to guarantee optimality (once a parameter exceeds the minimal value, all its successors can be ignored).

\(\textsf {MTSynth}\) vs \(\textsf {MPSynth}\). Here, we find that \(\textsf {MTSynth}\) outperforms \(\textsf {MPSynth}\), similar to the comparison with \(\textsf {EFSynth}\). The results also show a second scalable model around (0.003, 10) and we see that \(\textsf {MPSynth}\) is able to solve the ‘bad performing model’ for \(\textsf {MTSynth}\) as quickly as \(\textsf {EFSynth}\). Still, we can conclude that the minimal-time synthesis problem is in general more efficiently solved with the \(\textsf {MTSynth}\) algorithm.

\(\textsf {MTSynth}\) vs MTSynth-noRed. Here we can see the advantage of using the inclusion and merging reductions to reduce the search space. For most models there is a non-existent to slight improvement, but for others it makes a large difference. While there is some computational overhead in performing these reductions, this overhead is not significant enough to outweigh their benefits.

\(\textsf {MTReach}\) vs \(\textsf {MTSynth}\). With \(\textsf {MTReach}\) we expect faster execution times as the algorithm terminates once a parameter valuation is found. The experiments show that this is indeed the case (mostly visible from the timeout line). However, we also observe that for quite a few models the difference is not as significant, implying that synthesis results can often be quickly obtained once a single minimal-time valuation is found.

\(\textsf {MPReach}\) vs \(\textsf {MPSynth}\). Here we also expect \(\textsf {MPReach}\) to be faster than its synthesis variant. While it does quickly solve six instances for which \(\textsf {MPSynth}\) timed out, other than that there is no real performance gain. We also argue here that synthesis is obtained quickly when a minimal parameter bound is found. Of course we are effectively computing a minimal global time, so results may change when a different parameter is minimized.

We have designed and implemented several algorithms to solve the minimal-time parameter synthesis and related problems for PTAs. From our experiments we observed in general that minimal-time reachability synthesis is in fact faster to compute compared to standard synthesis. We further show that synthesis while minimizing a parameter is also more efficient, and that existing search space reductions apply well to our algorithms.

Aside from the performance improvement, we deem minimal-time reachability synthesis to be useful in practice. It allows for evaluating which parameter valuations guarantee that the goal is reached in minimal time. We consider it particularly valuable when reasoning about real-time systems.

On the theoretical side, we did not address the minimal-parameter reachability problem for L/U-PTAs (we only showed intractability of the synthesis). While finding the minimal valuation of a given lower-bound parameter is trivial (the answer is 0 iff the target location is reachable), finding the minimum of an upper-bound parameter boils down to reachability-synthesis for U-PTAs, a problem that remains open in general (it is only solvable for integer-valued parameters [15]), as well as to shrinking timed automata [23], but with 0-coefficients in the shrinking vector—not allowed in [23].

A direction for future work is to improve performance by exploiting parallelism. Parallel random search could significantly speed up the computation process, as demonstrated for timed automata [24, 25]. Another interesting research direction is to look at maximizing the time to reach the target, or to minimize the upper-bound time to reach the target (e. g. for minimizing the worst-case response-time in real-time systems); a preliminary study suggests that the latter problem is significantly more complex than the minimal-time synthesis problem. One may also study other quantitative criteria, e. g. minimizing cost parameters.