Peter Schrammel
email: peter.schrammel@inria.fr

Bertrand Jeannet
email: bertrand.jeannet@inria.fr

Applying Abstract Acceleration to (Co-)Reachability Analysis of Reactive Programs

Keywords: Static Analysis, Acceleration, Abstract Interpretation, Linear Relation Analysis

Acceleration methods are commonly used for computing precisely the effects of loops in the reachability analysis of counter machine models. Applying these methods on synchronous dataflow programs, e.g. Lustre programs, requires to deal with the non-deterministic transformations due to numerical input variables. In this article we address this problem by extending the concept of abstract acceleration of Gonnord et al. to numerical input variables. Moreover, we describe the dual analysis for co-reachability. We compare our method with some alternative techniques based on abstract interpretation pointing out its advantages and limitations. At last, we give some experimental results.

Introduction

This article considers the reachability analysis of non-recursive, numerical programs represented by symbolic automata manipulating numerical variables, as illustrated in Fig. 1(a). More specifically, we focus on techniques enabling a precise analysis of selfloops that can be smoothly combined with methods for general numerical programs. For instance, considering the program of Fig. 1(a) with the set X 0 of initial values for the (a) X 0 The idea of acceleration is to accelerate cycles labelled by a function τ in the control structure of a program by computing the effect of its reflexive and transitive closure τ * = k≥0 τ k on a set of states X (the term "closure" refers to τ viewed as a relation). Applied to the program of Fig. 1(a), we obtain the program of Fig. 1(b). If the program is flat (i.e. it does not contain nested loops) and all loops can be accelerated, then the method is complete. If the program contains nested loops as in Fig. 1(a), the method is not complete any more; the standard heuristics is to enumerate and accelerate cycles (which form an infinite set) in the hope of terminating with the smallest fixed point after a finite number of steps. The same remark applies if transition functions in some cycles are too expressive to be accelerated. Acceleration has been mostly applied to automata manipulating integer variables using Presburger arithmetic [START_REF] Fribourg | Proving safety properties of infinite state systems by compilation into presburger arithmetic[END_REF]; [START_REF] Finkel | How to compose Presburger-accelerations: Applications to broadcast protocols[END_REF]; [START_REF] Bardin | FAST: Fast acceleration of symbolic transition systems[END_REF]), or FIFO queues using subclasses of regular expressions [START_REF] Boigelot | Symbolic verification of communication protocols with infinite state spaces using QDDs[END_REF]; [START_REF] Abdulla | Using forward reachability analysis for verification of lossy channel systems[END_REF]).

l 0 l 1 p ≤ 20 p = p+1 τ : 2x 1 +2x 2 ≤ p 0 ≤ ξ ≤ 1 → x ′ 1 = x 1 +ξ+1 x ′ 2 = ξ p ′ = p (b) X 0 l 0 l ′ 1 l 1 (c) X 0 = (x 1 , x 2 , p) 0 ≤ x 1 ∧ 1 ≤ x 2 x 1 +x 2 ≤ 2 ∧ p = 3 p ≤ 20 τ * p = p+1
Widening basically extrapolates the limit of a sequence of abstract invariants without referring to the program that generates them, whereas acceleration uses the structure of the program to perform an exact extrapolation. [START_REF] Gonnord | Combining widening and acceleration in linear relation analysis[END_REF] have proposed the concept of abstract acceleration which combines these approaches: wherever possible, simple loops are accelerated in the abstract domain, and in any other cases (multiple self-loops, nested loops, too expressive transitions) one resorts to the use of widening to guarantee the convergence of the fixed point computation at the cost of over-approximations.

Applying acceleration to reactive programs. Many acceleration techniques such as those introduced by [START_REF] Leroux | Algorithmique de la vérification des systèmes à compteurs -approximation et accélération -implémentation dans l'outil FAST[END_REF]; [START_REF] Bardin | FAST: Fast acceleration of symbolic transition systems[END_REF]; [START_REF] Gonnord | Combining widening and acceleration in linear relation analysis[END_REF] consider automata with transition functions in the form of guarded actions

τ : g(x) guard → x ′ = f (x) action x, x ′ ∈ R n (1)
However, reactive programs such as Lustre data-flow programs interact with their environment: at each computation step they have to take into account the value of input variables, which typically correspond to values acquired by sensors.

Boolean input variables can be encoded in an automaton by finite non-deterministic choices but numerical input variables demand a more specific treatment. Indeed, they induce transition functions of the form

τ : g(x, ξ) → x ′ = f (x, ξ) x, x ′ ∈ R n ξ ∈ R p (2)
that depends on both state variables x and numerical input variables ξ. This article addresses specifically this point, by extending the abstract acceleration concept introduced by [START_REF] Gonnord | Combining widening and acceleration in linear relation analysis[END_REF] to systems with numerical inputs. The methods developped in this article can also be seen as an alternative to acceleration methods-based on the computation of transitive closures of affine relations (rather than functions) [START_REF] Beletska | Computing the transitive closure of a union of affine integer tuple relations[END_REF]; [START_REF] Bozga | Fast acceleration of ultimately periodic relations[END_REF]). Indeed, transition functions with inputs can be viewed as relations between states defined as

R(x, x ′ ) = ∃ξ : g(x, ξ) ∧ x ′ = f (x, ξ) (3)
Contributions and outline. Our first two contributions are extensions of the abstract acceleration concept as introduced by [START_REF] Gonnord | Combining widening and acceleration in linear relation analysis[END_REF] in two directions: (i) We consider open systems, i.e., with numerical inputs, instead of closed systems; in particular we show how to accelerate loops where translations and resets depend on inputs, provided that the guard of the loop constrains separately state and input variables. (ii) We also extend abstract acceleration techniques from forward (reachability) analysis to backward (co-reachability) analysis. In consequence, it possible to apply the abstract acceleration concept to related, but slightly different problems in verification, such as parameter synthesis for example. Moreover, experience shows that combining forward and backward analyses is very useful in the context of abstract interpretation (e.g. [START_REF] Jeannet | Dynamic partitioning in linear relation analysis. application to the verification of reactive systems[END_REF]). A third contribution is (iii) a detailed comparison of the abstract acceleration approach to the derivative closure approach of [START_REF] Ancourt | A modular static analysis approach to affine loop invariants detection[END_REF], which is related to methods based on transitive closures of relations. This article extends the results presented by [START_REF] Schrammel | Extending abstract acceleration to data-flow programs with numerical inputs[END_REF] with the contributions (ii) and (iii).

After some preliminaries in Section 2 about the considered program model, operations on convex polyhedra and the general analysis framework that we use for verification, we recall the main results of abstract acceleration in Section 3. Section 4 extends abstract acceleration techniques to systems with numerical input variables, in the context of forward analysis. Section 5 extends these results to backward analysis. Section 6 is dedicated to a comparison with other methods. Section 7 gives an overview and some experimental results on how to apply abstract accleration to logico-numerical programs. After a discussion of further related work in Section 8, we conclude in Section 9.

Analysis of Logico-Numerical Programs

Program model. We assume a set V of variable names. We consider in this article programs modeled as numerical automata (L, x, ξ, l 0 , X 0 , T ) where

• L is a finite set of locations, x ∈ V n a vector of real-valued state variables, and ξ ∈ V p a vector of real-valued input variables; • l 0 is the initial location and X 0 ⊆ R n is the set of initial values for state variables

x at location l 0 ; • T is a finite set of transitions of the form t : (l, l ′ , τ ) where l and l ′ are respectively the origin and destination locations, and τ is a (partial) transition function of the form g(x, ξ) → x ′ = f (x, ξ).

An execution of such a system is a sequence (l 0 , x 0 )

t0,ξ 0 ---→ . . . (l k , x k ) t k ,ξ k ---→ . . . such that x 0 ∈ X 0 and for any k ≥ 0, t k = (l k , l k+1 , τ k ) and x k+1 = τ k (x k , ξ k ).
This program model includes various models of counter automata [START_REF] Comon | Multiple counters automata, safety analysis and presburger arithmetic[END_REF]; [START_REF] Bardin | Flat acceleration in symbolic model checking[END_REF]). It can also be obtained from Lustre synchronous data-flow programs by (1) taking the output of their front-end compilation process, (2) performing on this output a partial evaluation [START_REF] Jones | Partial Evaluation and Automatic Program Generation[END_REF]) of all Boolean state variables (which are then encoded in control locations), and (3) eliminating Boolean input variables using non-deterministic choices. The partition refinement mechanics implemented in the NBac tool [START_REF] Jeannet | Dynamic partitioning in linear relation analysis. application to the verification of reactive systems[END_REF]) are capable of achieving this task and have been employed for connecting the Aspic tool [START_REF] Gonnord | Accélération abstraite pour l'amélioration de la précision en analyse des relations linéaires[END_REF][START_REF] Gonnord | The ASPIC tool: Accelerated symbolic polyhedral invariant computation[END_REF]) to Lustre, for example.

Convex Polyhedra. We use in this article the abstract domain of convex polyhedra for representing invariants on numerical variables. Convex polyhedra can be represented either as a conjunction of constraints denoted by

Ax ≤ b with x ∈ R n , A ∈ R m×n , b ∈ R m
or as the set of vectors generated by a vector of vertices V = (v 1 . . . v p ) ∈ R n×p and rays R = (r 1 . . . r q ) ∈ R n×q , denoted by (V, R):

{x | ∃λ, µ ≥ 0 : i λ i = 1 ∧ x = Vλ + Rµ}
We can convert from one representation to the other one (see [START_REF] Fukuda | Double description method revisited[END_REF]). We will use the same notation for polyhedra X interexchangeably for both the predicate X(x) = (Ax ≤ b) and the set X = {x | Ax ≤ b}. We briefly remind some classical operations described e.g. by [START_REF] Halbwachs | Verification of real-time systems using linear relation analysis[END_REF]:

