This article presents an extension of the method of [1] to time-triggered hybrid systems, providing over- and under-approximations of the set of reachable states. Our results on the vehicles platoon benchmark [2] compare favorably to the state of the art tools Flow* and SpaceEx, with more precise over-approximations. Moreover, we provide a measure of the approximation's accuracy using the ratio of under- to overapproximation.
Introduction and presentation of the platoon benchmark
X_ = AcX
timer c1 (b) Mode qc Leader
X_ = AnX Invariant timer c2 (c) Mode qn timer timer := timer timer := c01
Unlike in article [
We developed a prototype extending the method of [
To compute the continuous state in one mode of the system, we use a combination of a ne arithmetic [
Taylor model: A Taylor model of function x of t 2 [0; T ] is a pair (p; I) where p is a polynomial in t and I is a set called remainder (typically an interval) such that 8t 2 [0; T ]; x(t) 2 p(t) + I.
We improved the method of [
Moreover, in addition to over-approximations, our prototype is able to compute under-approximations (as will
be demonstrated in Section 3.3) following the algorithm of [
The prototype has been programmed in C++ with the library \aa ib" [
Flow*[
The original benchmark [
SpaceEx [
We now set c1 = c2 = c (same duration of communication and loss of communication) and we run multiple analyzes with various values for c, in [1; 10]. We also assume that the leader acceleration aL is uncertain but constant in [ 9; 1]. We x initial state variables to 0 (no spacing error and no acceleration), except for aL that is set to be the interval [ 9; 1]. As mentioned in section 1, each vehicle is described using 3 variables (the spacing error ei from the reference distance, the derivative of this error e_i and acceleration of the vehicule ai). We only present results for e1 as a function of time in this section, but we obtain similar results with e2 and e3.
We use an adaptative time step between 10 5 and 10 1 seconds, a remainder estimation of 10 8, a cuto threshold of 10 12 and a precision of 100 bits (for the MPFR library). These parameter values were obtained after several tests, in order to make the simulation successful (by reducing the time step) and reduce divergence (by adapting the cuto threshold and remainder estimation). To reduce divergence of the over-approximation, we increased the Taylor Model order up to 16. Results of simulations however still diverge after about 14 seconds as shown in Figure 4. Interestingly, the analysis takes more time with order 4 Taylor Models (we stopped it after 10 minutes) than order 16 for which results for same time horizon 17 were obtained in 106 seconds. We expect the analysis is re ning a lot the time step in order to try to control the increasing approximation error. 2All experiments can be downloaded on http://www.lix.polytechnique.fr/Labo/Francois.Bidet/ -1000 -100 -150
We used the STC Support Function with octagons, without set aggregation, an absolute owpipe tolerance of 1 and a relative of 0, a local time horizon of 5 s (for c < 5), a maximum number of iterations of 30, a relative error of 10 12 and an absolute error of 10 15. We reduced the absolute owpipe tolerance to 10 2 without signi cative di erence. We also used uniformly distributed directions instead of octagons (with 12 directions) but had to stop the simulation after about 10 minutes of computation (with less than 12 directions, we obtained an error). Figure 5 shows that the analysis behaves well for c = 3, but diverges for fast switching, that is with (a) c = 1, time horizon = 30 s (com- (b) c = 3, time horizon = 180 s putation time = 123 seconds) (computation time = 394 seconds) c = 1, con rming that some accuracy is lost in transitions.
As shown in Figure 6, our prototype was able to compute an over-approximation of e1 without signi cant divergence even when c is small, e.g. when c = 1. We used Taylor models of order 4, an adaptative time step between 10 5 s and 10 1 s, and a cuto threshold of 10 5 (for each a ne form, we regroup all noise terms with coe cient smaller than this threshold into a single noise term). The two analyzes represented in Figure 6 seem to reach an almost periodic behavior, which is the expected behavior.
For a switching time period c = 3, our prototype's over-approximation is slightly more accurate than that of SpaceEx but both are comparable. But when the switching frequency is higher (c = 1), our prototype is clearly more accurate than SpaceEx and Flow*. As already hinted, these tools lose precision when localizing and taking the time-triggered transitions.
A time comparison is di cult because we used order 4 Taylor models in our prototype and order 16 Taylor
model in Flow* (but the latter is faster than its own order 4 analysis with same other parameters). But we can
note that for c = 1, our analysis takes 36 seconds for time horizon 30, while Flow* takes 106 seconds for time
(a) c = 1, time horizon = 30 s (computation time 36 (b) c = 3, time horizon = 180 s (computation time
seconds) = 142 seconds)
horizon 15, for less accurate results. SpaceEx is running on a virtual machine with only 4Go of RAM against
8Go for our machine. In this setting, our prototype is between two and three times faster on this example.
In addition to the over-approximation, our prototype produces an under-approximation of the reachable states
(see the case of purely continuous systems in [
The under-approximation is useful as a complement of an over-approximation in many applications. It can be used to obtain a measure of precision of the approximation (e.g. the ratio of the under- to the overapproximations). It can also be used to invalidate some properties. Over-approximations ensure that if they do not intersect a set of \bad" states, then the systems' executions are safe. In the case of the platoon benchmark, such \bad" states are when the distances between two consecutive vehicles become negative (ei < dref;i). If the under-approximation intersects the set of bad states, then we are bound to run into an erroneous state, for some initial state. We can see on Figure 7b that if we x dref;3 11, we will never have a collision between vehicles 2 and 3 in the next 60 seconds following the acceleration of the leader aL 2 [ 9; 1] (over-approximation). Conversely, if we x dref;3 = 10, we are sure that there is a value of the acceleration of the leader aL 2 [ 9; 1] for which we will have a collision between vehicles 2 and 3 (under-approximation at time 7 seconds).
As in [
Our prototype is able to compute over-approximation of reachable states of time-triggered system faster and with more accuracy than Flow* and SpaceEx for a challenging benchmark (the platoon benchmark). This is because we use a combination of a ne arithmetic and Taylor models, with adaptative time steps, and because we use the time value as part of our Taylor models and not as an extra state variable, making guards for such time-triggered hybrid systems much simpler to interpret. The under-approximation allows us to refute hypotheses and to de ne an accuracy measure of our approximation as a ratio of under- to over-approximation's width.
We do not yet handle problems due to oating-point arithmetic. They potentially result in small errors on the over- and under-approximations' widths. This can be taken care of by carefully rounding (in the right direction) the a ne forms coe cients, this will be included in the prototype in the near future.
Another limitation of our prototype is the exact time of transition guards. The next step of our development
is the analysis of arbitrary switching, e.g. guards like t 2 [t1; t2] or t t1. Once done, we will be able to compare
our performance with other platoon models (arbitrary loss of communication or loss at nondeterministic times)
presented in [