The constraint representation is used for computing the intersection ⊓ of two polyhedra (i.e. the conjunction of their constraints) and the inverse image τ -1 (X) of a polyhedron X = (Ax ≤ b) by an affine assignment τ :

x ′ = Cx + d, i.e. τ -1 (X) = (ACx ≤ b -Ad).
The generator representation is used for computing the convex hull (union) ⊔ of two polyhedra (i.e. the union of their generators), the projection of dimensions, and the image τ (X) of a polyhedron X = (V, R) by an affine assignment τ :

x ′ = Cx + d: τ (X) = (CV + (d . . . d p times
)), CR .

Mind that the intersection of two convex polyhedra is again a convex polyhedron: X ∩ Y = X ⊓ Y . In contrast, the union of two convex polyhedra is not convex in general. For that reason the convex hull, i.e. an over-approximation, is used instead of the ordinary union for sets:

X ∪ Y ⊆ X ⊔ Y
The time elapse operation, defined as

X ր D = {x + td | x ∈ X, d ∈ D, t ∈ R ≥0 } can be implemented using the systems of generators (V X , R X ) and (V D , R D ) of the polyhedra X and D: (V X , R X ∪ V D ∪ R D ) is a system of generators for X ր D. The Minkowski sum (see de Berg et al. (2008)) of two polyhedra X = X 1 + X 2 is defined by X(x) = ∃x 1 , x 2 : (x = x 1 +x 2 ) ∧ X 1 (x 1 ) ∧ X 2 (x 2 ).
⊤ and ⊥ denote the polyhedra R n and ∅ respectively. Concerning the complexity, the translation between the two representations may be exponential in the number of dimensions n (see [START_REF] Fukuda | Double description method revisited[END_REF]), hence any composition of basic operations requiring both representations has a worst-case exponential complexity.

Note that the operations defined on generators can also be computed using only systems of constraints and projection as shown by [START_REF] Benoy | Computing convex hulls with a linear solver[END_REF]. However, this does not allow to improve the worst-case complexity.

Overview of Acceleration and Abstract Acceleration

As mentioned in the introduction, the idea of acceleration (Fig. 1) is to replace a self-loop τ by an ordinary transition τ * that is the reflexive and transitive closure of τ . Abstract acceleration introduced by [START_REF] Gonnord | Combining widening and acceleration in linear relation analysis[END_REF] and [START_REF] Gonnord | Accélération abstraite pour l'amélioration de la précision en analyse des relations linéaires[END_REF] relaxes exact acceleration in the sense that it aims at approximating the exact set τ * (X) by a convex polyhedron τ ⊗ (X) ⊇ τ * (X) that is close to the convex hull of the exact

search stop s > 2 ∨ t > 3 σ ∧ s ≤ 2 ∧ t ≤ 3 → s ′ = 0; t ′ = t + 1 µ ∧ s ≤ 2 ∧ t ≤ 3 → s ′ = s + 1; d ′ = d + 1 s ′ = 0; t ′ = 0; d ′ = 0
Fig. 2. Example: A robot car safety controller. The lower loop means: When a "meter" signal µ is received the speed estimation s and the distance d are incremented: this transition is a translation. On the contrary, the upper loop is a translation with resets: when a "second" signal σ is received the speed estimation is reset and the time t is incremented. If the speed is above 2m/s or no input signal has been received for 3s then the car is stopped.

set. This method is also inspired by the time elapse operator used in timed or in hybrid automata [START_REF] Halbwachs | Verification of real-time systems using linear relation analysis[END_REF]).

Following the notations of Section 2, a self-loop τ has the structure: G → A meaning "while guard G do action A". Generally, acceleration methods for numerical variables x deal with transitions of the form

Ax ≤ b → x ′ = Cx + d (4)
where Ax ≤ b represents a conjunction of linear constraints defining a convex polyhedron, and

x ′ = Cx + d is an affine transformation; C is a square matrix. A transition is called • a reset iff C is the zero matrix,
• a translation iff C is the identity matrix,

• a translation with resets (or translation/reset) iff C is a diagonal matrix with zeros and ones only, • a periodic affine transformation iff ∃p > 0, ∃l > 0 :

C p+l = C p ,
• a general affine transformation otherwise. Existing acceleration methods do not address general affine transformations. We will not consider in this paper the case of periodic affine transformations, but we discuss the generalization of our results to this case in the conclusion.

Fig. 2 shows an example of a simplistic safety controller for a robot car (cf. [START_REF] Halbwachs | Verification of real-time systems using linear relation analysis[END_REF]; [START_REF] Ancourt | A modular static analysis approach to affine loop invariants detection[END_REF]). The car should follow a given track, but in case it has lost the track it should keep on searching the track for a while before being stopped. This example illustrates two of the above types of transitions.

In the context of abstract acceleration, [START_REF] Gonnord | Combining widening and acceleration in linear relation analysis[END_REF] show that translations and translations with resets can be accelerated as follows:

Theorem 1 (Translations, [START_REF] Gonnord | Accélération abstraite pour l'amélioration de la précision en analyse des relations linéaires[END_REF]). Let τ be a translation G → x ′ = x + d, then for every convex polyhedron X, the convex polyhedron

τ ⊗ (X) = X ⊔ (X ⊓ G) ր {d} ⊓ (G + {d}) is a convex over-approximation of τ * (X). 0 1 2 3 4 0 1 2 3 4 5 x 1 x 2 τ ⊗ (X)
X G d Fig. 3. Abstract acceleration of a translation (Ex. 1) by vector d starting from X (dark gray) resulting in τ ⊗ (X) (whole shadowed area).

0 1 2 3 4 0 1 2 3 4 5 x 1 x 2 τ ⊗ (X) X τ (X) G Fig. 4
. Abstract acceleration of a translation with resets (Ex. 2) starting from X (dark gray): τ (X) (bold line) and result τ ⊗ (X) (whole shadowed area).

Example 1 (Translation). (see Fig. 3)

τ : x 1 +x 2 ≤ 4 ∧ x 2 ≤ 3 G →   x ′ 1 x ′ 2   =   x 1 x 2   +   2 1   d Starting from X = (0 ≤ x 1 ≤ 1 ∧ 0 ≤ x 2 ≤ 4) we compute τ ⊗ (X): X ⊓ G = (0 ≤ x 1 ≤ 1 ∧ 0 ≤ x 2 ≤ 3) (X ⊓ G) ր {d} =    x 1 ≥ 0 ∧ x 2 ≥ 0 ∧ x 1 -2x 2 ≥ -6 ∧ -x 1 +2x 2 ≥ -1) ((X ⊓ G) ր {d}) ⊓ (G + {d}) =    x 1 ≥ 0 ∧ 0 ≤ x 2 ≤ 4 ∧ x 1 -2x 2 ≥ -6 ∧ -x 1 +2x 2 ≥ -1 ∧ x 1 +x 2 ≤ 7 τ ⊗ (X) =    x 1 ≥ 0 ∧ 0 ≤ x 2 ≤ 4 ∧ -x 1 +2x 2 ≥ -1 ∧ x 1 +x 2 ≤ 7
Theorem 2 (Translations with resets, [START_REF] Gonnord | Accélération abstraite pour l'amélioration de la précision en analyse des relations linéaires[END_REF]). Let τ be a translation with resets G → x ′ = Cx + d, then for every convex polyhedron X, the convex polyhedron

τ ⊗ (X) = X ⊔ τ (X) ⊔ (τ (X) ⊓ G) ր {Cd} ⊓ (G + {Cd})
is a convex over-approximation of τ * (X).

Example 2 (Translation with resets). (see Fig. 4)

τ : x 1 +x 2 ≤ 4 ∧    x ′ 1 = x 1 +2 x ′ 2 = 1 Starting from X = (0 ≤ x 1 ≤ 3 ∧ 2 ≤ x 2 ≤ 3) we compute τ ⊗ (X): τ (X) = (2 ≤ x 1 ≤ 4 ∧ x 2 = 1) τ (X) ⊓ G = (2 ≤ x 1 ≤ 3 ∧ x 2 = 1) (τ (X) ⊓ G) ր {Cd} = (x 1 ≥ 2 ∧ x 2 = 1) ((τ (X) ⊓ G) ր {Cd}) ⊓ (G + {Cd}) = (2 ≤ x 1 ≤ 5 ∧ x 2 = 1) τ ⊗ (X) =    x 1 ≥ 0 ∧ 1 ≤ x 2 ≤ 3 ∧ x 1 +2x 2 ≥ 4 ∧ x 1 +x 2 ≤ 6
Remark 1. Theorem 2 exploits the property that a translation with resets to constants iterated N times is equivalent to the same translation with resets, followed by a pure translation iterated N -1 times. Hence the structure of the obtained formula Remark 2. Ideally, τ ⊗ (X) as defined in Theorems 1 and 2 should be the best overapproximation of τ * (X) by a convex polyhedron. This is not the case as shown by the following example in one dimension. Let X = [1, 1] and τ : , 6], whereas the best convex over-approximation of τ * (X) = {1, 3, 5} is the interval [1,5]. This is because the operations involved in the definition of τ ⊗ (X) manipulate dense sets and do not take into account arithmetic congruences. In this article we will not improve in this respect, but we will point out in our proofs where this dense approximation takes place, and we discuss in Section 9 how the linear congruences abstract domain mentioned in the introduction can be exploited to improve on this point.

x 1 ≤ 4 → x ′ 1 = x 1 + 2. τ ⊗ (X) = [1

Abstract Acceleration with Numerical Inputs

We now extend numerical abstract acceleration by numerical input variables ξ. We consider transitions τ of the form1

  A L 0 J     x ξ   ≤   b k   Ax+Lξ≤b ∧ Jξ≤k → x ′ = C T   x ξ   + u Cx+Tξ+u (5)
General and simple guards. The following proposition shows the challenge raised by adding inputs:

Proposition 1 (General guards and general affine transformations). Any general affine transformation without inputs Ax ≤ b → x ′ = Cx + d can be expressed -as a "reset with inputs"

(Ax ≤ b ∧ ξ = Cx + d) → x ′ = ξ,
-as well as a "translation with inputs" (Ax

≤ b ∧ ξ = (C-I)x + d) → x ′ = x + ξ.
This means that there is no hope to get precise acceleration for such resets or translations with inputs, unless we know how to accelerate precisely general affine transformations without inputs, which is out of the scope of the current state of the art.

Nevertheless, we can accelerate transitions with inputs if the constraints on the state variables do not depend on the inputs, i.e., the guard is of the form Ax ≤ b ∧ Jξ ≤ k, i.e., when L = 0 in Eqn. ( 5). We call the resulting guards simple guards.

In the following, we show how to accelerate translations and translations with resets with simple guards. We provide in §4.3 an over-approximation of our results for general guards.

Translations with Inputs and Simple Guards

Definition 1. Translations with inputs and simple guards are defined as

  A 0 0 J     x ξ   ≤   b k   Ax ≤ b G ∧ Jξ≤k → x ′ = I T   x ξ   + u x+Tξ+u
The first step we perform is to reduce such a translation with inputs to a polyhedral translation τ :

G → x ′ = x + D and defined by τ (X) = (X ⊓ G) + D.
Proposition 2 (Translation with inputs = polyhedral translation). A translation τ with inputs and a simple guard (Def. 1) is equivalent to a polyhedral translation defined by

G → x ′ = x + D with D = {d | ∃ξ : d = T ξ + u ∧ J ξ ≤ k} (D can be computed by standard polyhedra operations.) Proof. x ′ ∈ τ (X) ⇐⇒ ∃x ∈ X, ∃ξ : Ax ≤ b ∧ Jξ ≤ k ∧ x ′ = x + Tξ + u ⇐⇒ ∃x ∈ X ⊓ G, ∃ξ, ∃d : Jξ ≤ k ∧ d = Tξ + u ∧ x ′ = x + d ⇐⇒ ∃x ∈ X ⊓ G, ∃d ∈ D : x ′ = x + d with D = {d | ∃ξ : Jξ ≤ k ∧ d = Tξ + u} 2
We now generalize Thm. 1 from ordinary translations to polyhedral translations.

Proposition 3 (Polyhedral translation). Let τ be a polyhedral translation G → x ′ = x + D. Then, the set τ ⊗ (X) = X ⊔ τ (X ⊓ G) ր D is a convex over-approximation of τ * (X). Proof. x ′ ∈ k≥1 τ k (X) ⇐⇒ x ′ ∈ τ ( k≥0 τ k (X)) ⇐⇒ ∃k ≥ 0, ∃x 0 ∈ X, ∃x k , ∃d 1 . . . d k ∈ D :          x ′ ∈ τ (x k ) x k = x 0 + k j=1 d j G(x 0 ) ∧ ∀k ′ ∈ [1, k] : G(x 0 + k ′ j=1 d j ) ⇐⇒ ∃k ≥ 0, ∃x 0 ∈ X, ∃x k , ∃d ∈ D : x ′ ∈ τ (x k ) ∧ x k = x 0 + kd ∧ G(x 0 ) ∧ G(x k ) (because D and G are convex, see Rem. 3) =⇒ ∃α ≥ 0, ∃x 0 ∈ X, ∃x k , ∃d ∈ D : x ′ ∈ τ (x k ) ∧ x k = x 0 + αd ∧ G(x 0 ) (dense approximation; G(x k ) implied by x ′ ∈ τ (x k )) ⇐⇒ ∃x 0 ∈ X ⊓ G, ∃x k : x ′ ∈ τ (x k ) ∧ x k ∈ ({x 0 } ր D) ⇐⇒ x ′ ∈ τ ((X ⊓ G) ր D) 2
Mind that the only approximation takes place in the line (⇒) where the integer coefficient k ≥ 0 is replaced by a real coefficient α ≥ 0. This is the technical explanation of Rem. 2.

Remark 3 (Convexity argument). For any k loop iterations with d 1 , . . . ,

d k ∈ D s.t. ∀k ′ ∈ [0, k] : G(x + k ′ j=1 d j ) we have ∃d ∈ D, ∃α ≥ 0 : G(x) ∧ G(x + αd) s.t. k j=1 d j = αd: any intermediate point x + αd must be in G, because G is convex; moreover α ≥ 0 and a vector d ∈ D actually exist: for example, take α = k and d = 1 k k j=1 d j , which is in D because D is convex.
Remark 4 (Inputs vs. constants). One might think that Thm. 1 can be applied directly by accelerating the transition for each d ∈ D and taking the union, i.e. computing τ ⊗ (X) by X ⊔ d∈D X d with

X d = (X ⊓ G) ր {d} ⊓ (G + {d}).
However, this formula is not correct for the last step beyond the guard, which is illustrated in the figure on the right-hand side for a polyhedral translation with

X = {(0, 0)}, D = (0 ≤ d 1 ≤ 1 ∧ d 2 = 1) and the guard G given in the 0 1 2 0 1 2 x 1 x 2 G figure.
For the step crossing the guard, e.g. at (2, 2), there is actually a choice among all values in D (correct abstract acceleration: whole shadowed area), whereas the wrong acceleration (dark gray) considers only the vector d = (1, 1) which led to (2, 2).

We combine Propositions 2 and 3 to formulate the following theorem:

Theorem 3 (Translation with inputs and simple guards). Let τ be a translation with inputs and a simple guard

τ : (Ax ≤ b G ) ∧ (Jξ ≤ k) → x ′ = x + Tξ + u Then, the set τ ⊗ (X) = X ⊔ τ (X ⊓ G) ր D with D = {d | ∃ξ : d = T ξ + u ∧ J ξ ≤ k} is a convex over-approximation of τ * (X).
Proof. Follows directly from Prop. 2 and 3. 2 Example 3 (Translation with inputs and simple guards). Consider the polyhedron X = {(x 1 , x 2 ) | 0 ≤ x 1 ≤ x 2 ≤ 1} and the transition τ : 6. Precision loss in example 3 when using the approximate formula according to Rem. 5.

x 1 + x 2 ≤ 4 1 ≤ ξ ≤ 2 → x ′ 1 = x 1 + 2ξ -1 x ′ 2 = x 2 + ξ Eliminating the inputs as in Proposition 2 yields D = {(d 1 , d 2 )|1 ≤ d 1 ≤ 3 ∧ -d 1 +2d 2 = 1}, see
(x 1 , x 2 )|x 1 ≥ 0 ∧ -x 1 +x 2 ≤ 1 ∧ x 1 +x 2 ≤ 9 ∧ -2x 1 +4x 2 ≤ 9 ∧ 2x 1 -3x 2 ≤ 0}. d 1 d 2 ξ 1 1 D J ξ ≤k x 1 x 2 1 1 X τ ⊗ (X) G
1 x 2 1 1 X τ ⊗ (X) G G + D Fig.
Remark 5 (Alternative, less precise formula). In analogy to Thm. 1, we could alternatively consider the formula

X ⊔ ((((X ⊓ G) ր D) ⊓ (G + D)).
In order to justify this, we extend the proof of Proposition 3 by continuing at the label (dense approximation):

⇐⇒ ∃α ≥ 0, ∃x 0 ∈ X ⊓ G, ∃x k , ∃d, d ′ ∈ D : x ′ = x k +d ′ ∧ x k = x 0 +αd ∧ G(x k ) ⇐⇒ ∃α ≥ 0, ∃x 0 ∈ X ⊓ G, ∃d, d ′ ∈ D : x ′ = x 0 +αd+d ′ ∧ G(x ′ -d ′ ) =⇒ ∃α ≥ 0, ∃x 0 ∈ X ⊓ G, ∃d, d ′ ∈ D : x ′ = x 0 +αd+d ′ ∧ ∃d ′ ∈ D : G(x ′ -d ′ ) ⇐⇒ ∃α ′ ≥ 1, ∃x 0 ∈ X ⊓ G, ∃d ′′ ∈ D : x ′ = x 0 +α ′ d ′′ ∧ ∃d ′ ∈ D : G(x ′ -d ′ ) =⇒ x ′ ∈ (X ⊓ G) ր D ∧ x ′ ∈ (G + D) using {x | ∃d ∈ D ∧ G(x-d)} = {z+d | d ∈ D ∧ G(z)} = (G + D).
It can be observed that for the translation of example 3 the latter formula results in an over-approximation (see Fig. 6) as compared to the result in Fig. 5. This reflects the additional approximation steps in the proof indicated by (=⇒).

Translations/Resets with Inputs and Simple Guards

Definition 2. Translations/resets with inputs and simple guards are defined as

  A 0 0 J     x ξ   ≤   b k   Ax≤b ∧ Jξ≤k → x ′ = C T   x ξ   + u Cx+Tξ+u
where C is a diagonal matrix with C i,i ∈ {0, 1} for all i.

Notations. Let C ′ = I -C, then we can decompose any vector x in Cx + C ′ x. We denote Cx = x t,0 a vector where the reset dimensions are set to zero, and C ′ x = x 0,r a vector where the translated dimensions are set to zero. We extend such notations to sets: X t,0 = {x t,0 | x ∈ X} and X 0,r = {x 0,r | x ∈ X}. We use a similar notation for projection:

X t,• = {x | x t,0 ∈ X t,0 } and X •,r = {x | x 0,
r ∈ X 0,r } denote the sets obtained by existential quantification of the reset (resp. translated) dimensions.

Observe that the over-approximation X t,• ⊓ X •,r of a set X by the cartesian product w.r.t. to translated and reset dimensions is equal to the Minkowski sum X t,0 + X 0,r .

The case of translations/resets with inputs can be handled similarly to translations: we combine Proposition 2 and Thm. 2 to reduce translations/resets with inputs to polyhedral translations with resets τ : G → x ′ = Cx+D defined by τ (X) = (X ⊓ G) t,0 +D.

Mind, however, that Rem. 1 does not apply any more and cannot be exploited in the presence of inputs, because the variables being reset may be assigned a different value in each iteration.

Proposition 4 (Polyhedral translation with resets). Let τ be a polyhedral translation with resets G → x ′ = Cx + D. Then, the set

τ ⊗ (X) = X ⊔ τ (X) ⊔ τ (τ (X) ⊓ G) t,0 ր D t,0 + D 0,r
is a convex over-approximation of τ * (X).

In the formula above and in the proof below, we unfold τ twice, that is, we accelerate only the central part of the sequence

x τ -→ x 0 . . . x n τ -→ x ′ with x ∈ X because we have ∀k ∈ [0, n] : x k ∈ G ⊓ D •,
r , whereas we only have x ∈ G at the start-point, and x ′ ∈ D •,r at the end-point.

Proof. The formula is trivially correct for 0 or 1 iterations of the self-loop τ . It remains to show that, for the case of k ≥ 2 iterations, our formula yields an over-approximation of k≥2 τ k (X).

x ′ ∈ k≥2 τ k (X) ⇐⇒ x ′ ∈ τ k≥0 τ k (τ (X)) ⇐⇒ ∃k ≥ 0, ∃x ∈ X, ∃x 0 . . . x k , ∃d 1 . . . d k ∈ D :                      x 0 ∈ τ (x) ∧ ∀k ′ ∈ [1, k] :    x i k ′ = x i 0 + k ′ j=1 d i j for i ∈ I t x i k ′ = d i k ′ for i ∈ I r ∧ x ′ ∈ τ (x k ) ∧ ∀k ′ ∈ [0, k] : G(x k ′ ) ⇐⇒ ∃k ≥ 0, ∃x ∈ X, ∃x 0 . . . x k , ∃d 1 . . . d k ∈ D :          ∀k ′ ∈ [1, k] : x k ′ = x t,0 0 + ( k ′ j=1 d t,0 j ) + d 0,r k ′ ∧ ∀k ′ ∈ [0, k] : G(x k ′ ) ∧ x 0 ∈ τ (x) ∧ x ′ ∈ τ (x k ) =⇒ ∃k ≥ 0, ∃x ∈ X, ∃x 0 . . . x k , ∃d t,0 1 . . . d t,0 k ∈ D t,0 , ∃d 0,r 1 . . . d 0,r k ∈ D 0,r :          ∀k ′ ∈ [1, k] : x k ′ = x t,0 0 + ( k ′ j=1 d t,0 j ) + d 0,r k ′ ∧ ∀k ′ ∈ [0, k] : G(x k ′ ) ∧ x 0 ∈ τ (x) ∧ x ′ ∈ τ (x k )
(D approximated by the sum (D t,0 + D 0,r ))

x 1 x 2 1 1 G X x 1 x 2 1 1 G X Fig. 7
. Translation/reset with inputs: Ex. 4. Left-hand side: τ (X) (dark shadowed) and ((τ (X) ⊓ G) t,0 ր D t,0 ) + D 0,r (whole shadowed area). Right-hand side: τ (((τ (X) ⊓ G) t,0 ր D t,0 ) + D 0,r ) (dark shadowed) and τ ⊗ (X) (whole shadowed area).

⇐⇒ ∃k ≥ 0, ∃x ∈ X, ∃x 0 , x k , ∃d t,0 ∈ D t,0 , ∃d 0,r k ∈ D 0,r :

         x k = x t,0 0 + kd t,0 + d 0,r k ∧ G(x 0 ) ∧ G(x k ) ∧ x 0 ∈ τ (x) ∧ x ′ ∈ τ (x k )
(because D t,0 , D 0,r and G are convex and

x 0,r 0 ∈ D 0,r ) =⇒ ∃α ≥ 0, ∃x ∈ X, ∃x 0 , x k , ∃d t,0 ∈ D t,0 , ∃d 0,r k ∈ D 0,r :    ∧ x k = x t,0 0 + αd t,0 + d 0,r k ∧ x 0 ∈ τ (x) ∧ G(x 0 ) ∧ x ′ ∈ τ (x k ) (dense over-approximation; G(x k ) already implied by x ′ ∈ τ (x k )) ⇐⇒ x ′ ∈ τ (τ (X) ⊓ G) t,0 ր D t,0 + D 0,r 2
Theorem 4 (Translation with resets, inputs and simple guards). The accelerated transition τ ⊗ for a translation/reset with inputs and a simple guard τ can be computed by applying Proposition 4 with D defined as in Proposition 2.

Example 4 (Translation with resets, inputs and simple guards). Consider the polyhedron

X = {(x 1 , x 2 ) | 0 ≤ x 1 ∧ 1 ≤ x 2 ∧ x 1 +x 2 ≤ 2}
and the transition τ :

x 1 + 2x 2 ≤ 3 0 ≤ ξ ≤ 1 → x ′ 1 = x 1 + ξ + 1 x ′ 2 = ξ Eliminating the inputs yields D = {(d 1 , d 2 ) | 1 ≤ d 1 ≤ 2 ∧ d 1 -d 2 = 1} and D t,0 = {(d 1 , d 2 ) | 1 ≤ d 1 ≤ 2 ∧ d 2 = 0}. We obtain τ ⊗ (X) = {(x 1 , x 2 ) | x 1 + x 2 ≥ 1 ∧ x 2 ≥ 0 ∧ x 1 -x 2 ≤ 4 ∧ x 1 +5x 2 ≤ 10 ∧ x 1 ≥ 0}, see Fig. 7.

Relaxing General Guards to Simple Guards

As discussed at the beginning of §4, allowing constraints that relate state variables with input variables in guards, i.e. G = Ax + Lξ ≤ b ∧ Jξ ≤ k with L = 0 (see Eqn. ( 5)), makes acceleration very difficult (Prop. 1). Our solution is to relax the guard G to a simple guard (or cartesian product) G = (∃ξ : G)

A ′ x≤b ′ ∧ (∃x : G) J ′ ξ≤k ′ .
We can now apply the accelerated transition from Theorems 3 and 4 with 8. Ex. 5: accelerated transition τ ⊗ (X) using the relaxed guard G (result shadowed).

G ′ = x 1 x 2 1 1 X G Fig.
x 1

x 2 1 1 Fig. 9. Ex. 5: comparison between convex hull of the exact result (dark gray), our method (gray), and widening with no delay and 3 descending iterations (light gray).

(A ′ x ≤ b ′ ) and D ′ = {d | ∃ξ : d = T ξ + u ∧ J ′ ξ ≤ k ′ }.
This trivially results in a sound over-approximation because a weaker guard is used for abstract acceleration.

Note however that in the corresponding acceleration formulas, we can still compute exactly the function τ using the original guard G. Indeed, the proofs of those theorems are not based on the assumption L = 0 when they introduce the function τ .

Example 5 (Relaxed guard). Consider the polyhedron

X = {(x 1 , x 2 ) | x 1 ≤ 1 ∧ x 2 ≤ 1 ∧ x 1 +x 2 ≥ 1}
and the transition τ :

2x 1 + x 2 + ξ ≤ 6 x 2 -ξ ≤ 2 0 ≤ ξ ≤ 1 → x ′ 1 = x 1 + ξ + 1 x ′ 2 = x 2 + 1 The relaxed guard is G = (2x 1 +x 2 ≤ 6 ∧ x 1 +x 2 ≤ 4 ∧ x 2 ≤ 3) ∧ (0 ≤ ξ ≤ 1). Eliminating the inputs yields D = {(d 1 , d 2 ) | 1 ≤ d 1 ≤ 2 ∧ d 2 = 1}. We obtain τ ⊗ (X) = {(x 1 , x 2 ) | x 1 +x 2 ≥ 1∧x 2 -x 1 ≤ 1∧-4 ≤ x 1 -2x 2 ≤ 1∧x 1 +2x 2 ≤ 10∧2x 1 +x 2 ≤ 10}, see Fig. 8. The convex hull of the exact result is {(x 1 , x 2 )|x 1 +x 2 ≥ 1∧-2 ≤ x 2 -x 1 ≤ 1∧x 1 -2x 2 ≤ 1∧x 2 ≤ 3∧2x 1 +x 2 ≤ 10}, see Fig. 9.

Backward Abstract Acceleration

Abstract acceleration has been applied to forward reachability analysis in order to compute the reachable states starting from a set of initial states. Backward analysis computes the states co-reachable from the error states. For example, combining forward and backward analysis allows to obtain an approximation of the sets of states belonging to a path from initial to error states (see for instance [START_REF] Jeannet | Dynamic partitioning in linear relation analysis. application to the verification of reactive systems[END_REF]). Moreover, a backward analysis allows us to synthesize constraints on parameter variables that ensure that a property is satisfied (see e.g. [START_REF] Alur | The algorithmic analysis of hybrid systems[END_REF]).

In this section, we present how to compute the accelerated backward transitions in the case of translations and translations/resets. Although the inverse of a translation is a translation, the difference is that the intersection with the guard occurs after the (inverted) translation. The case of backward translations with resets is more complicated than for the forward case, because resets are not invertible. Finally, the relaxation of general guards to simple guards applies in the same way to backward acceleration.

Translations

Proposition 5 (Polyhedral backward translation). Let τ be a polyhedral translation

G → x ′ = x + D. Then the set τ -⊗ (X ′ ) = X ′ ⊔ (τ -1 (X ′ ) ր (-D) ⊓ G
is a convex over-approximation of τ - * (X ′ ), where τ - * = (τ -1 ) * = (τ * ) -1 is the reflexive and transitive backward closure of τ .

The negation2 of a polyhedron has the following meaning: d ∈ (-D) ⇐⇒ (-d) ∈ D. It is hence the reflexion of D w.r.t. the origin.

Proof.

x 0 ∈ k≥1 τ -k (X ′ ) ⇐⇒ ∃x ′ ∈ X ′ : x ′ ∈ τ k≥0 τ k ({x 0 }) ⇐⇒ ∃k ≥ 0, ∃x ′ ∈ X ′ , ∃x k , ∃d 1 , . . . , d k ∈ D :          x k = x 0 + k j=1 d j ∀k ′ ∈ [0, k] : G(x 0 + k ′ j=1 d j ) x ′ ∈ τ ({x k }) (forward reachability) ⇐⇒ ∃k ≥ 0, ∃x ′ ∈ X ′ , ∃x k , ∃d 1 , . . . , d k ∈ D :          x k ∈ τ -1 ({x ′ }) x 0 = x k - k j=1 d j ∀k ′ ∈ [0, k] : G(x k - k j=k ′ +1 d j ) (rewritten as backward reachability) ⇐⇒ ∃k ≥ 0, ∃x ′ ∈ X ′ , ∃x k , ∃d ∈ D : x k ∈ τ -1 ({x ′ }) ∧ x 0 = x k -kd ∧ G(x 0 ) ∧ G(x k ) (because D and G are convex) =⇒ ∃α ≥ 0, ∃x ′ ∈ X ′ , ∃x k , ∃d ∈ D : x k ∈ τ -1 ({x ′ }) ∧ x 0 = x k -αd ∧ G(x 0 ) (dense approximation; G(x k ) implied by x k ∈ τ -1 ({x ′ })) ⇐⇒ x 0 ∈ (τ -1 (X ′ ) ր (-D) ⊓ G. 2 Example 6 (Polyhedral backward translation). Consider the polyhedron X ′ = {(x 1 , x 2 ) | 3 ≤ x 1 ≤ 6 ∧ 4 ≤ x 2 ≤ 5} and the transition τ : x 1 + 2x 2 ≤ 10 ∧ 0 ≤ x 1 ≤ 4 ∧ 0 ≤ x 2 ∧ 1 ≤ ξ ≤ 2 → x ′ 1 = x 1 + 1 x ′ 2 = x 2 + ξ The polyhedron D is {(d 1 , d 2 )|d 1 = 1 ∧ 1 ≤ d 2 ≤ 2}.
As result of the backward acceleration (Fig. 10) we obtain the polyhedron 10. Backward acceleration of a translation loop (Ex. 6) starting from X ′ with τ -1 (X ′ ) (dark gray) and τ -1 (X ′ ) ր (-D) (whole shadowed area) on the left-hand side and the final result (right-hand side).

{(x 1 , x 2 ) | 0 ≤ x 1 ≤ 6 ∧ 0 ≤ x 2 ≤ 5 ∧ -x 1 + x 2 ≤ 2 ∧ 4x 1 -3x 2 ≤ 12}. x 1 x 2 1 1 X ′ G x 1 x 2 1 1 X ′ G Fig.

Translations with Resets

Proposition 6 (Polyhedral backward translation with resets). Let τ be a polyhedral translation with resets G → x ′ = Cx + D. Then, the set

τ -⊗ (X ′ ) = X ′ ⊔ τ -1 (X ′ ) ⊔ τ -1 (τ -1 (X ′ ) t,• ր (-D t,0 ) ⊓ D •,r ⊓ G is a convex over-approximation of τ - * (X ′ ).
Proof. The formula is trivially correct for 0 or 1 backward iterations of the self-loop τ , thus, it remains to show that, for the case of k ≥ 2 iterations, our formula yields an over-approximation of k≥2 τ -k (X).

x ∈ k≥2 τ -k (X ′ ) ⇐⇒ ∃x ′ ∈ X ′ : x ′ ∈ τ k≥0 τ k (τ (x)) ⇐⇒ ∃k ≥ 0, ∃x ′ ∈ X ′ , ∃x 0 . . . x k , ∃d 1 . . . d k ∈ D :          x 0 ∈ τ (x) ∧ x ′ ∈ τ (x k ) ∧ ∀k ′ ∈ [1, k] : x k ′ = x t,0 0 + k ′ j=1 d t,0 j + d 0,r k ′ ∧ ∀k ′ ∈ [0, k] : G(x k ′ ) (forward reachability) ⇐⇒ ∃k ≥ 0, ∃x ′ ∈ X ′ , ∃x 0 . . . x k , ∃d 1 . . . d k ∈ D :          ∀k ′ ∈ [0, k-1] : x k ′ = x t,0 k - k j=k ′ +1 d t,0 j + d 0,r k ′ ∧ ∀k ′ ∈ [0, k] : G(x k ′ ) ∧ x k ∈ τ -1 ({x ′ }) ∧ x ∈ τ -1 ({x 0 }) (rewritten as backward reachability) =⇒ ∃k ≥ 0, ∃x ′ ∈ X ′ , ∃x 0 . . . x k , ∃d t,0 1 . . . d t,0 k ∈ D t,0 , ∃d 0,r 1 . . . d 0,r k ∈ D 0,r :          ∀k ′ ∈ [0, k-1] : x k ′ = x t,0 k - k j=k ′ +1 d t,0 j + d 0,r k ′ ∧ ∀k ′ ∈ [0, k] : G(x k ′ ) ∧ x k ∈ τ -1 ({x ′ }) ∧ x ∈ τ -1 ({x 0 })
(D approximated by the sum (D t,0 + D 0,r ))

⇐⇒ ∃k ≥ 0, ∃x ′ ∈ X ′ , ∃x 0 , x k , ∃d t,0 ∈ D t,0 , ∃d 0,r ∈ D 0,r :          x 0 = x t,0 k -kd t,0 + d 0,r ∧ G(x 0 ) ∧ G(x k ) ∧ x k ∈ τ -1 ({x ′ }) ∧ x ∈ τ -1 ({x 0 }) (because D t,0 , D 0,r and G are convex and x 0,r k ∈ D 0,r ) =⇒ ∃α ≥ 0, ∃x ′ ∈ X ′ , ∃x 0 , x k , ∃d t,0 ∈ D t,0 , ∃d 0,r ∈ D 0,r :    x 0 = x t,0 k -αd t,0 + d 0,r ∧ x k ∈ τ -1 ({x ′ }) ∧ x ∈ τ -1 ({x 0 }) ∧ G(x 0 ) (dense approximation; G(x k ) implied by x k ∈ τ -1 ({x ′ })) ⇐⇒ x ∈ τ -1 (τ -1 (X ′ )) t,• ր (-D t,0 ) ⊓ D •,r ⊓ G (because x ∈ τ -1 ({x ′ }) ⇒ x ′ ∈ D •,r ) 2
Example 7 (Polyhedral backward translation with resets). Consider the polyhedron

X ′ = {(x 1 , x 2 ) | 4 ≤ x 1 ≤ 5 ∧ 1 ≤ x 2 ≤ 4} and the transition τ : 3 ≤ x 1 + x 2 ≤ 5 ∧ 1 ≤ ξ ≤ 3 ∧ 0 ≤ x 2 → x ′ 1 = x 1 + 1 x ′ 2 = ξ The polyhedron D is {(d 1 , d 2 )|d 1 = 1 ∧ 1 ≤ d 2 ≤ 3}.
As result of the backward acceleration (Fig. 11), we obtain the polyhedron

{(x 1 , x 2 )|-1 ≤ x 1 ≤ 5 ∧ 0 ≤ x 2 ∧ x 1 +x 2 ≥ 3 ∧ x 1 -x 2 ≤ 4 ∧ x 1 +3x 2 ≤ 17}.

Evaluation and Comparison

This section discusses the advantages and shortcomings of abstract acceleration in comparison with more general abstract-interpretation-based methods like standard widening [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]) and the affine derivative closure method of [START_REF] Ancourt | A modular static analysis approach to affine loop invariants detection[END_REF].

Comparing Abstract Acceleration with Kleene Iteration

Abstract acceleration aims at computing a tight over-approximation of α( k≥0 τ k (X 0 )) where X 0 is a convex polyhedron and τ is an affine transformation with an affine guard. Since convex polyhedra are closed under affine transformations (α(τ (X 0 )) = τ (X 0 )), we 11. Backward acceleration of a loop with translations and resets (Ex. 7) starting from the initial set X ′ . Right-hand side: τ -1 (X ′ ) (dark gray) and (τ -1 (X ′ )|t ր (-D t ) ⊓ G (whole shadowed area). Left-hand side: final result (whole shadowed area).

x 1 x 2 1 1 X ′ G x 1 x 2 1 1 X ′ G Fig.
have α( k≥0 τ k (X 0 )) = k≥0 τ k (X 0 ). The latter formula is known as Merge-Over-All-Paths (MOP) solution of the reachability problem [START_REF] Kam | Monotone data flow analysis frameworks[END_REF]), which computes the limit of the sequence:

X 0 X 1 = X 0 ⊔ τ (X 0 ) X 2 = X 0 ⊔ τ (X 0 ) ⊔ τ 2 (X 0 ) . . .
In contrast, the standard approach in abstract interpretation computes the fixed point X ′ ∞ of X = X 0 ⊔ τ (X), known as the Minimal-Fixed-Point (MFP) solution. It proceeds as follows:

X ′ 0 = X 0 X ′ 1 = X ′ 0 ⊔ τ (X ′ 0 ) X ′ 2 = X ′ 0 ⊔ τ (X ′ 0 ⊔ τ (X ′ 0 )) . . .
The MOP solution is more precise than the MFP solution [START_REF] Kam | Monotone data flow analysis frameworks[END_REF]).

The reason is that, in general, τ does not distribute over ⊔ and we have τ

(X 1 ) ⊔ τ (X 2 ) ⊑ τ (X 1 ⊔ X 2 ). For instance, if X 0 = [0, 0] and τ : x ≤ 1 → x ′ = x + 2, we have X 2 = [0, 0] ⊔ [2, 2] ⊔ ⊥ = [0, 2] and X ′ 2 = [0, 0] ⊔ τ ([0, 2]) = [0, 3].
Since abstract acceleration should deliver a tight over-approximation of the MOP solution, we should generally have the relationship k≥0 τ k (X 0 ) ⊑ τ ⊗ (X 0 ) ⊑ X ′ ∞ , i.e. abstract acceleration should be more precise than the standard abstract interpretation approach (MFP) even without widening.

Fig. 12 shows an example illustrating this issue: in the standard abstract interpretation approach (MFP), each iteration translates the approximation added by the convex union with the result of the previous iteration in each step and converges slowly. Abstract acceleration translates only the intersection with the guard and takes the union as a last step. Observe, however, that in the case where X 0 is contained in the guard G, MOP and MFP solutions give identical results for this example [START_REF] Leroux | Acceleration in convex data-flow analysis[END_REF]).

Non-flat systems. Generally, the invariants computed by abstract acceleration of a single self-loop τ are not inductive, which implies that τ ⊗ is not idempotent, i.e. τ ⊗ (τ ⊗ (X 0 )) = τ ⊗ (X 0 ). While this is not a problem for flat systems, it has negative effects in the presence of nested loops.

For example, in the system (id • τ * ) * we can apply abstract acceleration to the innermost loop: (id • τ ⊗ ) * = (τ ⊗ ) * . If τ ⊗ is not idempotent (like in Fig. 12b), then the outer loop might not converge and thus widening is needed. Thus, the considerations w.r.t. MOP and MFP solutions for τ * above apply to (τ ⊗ ) * in the same manner.

x 1 x 2 1 1 X G 1 2 3 ∞ (a)
MFP: X dark gray, iteration 1 medium gray, iterations 2 and 3 dashed, final result whole shadowed area.

x 1 x 2 1 1 X G ≥ 1 ⊗ (b)
Abstract acceleration: X dark gray, iterations ≥ 1 medium gray, final result whole shadowed area.

: G → (x ′ 1 , x ′ 2 ) = (x1+1, x2 +1
) with G and X as given in the figures.

Since this problem arises in particular when the initial set is not contained in the guard G (like in Fig. 12b), [START_REF] Leroux | Acceleration in convex data-flow analysis[END_REF] propose to accelerate translations by the formula τ ⊗ (X) = τ (X ր D), i.e. without initially intersecting with G, which is idempotent and hence convergence without widening can be expected more often. However, this formula is clearly less precise and should not be used for accelerating non-nested loops.

Comparing Abstract Acceleration to Widening

In this section, we illustrate by some examples where abstract acceleration helps increasing the predictability and the robustness of the analysis.

Widening in self-loops. We consider Ex. 5, which has the structure depicted in Fig. 13 when analyzed with abstract acceleration or Kleene iteration with widening and descending iterations respectively.

The standard widening operator for convex polyhedra and refinements of it, like widening with thresholds [START_REF] Halbwachs | Verification of real-time systems using linear relation analysis[END_REF]), may sometimes lead to good results. Analyzing such a program using widening after a number N of initial steps resorts to computing the limit of the sequences

X 0 = X X ′ 0 = X N X n+1 = X 0 ⊔ τ (X n ) for n < N X ′ n+1 = X ′ n ∇(X ′ n ⊔ τ (X ′ n ))
in which X n , X ′ n are associated with location l 1 on Fig. 13 (right-hand side). The properties of the widening operator ∇ guarantee that the sequence (X ′ n ) n≥0 converges in a finite number of steps to X ′ ∞ [START_REF] Cousot | Abstract interpretation and application to logic programs[END_REF]), which is an over-approximation of the reachable valuations at location l 1 . This result may be improved by computing the first elements of the narrowing sequence 13. Analysis with acceleration (left-hand side) and with widening (right-hand side) for Ex. 5. We try first an analysis with undelayed widening, i.e. N = 0:

X ′′ 0 = X ′ ∞ , X ′′ n+1 = X 0 ⊔ τ (X ′′ n ), which does not necessarily converge. X ℓ ′ 1 ℓ 1 τ ⊗ X ℓ 1 τ Fig.
X ℓ 0 ℓ ′ 1 ℓ 1 x 3 ≤ 20 τ ⊗ ¬G → x ′ 3 = x 3 +1 X ℓ 0 ℓ 1 x 3 ≤ 20 τ ¬G → x ′ 3 = x 3 +1
X ′ 1 = {(x 1 , x 2 ) | x 1 +x 2 ≥ 1}
(result of converged widening sequence)

X ′′ 1 = {(x 1 , x 2 ) | x 1 +x 2 ≥ 1 ∧ 2x 1 +x 2 ≤ 10 ∧ x 2 ≤ 4 ∧ 0 ≤ x 1 ≤ 6 ∧ 3x1+5x 2 ≥ 3} . . . X ′′ 3 = {(x 1 , x 2 ) | x 1 +x 2 ≥ 1 ∧ 2x 1 +x 2 ≤ 10 ∧ 3x 2 -2x 1 ≤ 6 ∧ 3x 2 -4x 1 ≤ 3∧ 5x 1 -22x 2 ≤ 8 ∧ 29x 1 -157x 2 ≤ 29} ⊐ τ ⊗ (X) . . . (descending sequence)
Here, the descending iterations do not converge and improve the result slowly. See Fig. 9 for X ′′ 3 . By increasing the delay to N = 1, we can improve the result, and we get the same result as with abstract acceleration: X ′′ 1 = τ ⊗ (X). However, this is not guaranteed in general, because widening is not monotonic. Moreover, abstract acceleration is more efficient computationally: delaying widening and a long descending sequence increase the number of iterations. In flat programs, like in Ex. 5, abstract acceleration does not even require convergence tests.

Widening in nested loops. In the previous example, delayed widening and descending iterations allowed to get the same result as with abstract acceleration. However, this is less likely if the loop is embedded in an outer loop as in Fig. 14: descending iterations cannot be applied during the ascending iterations, but only after convergence of the widening sequence of the whole program, otherwise convergence would not be guaranteed.

Example 8 (Widening in nested loops).

We consider the program depicted in Fig. 14 in which the inner loop τ is adapted from Ex. 4:

τ : 2x 1 + 2x 2 ≤x 3 0 ≤ ξ≤1 → x ′ 1 = x 1 +ξ+1 x ′ 2 = ξ x ′ 3 = x 3 X =    (x 1 , x 2 , x 3 ) 0 ≤ x 1 ∧ 1 ≤ x 2 x 1 +x 2 ≤ 2 ∧ x 3 = 3   
The analysis without abstract acceleration yields for any widening delay N ≥ 1 (widening point ℓ 1 ) and any number of descending iterations N ′′ ≥ 1 the following very weak invariant:

X ′ 1 = {(x 1 , x 2 , x 3 ) | 0 ≤ x 1 ∧ 3 ≤ x 3 } X ′′ 1 = {(x 1 , x 2 , x 3 ) | 0 ≤ x 1 ∧ 1 ≤ x 1 + x 2 ∧ 3 ≤ x 3 } Abstract acceleration
with widening delay N ≥ 1 (widening point ℓ 1 ) and one descending iteration gives much better results: we give here a simplified (over-approximated) invariant, because the actual result consists of more constraints:

X ′′ 1 = {(x 1 , x 2 , x 3 ) | 0 ≤ x 1 ≤ 12 ∧ 0 ≤ x 2 ≤ 3 ∧ 3 ≤ x 3 ≤ 20 ∧ 1 ≤ x 1 + x 2 }
One can also consider widening with thresholds. A natural threshold set for our example is the postcondition of the guard of τ by the body of τ :

τ (⊤) = {(x 1 , x 2 ) | 0 ≤ x 2 ≤ 1}.
Yet, this does improve the result.

Extending the threshold set with the postcondition of the guard of the outer loop x 3 ≤ 21 improves the result (all variables are bounded), but it is still less precise than the result obtained by combining abstract acceleration and widening (in particular the descending iteration does not converge).

Comparing Abstract Acceleration to the Affine Derivative Closure Algorithm

The affine derivative closure algorithm of [START_REF] Ancourt | A modular static analysis approach to affine loop invariants detection[END_REF] is another abstract interpretation-based analysis method. The idea is to compute an abstract transformer, i.e. a relation between variables x and x ′ , independently of the initial state of the system. The abstract transformer abstracts the effect of the loop by a polyhedral translation

true → x ′ = x + D R with D R = {d | ∃x, ξ, x ′ : R(x, ξ, x ′ ) ∧ x ′ = x + d}
where R is the concrete transition relation. The polyhedron D R is called the "derivative" of the relation R. The effect of several self-loops with relations R 1 , . . . , R k is abstracted by considering the convex union i D Ri .

Then, the reflexive and transitive closure

R * = {(x, x ′ ) | ∃k ≥ 0 : x ′ = x+kd ∧ D R (d)}
is applied to a polyhedron X of initial states:

R * (X) = {x ′ | ∃x : R * (x, x ′ ) ∧ X(x)}
The final result is obtained by computing one "descending" iteration, in the same way as it is done in standard abstract interpretation after widening. The affine derivative closure algorithm is implemented in the code optimization tool Pips3 .

In single self-loops with translations or translations/resets, the method works similarly to abstract acceleration, as illustrated by the following example involving resets and inputs:

Example 9 (Single loop). τ :

x 1 ≤ 4 x 2 ≤ 4 0 ≤ ξ ≤ 1 → x ′ 1 = x 1 +ξ+1 x ′ 2 = ξ+2 X =    (x 1 , x 2 ) x 1 ≤ 1 ∧ x 2 ≤ 1 x 1 +x 2 ≥ 1    The transition relation R = {(x 1 , x 2 , ξ, x ′ 1 , x ′ 2 ) | x ′ 1 = x 1 +ξ+1 ∧ x ′ 2 = ξ+2 ∧ x 1 ≤ 4 ∧ x 2 ≤ 4 ∧ 0 ≤ ξ ≤ 1} expressed in terms of derivatives is X G x 1
x 2 1 1 (a) Derivative closure method: R * applied to X (whole shadowed area), final result (dark gray).

x 1 ≤ 9 → x ′ 1 = x 1 + 1 ∧ x ′ 2 = 0 x 2 ≤ 9 → x ′ 1 = x 1 ∧ x ′ 2 = x 2 + 1 x ′ 1 = 0 ∧ x ′ 2 = 0 Fig. 16. Ex. 10. D R = {(d 1 , d 2 ) | ∃x 1 , x 2 , ξ, x ′ 1 , x ′ 2 : R(x 1 , x 2 , ξ, x ′ 1 , x ′ 2 ) ∧ x ′ 1 = x 1 +d 1 ∧ x ′ 2 = x 2 +d 2 } = {(d 1 , d 2 ) | 1 ≤ d 1 ≤ 2 ∧ d 1 -d 2 ≤ 3}
The closure of the loop starting from X gives

R * (X) = {(x ′ 1 , x ′ 2 ) | ∃k ≥ 0, x 1 , x 2 : x ′ 1 ≥ x 1 + k ∧ x ′ 1 ≤ x 1 + 2k∧ x ′ 1 -x ′ 2 ≤ x 1 -x 2 + 3k ∧ X(x 1 , x 2 )} = = {(x ′ 1 , x ′ 2 ) | 0 ≤ x ′ 1 ∧ 2x ′ 1 + x ′ 2 ≥ 1} Finally, a descending iteration is computed: X ⊔ τ (R * (X)) = {(x ′ 1 , x ′ 2 ) | x ′ 1 +x ′ 2 ≥ 1 ∧ x ′ 1 -2x ′ 2 ≤ 1 ∧ x ′ 1 -x ′ 2 ≤ 3∧ x ′ 2 ≤ 3 ∧ x ′ 1 -x ′ 2 ≥ -1}
This result equals the one obtained by abstract acceleration (see Fig. 15).

Resets cannot be expressed as polyhedral translations: for instance, if R(x, x ′ ) = (x ′ = 0), then D R = {d |∃x, x ′ : x ′ = 0 ∧ x ′ = x + d } = ⊤. However, this information is recovered during the descending iteration. Hence, similarly to widening, these descending iterations may fail in the presence of multiple loops:

Example 10 (Multiple loops). For the CFG in Fig. 16, the derivatives for the upper and the lower loop are D R1 = (d 1 = 1) and D R2 = (d 1 = 0 ∧ d 2 = 1) respectively. Their convex union is D R1,2 = (0 ≤ d 1 ≤ 1). The transitive closure applied to X = (x 1 = x 2 = 0) gives R * 1,2 (X) = (x 1 ≥ 0), and the final result after the descending iteration is X ′ = (x 1 ≥ 0 ∧ x 2 ≤ 10). Here, the descending iteration fails to recover the upper bound of x 1 .

In contrast, abstract acceleration converges after two ascending iterations with the invariant X 2 = (0 ≤ x 1 ≤ 10 ∧ 0 ≤ x 2 ≤ 10).

Hence, even though the derivative closure method elegantly deals with multiple loops by taking the convex union of the derivatives, it is also less precise than abstract acceleration for such programs. However, the main advantage of the derivative closure method is that it is more general than abstract acceleration, because it automatically approximates any kind of transformations. Moreover, since it computes abstract transformers, it is modular and can be used in the context of interprocedural analyses.

Applying Abstract Acceleration

Control flow graphs. Program analysis using abstract interpretation in general and abstract acceleration in particular, is done on a control flow graph (CFG) of the program, which manipulates only numerical variables. This graph can be easily obtained from imperative programs by associating control points to programming constructs.

As mentioned in the introduction our goal is to analyze logico-numerical data-flow programs such as Lustre [START_REF] Caspi | LUSTRE: a declarative language for real-time programming[END_REF]) programs: In order to reduce such a program to a purely numerical CFG, all possible valuations of Boolean state variables need to be enumerated and encoded in locations of the CFG. This partitioning and partial evaluation process may lead to a combinatorial explosion of control locations. [START_REF] Jeannet | Dynamic partitioning in linear relation analysis. application to the verification of reactive systems[END_REF] presented abstract interpretation methods for analyzing such programs using controlled partitioning, i.e. some Boolean states are encoded explicitly as locations in the CFG, whereas the other Boolean variables are handled symbolically. Pursuing this approach, we have developed methods for applying abstract acceleration to such a logico-numerical CFG (see [START_REF] Schrammel | Logico-numerical abstract acceleration and application to the verification of data-flow programs[END_REF] for details).

Pre-processing. Some transformations are necessary in order to prepare a self-loop in a CFG for abstract acceleration. These comprise especially the elimination of Boolean input variables resulting in a non-deterministic CFG and splitting non-convex guards into convex ones. Methods for dealing with multiple self-loops in a single location are described by [START_REF] Gonnord | Accélération abstraite pour l'amélioration de la précision en analyse des relations linéaires[END_REF].

Experimental results. Table 1 shows some experimental results comparing our tool nbAC-Cel, which implements the methods presented in this article, with the tool Nbac (Jeannet ( 2003)). The benchmarks have quite different sizes from ten up to a few hundred lines of Lustre code. The safety properties we want to prove about the small examples require a very good precision on the numerical variables. We observe that we are able to prove some benchmarks that are not provable using Nbac. This is due to the precision gained by abstract acceleration. But also on the other examples nbACCel is mostly faster than Nbac; except for some of the larger benchmarks where the more sophisticated dynamic partitioning techniques employed in Nbac start to pay off. Further results including a comparison with Aspic (Gonnord ( 2009)) can be found in [START_REF] Schrammel | Logico-numerical abstract acceleration and application to the verification of data-flow programs[END_REF].

Related Work

As already outlined in the introduction, there are essentially two approaches to the reachability problem: Those that aim at computing exact results using additive integer (Presburger) or real arithmetic without guarantee of termination (in the cases mentioned in the introduction); and those that are based on abstract interpretation which terminate but generally ignore divisibility properties and deliver only conservative approximations.

Presburger-based approaches. [START_REF] Bultan | Symbolic model checking of infinite state systems using presburger arithmetic[END_REF] use Presburger formulas to represent the state space of integer variables in symbolic model checking of concurrent programs, but they use an abstract-interpretation-like widening operator in order to accelerate loops and actually compute an over-approximation. [START_REF] Boigelot | Symbolic verification with periodic sets[END_REF]; [START_REF] Boigelot | Symbolic methods for exploring infinite state spaces[END_REF] introduce a representation called periodic vector sets of the form ∃k ∈ Z m : x = Ck+d∧Pk ≤ q for capturing the transitive closure of affine transformations, and apply it to communication protocols involving integer variables. Their method tries to accelerate selected cycles in so-called meta-transitions, but without guarantee for termination. [START_REF] Fribourg | Proving safety properties of infinite state systems by compilation into presburger arithmetic[END_REF] compute the reachable state space of Petri nets with unbounded markings using a decision procedure over Presburger arithmetic. [START_REF] Finkel | How to compose Presburger-accelerations: Applications to broadcast protocols[END_REF]; [START_REF] Bardin | Faster acceleration of counter automata in practice[END_REF] apply Presburger-based acceleration to communication protocols. They extend the results of [START_REF] Boigelot | Symbolic methods for exploring infinite state spaces[END_REF] to periodic affine transformations as defined in Sec. 3. Their methods have also been applied to FIFO queues using subclasses of regular expressions [START_REF] Boigelot | Symbolic verification of communication protocols with infinite state spaces using QDDs[END_REF]; [START_REF] Abdulla | Using forward reachability analysis for verification of lossy channel systems[END_REF]). [START_REF] Bardin | FAST: Fast acceleration of symbolic transition systems[END_REF] describes the tool Fast for analyzing flattable programs, i.e. without nested loops. [START_REF] Bardin | Flat acceleration in symbolic model checking[END_REF] present an overall framework for various classes of systems that can be treated by exact acceleration. [START_REF] Bozga | Fast acceleration of ultimately periodic relations[END_REF] unifies the computation of transitive closures of such as difference relations, octagonal relations and finite monoid affine transformations by defining the notion of ultimately periodic relations. Their method is also based on Presburger arithmetic. Like us, this work investigates the case of relations instead of deterministic functions. Difference relations (and their octogonal generalization) have an incomparable expressive power compared to translations/resets with inputs and simple guards seen as relations:

• Difference relations can express for instance variables permutation, unlike translations/resets; • but they cannot express translations/resets involving guards with general linear constraints, such as (x 1 +2x 2 ≤ 10) →

x

′ 1 = x 1 +1 x ′ 2 = x 2 +2 or (ξ 1 +2ξ 2 = 3) → x ′ 1 = x 1 +ξ 1 x ′ 2 =
x 2 +ξ 2 Last, finite monoid affine transformations, which are deterministic, correspond to the periodic case that we did not consider in Sec. 3.

Acceleration has also been used in the analysis of timed and hybrid automata. For example, the concepts of [START_REF] Boigelot | Symbolic methods for exploring infinite state spaces[END_REF] were developed further by [START_REF] Boigelot | Hybrid acceleration using real vector automata[END_REF] to the acceleration of general affine relations R(x, x ′ ). The basic technique applies to relations of the form G(x) ∧ G ′ (x ′ ) ∧ P (x ′x) where G, G ′ and P are conjunctions of linear inequalities. Observe that, if G ′ is true, such relations can be expressed in our setting as pure translations with inputs and simple guards, defined by G(x) ∧ P (ξ) → x ′ = x + ξ. [START_REF] Boigelot | The power of hybrid acceleration[END_REF] develop transformation methods (based mainly on variable changes) to reduce subclasses of affine relations to this basic case. It would be interesting to apply and adapt their methods to abstract acceleration. These two papers apply this approach to the verification of rectangular hybrid systems (as defined by [START_REF] Alur | The algorithmic analysis of hybrid systems[END_REF]) that include timed automata.

Recent research exhibited results on the transitive closure of affine integer tuple relations [START_REF] Beletska | Computing the transitive closure of a union of affine integer tuple relations[END_REF]). Their goal is to compute multiple clause relations, i.e. several self-loops, with commutative transition relations:

τ 1 • τ 2 = τ 2 • τ 1 , e.g. τ 1 : x ′ 1 = x 1 + 1; x ′ 2 = 2x 2 and τ 2 : x ′ 1 = x 1 + 3; x ′ 2 = 5x 2 .
They use Presburger-based methods and apply their results in the context of program parallelization.

Abstract interpretation-based approaches to acceleration are comparatively recent. Also our method falls into this category and extends the work of [START_REF] Gonnord | Combining widening and acceleration in linear relation analysis[END_REF] and [START_REF] Gonnord | Accélération abstraite pour l'amélioration de la précision en analyse des relations linéaires[END_REF]. Apart from self-loops of translations and translations with resets for which we developed our extensions, they also deal with periodic affine transformations and some special cases of multiple self-loops. Furthermore, they describe methods for unfolding multiple self-loops in order to compute the fixed point more efficiently.

The affine derivative closure algorithm [START_REF] Ancourt | A modular static analysis approach to affine loop invariants detection[END_REF]) that we explained in more detail in Section 6.3 is also based on abstract interpretation methods, but unlike abstract acceleration it neither inspects the types of transitions in order to apply an optimized acceleration formula nor specializes w.r.t. a given initial state.

Conclusion and Discussion

We have presented an extension of abstract acceleration to numerical inputs for forward and backward analysis. Table 2 shows a summary of the formulas. This extension is less straightforward than supposed -most notably due to the observation that inputs can be used to turn translations into arbitrary affine transformations; also, resetting variables to input values may cause some subtle behavior. Regarding approximations, Table 2 shows the cases where our method is precise in the sense that we perform only dense and convex approximations, and the more complex cases for which additional approximations are necessary to abstract away the number of iterations.

Abstract acceleration elegantly integrates into an abstract interpretation-based verification tool, where it is usually used in combination with widening: as pointed out in Sec. 6.2, due to its monotonicity property it is possible to accelerate the innermost loops precisely while using widening for the outer loops in nested loop situations. Thus, much better invariants can be computed for programs where a lot of information is lost when using widening only.

In comparison to other abstract interpretation-based transitive closure methods, for instance the affine derivative closure algorithm of [START_REF] Ancourt | A modular static analysis approach to affine loop invariants detection[END_REF], abstract acceleration deals only with some frequently occurring types of self-loop transitions, for which it yields more precise results (especially for transitions with resets), but it needs to resort to widening in the general case.

We have reported some first experimental results that give evidence about the potential of abstract acceleration w.r.t. improving reachability analysis in terms of precision and performance.

Regarding future work, we could extend slightly the transformations we consider. Firstly, we conjecture that it is possible to generalize our results from the case where C Translations/resets D is approximated by the Cartesian product D t × D r .

Table 2. Overview of abstract acceleration formulas is a diagonal matrix with either 0 or 1 to the case where C is periodic with prefix p and period l as defined in Sec. 3. This could be done in the same way as [START_REF] Finkel | How to compose Presburger-accelerations: Applications to broadcast protocols[END_REF] by rewriting k≥0 τ k as

τ 0 ∪ . . . ∪ τ p-1 ∪ k≥0 (τ l ) k • τ p ∪ . . . ∪ k≥0 (τ l ) k • τ p+l-1
and accelerating τ l on the image of τ p+i with 0 ≤ i ≤ l-1.

Secondly, it should be also possible to generalize and unify the two classes of relations induced resp. by forward and backward translations/resets with inputs and simple guards to a more general symmetrical class, and to consider the acceleration of such relations. A candidate could be

R(x, x ′ ) ⇔    Ax ≤ b ∧ Jξ ≤ k A ′ x ′ ≤ b ′ ∧        x ′ t -x t = T t ξ + u t (translated dimensions) x ′ f = T f ξ + u f (forward reset dimensions) x b = T b ξ + u b (backward reset dimensions)
in which the set of dimensions is partioned into three classes.

Regarding integer (e.g., divisibility) properties, our techniques based on convex polyhedra cannot express them and Remark 2 discusses the effect of the induced dense approximation. To improve on this we could combine our techniques with the linear congruence abstract domain introduced in [START_REF] Granger | Static analysis of linear congruence equalities among variables of a program[END_REF]. This domain satisfies the finite ascending condition, hence it does not require widening nor acceleration. By this means we are able to tighten the results. For instance, if the abstract acceleration results in a convex polyhedron 2 ≤ x 1 ≤ 8∧2x 1 +x 2 ≤ 9, and we know from the linear congruences domain that x 1 = 1 mod 4 ∧ x 2 = 0 mod 2 (typically because (x 1 , x 2 ) are iteratively translated by (4, 2) from a known value), then the convex polyhedron can be tightened to x 1 = 5∧2x 1 +x 2 ≤ 8. Compared to Presburger arithmetic, we still limit ourselves to convex sets with such a technique. The general goal would be to add congruence constraints in the guard of the transformation τ and to exploit them as sketched above.

The question under which condition translations/resets with inputs viewed as relations are ultimately periodic relations in the sense of [START_REF] Bozga | Fast acceleration of ultimately periodic relations[END_REF] could be also investigated. We conjecture that this is only true in the cases where our methods perform only dense and convex approximations (see Table 2).

Fig. 1 .

 1 Fig. 1. Example program (a), transformed program (b) where τ * denotes the transitive closure of the transition τ , and set of initial states (c).

  Fig. 5 left-hand side. After translation of X by D (Fig. 5 right-hand side) we obtain the polyhedron {

Fig. 5 .

 5 Fig. 5. Translation with inputs (Ex. 3): The left-hand side shows the computation of D: Jξ ≤ k ∧ d = Tξ + u (bold line) is projected on variables d to obtain D. The shadowed area in the right-hand side figure is τ ⊗ (X).

  x

Fig. 12 .

 12 Fig. 12. Comparison between standard abstract interpretation (MFP) (a) and abstract acceleration (b): τ: G → (x ′ 1 , x ′ 2 ) = (x1+1, x2+1) with G and X as given in the figures.

Fig. 14 .

 14 Fig. 14. Analysis with acceleration (left-hand side) and with widening (right-hand side) for Ex. 8. G = (2x1 +2x2 ≤ x3).

  Abstract acceleration: iterations ≥ 1 (dark gray), final result (whole shadowed area).

Fig. 15 .

 15 Fig. 15. Comparison between the affine derivative closure algorithm (a) and abstract acceleration (b), Ex. 9.

  X) = X ⊔ τ (X ⊓ G) ր D Translations/resets τ ⊗ (X) = X ⊔ τ (X) ⊔ τ (τ (X) ⊓ G) t,0 ր D t,0 + D 0,r Backward acceleration: Translations τ -⊗ (X ′ ) = X ′ ⊔ (τ -1 (X ′ ) ր (-D) ⊓ G Translations/resets τ -⊗ (X ′ ) = X ′ ⊔ τ -1 (X ′ )⊔ ⊔τ -1 (τ -1 (X ′ ) t,• ր (-D t,0 ) ⊓ D •,r ⊓ G with τ : ( G0(x, ξ) Ax + Lξ ≤ b ∧ G1(ξ) Jξ ≤ k) -→ x ′ = Cx + Tξ + u C diagonal with 0 or 1 only G(x) = ∃ξ : G0(x, ξ) D = {d | ∃ξ : d = T ξ + u ∧ G1(ξ) ∧ ∃x : G0(x, ξ)} Approximations:In all cases dense and convex approximation L = 0 G and D are decoupled.

Table 1 .

 1 Experimental comparison between nbACCel and Nbac (size. . . number of locations of the enumerated CFG; times in seconds; ?. . . property not proved)

		size nbACCel Nbac		size nbACCel Nbac
	Gate 1	7	0.73	?	LCM Quest 0c-2	25	0.24	14.8
	Escalator 1	12	0.49	?	LCM Quest 1-1	114	0.92	2.45
	Traffic 1	18	0.19	3.49	LCM Quest 2-1	247	7.84	12.8
	Traffic 2	18	0.35	?	LCM Quest 3-1	483	8.49	3.76
	LCM Quest 0a-1	7	0.04	0.05	LCM Quest 3b-1 1724	43.8	19.1
	LCM Quest 0a-2	6	0.05	0.19	LCM Quest 3c-1 1319	34.2	?
	LCM Quest 0b-1	19	0.08	?	LCM Quest 3d-1	281	5.43	?
	LCM Quest 0b-2	17	0.20	?	LCM Quest 3e-1	638	20.6	?
	LCM Quest 0c-1	28	0.16	0.86	LCM Quest 4-1	4482	186	50.1

Note that the 0 in the matrix of the guard does not imply a loss of generality.

Not to be confounded with the complement.

http://pips4u.org

⋆ This work was supported by the INRIA large-scale initiative Synchronics and the ANR project Asopt.