Peter Schrammel
email: peter.schrammel@inria.fr

Bertrand Jeannet
email: bertrand.jeannet@inria.fr

From Hybrid Data-Flow Languages to Hybrid Automata: A Complete Translation *

Keywords: D.2.1 [Software Engineering]: Requirements/Specification-Languages, D.2.4 [Software Engineering]: Software / Program Verification-Formal methods, I.6.2 [Computing Methodologies]: Simulation and Modelling-Simulation Languages Data-Flow Languages, Hybrid Systems, Hybrid Automata, Verification

Hybrid systems are used to model embedded computing systems interacting with their physical environment. There is a conceptual mismatch between high-level hybrid system languages like Simulink, which are used for simulation, and hybrid automata, the most suitable representation for safety verification. Indeed, in simulation languages the interaction between discrete and continuous execution steps is specified using the concept of zero-crossings, whereas hybrid automata exploit the notion of staying conditions. We describe a translation from a hybrid data-flow language to logiconumerical hybrid automata that points out this issue carefully. We expose various zero-crossing semantics, propose a sound translation, and discuss to which extent the original semantics is preserved.

INTRODUCTION

The motivation of this paper is the verification of safety properties of hybrid systems, like, for example, safety-critical controllers interacting with their physical environment as Specifying hybrid systems. Languages like Simulink1 , Modelica2 , and Zelus [START_REF] Benveniste | Divide and recycle: types and compilation for a hybrid synchronous language[END_REF] have been developed to support the modelling, implementation and simulation of hybrid systems. They offer features like modularity, hierarchy and a data-flow or equational syntax.

Simulink for example uses a data-flow-based description of the behavior of continuous-and discrete-time variables; Stateflow extends it with the ability of automata-based specifications of the discrete-time behavior. Zelus extends the synchronous, data-flow programming language Lucid-Synchrone [START_REF] Pouzet | Lucid Synchrone, version 3. Tutorial and reference manual[END_REF] with differential equations. In these languages, discrete execution steps that interrupt the continuous-time evolution are triggered by the activation of zerocrossings. 3 Roughly speaking, a zero-crossing is an event occurring during the integration of an ordinary differential equation (ODE) ẋ(t) = f (x(t), u(t)), when some expression z(x(t)) changes sign from negative to positive. A zerocrossing may also be triggered by a discrete execution step as in Simulink. All these data-flow languages are primarily designed for simulation, hence their semantics is mostly deterministic.

On the other hand, the concept of hybrid automata [START_REF] Alur | The algorithmic analysis of hybrid systems[END_REF][START_REF] Henzinger | The theory of hybrid automata[END_REF][START_REF] Henzinger | HyTech: A model checker for hybrid systems[END_REF] was developed for the verification of hybrid systems. They are lower-level representations of hybrid systems with a non-deterministic semantics by default, and in which continuous-time evolution is governed by staying conditions, usually referred to as location invariants.

Hence, there is a conceptual mismatch between high-level hybrid system languages and hybrid automata. The main differences between simulation and verification formalisms can be summarized as follows: -equation-based versus automata-based -continuous modes implicitly encoded in Boolean variables versus their explicit encoding with locations -discrete transitions triggered by zero-crossings versus combinations of staying conditions and guards -deterministic, open systems with inputs versus non-deterministic, closed systems. Our primary goal is to formalize the translation from a hybrid data-flow formalism to hybrid automata, and in particular to focus on the translation of zero-crossings. How-ever, a secondary aspect we have in mind is that we want to address hybrid systems specified as the composition of a discrete controller and its physical environment. This means that the discrete part of the system's state space might be complex, and defined by Boolean variables and numerical variables (counters, thresholds, etc. manipulated by the controller). The consequence is that we want to translate the data-flow input language to logico-numerical hybrid automata, that can manipulate symbolically discrete variables, in addition to continuous variables governed by differential equations. Such automata allow a compact representation by not requiring the enumeration of the discrete state space.

Verifying hybrid systems. There is a vast literature on hybrid system verification based on hybrid automata. Here, we cite only some selected methods, that can be classified as follows:

Bounded-time analysis methods analyze systems up to some time horizon. Systems with linear or non-linear dynamics require a time discretization: either a so-called flowpipe (a set of convex sets over-approximating the possible trajectories) is constructed by set integration [START_REF] Chutinan | Verification of polyhedral-invariant hybrid automata using polygonal flow pipe approximations[END_REF][START_REF] Frehse | PHAVer: Algorithmic verification of hybrid systems past HyTech[END_REF][START_REF] Frehse | SpaceEx: Scalable verification of hybrid systems[END_REF], or the discretized system is saturated by constraint propagation techniques [START_REF] Fränzle | HySAT: An efficient proof engine for bounded model checking of hybrid systems[END_REF][START_REF] Ratschan | Safety verification of hybrid systems by constraint propagation-based abstraction refinement[END_REF].

Unbounded-time methods are more challenging, because unbounded time raises a termination issue. [START_REF] Halbwachs | Verification of real-time systems using linear relation analysis[END_REF] analyzes systems with piecewise constant dynamics with convex polyhedra and solves the termination issue by the use of widening [START_REF] Cousot | Comparing the Galois connection and widening/narrowing approaches to abstract interpretation[END_REF]. [START_REF] Briand | Combining control and data abstraction in the verification of hybrid systems[END_REF] extends this approach, by considering the verification of hybrid systems with a large discrete state space and by combining symbolically properties on Boolean and numerical variables within the abstract interpretation framework. Recently a method exploiting max-strategy iteration on template polyhedra was proposed in [START_REF] Dang | Discretizing affine hybrid automata with uncertainty[END_REF].

Contributions. Our contributions can be summarized as follows:

1. We present the general principles behind the translation of a simple, yet complete hybrid data-flow language that serves as a low-level formalism for languages such as Simulink or Zelus, to logico-numerical hybrid automata, i.e. an extension of classical hybrid automata by Boolean variables. This extension prepares us w.r.t. the verification of programs with a large Boolean state space. 2. We discuss the various zero-crossing semantics that appear in the source simulation language. We propose sound translations to hybrid automata, and we investigate the extent to which these translations preserve the original semantics.

Related work.

Recent articles describe translations of hybrid system languages, like Simulink/Stateflow, to hybrid automata, but they only treat a subset of the ways in which discrete transitions may be activated. A translation of a subset of the Simulink/Stateflow language to hybrid automata is proposed in [START_REF] Agrawal | Semantic translation of Simulink/Stateflow models to hybrid automata using graph transformations[END_REF] for the purpose of verification. They handle Stateflow diagrams of which the translation is rather straightforward, but they do not handle proper zero-crossings. Another translation of a subset of the Simulink/Stateflow language to hybrid automata with the goal of improving simulation coverage is presented in [START_REF] Alur | Symbolic analysis for improving simulation coverage of Simulink/Stateflow models[END_REF], but they only consider deterministic models, and similarly they do not handle zero-crossings. The tool HyLink [START_REF] Manamcheri | A step towards verification and synthesis from Simulink/Stateflow models[END_REF], which performs a translation of Simulink/Stateflow models to hybrid automata, targets the applications of verification and controller synthesis. It is restricted to more or less the same subset as [START_REF] Agrawal | Semantic translation of Simulink/Stateflow models to hybrid automata using graph transformations[END_REF]. They introduce blocks for specifying non-deterministic inputs as required by verification methods. A formal definition of the translation is ongoing work. The translation of discrete-time Simulink models with periodic triggers to Lustre is presented in [START_REF] Tripakis | Translating discrete-time Simulink to Lustre[END_REF]. The inverse of what we are doing, namely the embedding of hybrid automata in a hybrid system language (here Scicos), is the goal of [START_REF] Najafi | Implementation of hybrid automata in Scicos[END_REF].

Organisation of the article. § §2 and 3 introduce the hybrid data-flow formalism and logico-numerical hybrid automata respectively. § §4 to 7 describe our contributions.

After discussing the results in §8 we conclude in §9.

HYBRID DATA-FLOW MODEL

Simulink and Zelus are full programming languages with constructs for modularity. In order to abstract from such constructs, we present here a lower-level data-flow formalism that will serve as the generic input language for the translation.

As this formalism is dedicated not only to simulation, but also serves as a specification language, we use the notion of inputs constrained by an assertion as in Lustre [START_REF] Caspi | LUSTRE: a declarative language for real-time programming[END_REF]. This allows us to give a semantics to the components of a more general system. Simulation can still be performed by connecting a component with inputs to an input generator, see for instance [START_REF] Raymond | Lutin: A language for specifying and executing reactive scenarios[END_REF] for the simulation of discrete synchronous systems.

Notations. We will use the following notations: s = (b, x) : state variable vector, with b discrete (Boolean and numerical) and x continuous numerical subvectors, e.g.

((b1, b2, n1), x1, x2, x3) ∈ (B 2 × Z)×R
   I(s) A(s, i) ∧ ẋ = f c (s, i) s ′ = f d (s, i)
where the predicate I(s) defines the initial states, the predicate A(s, i) is the global assertion constraining the inputs, the continous flow equations ẋ = f c (s, i) and the discrete transition functions s ′ = f d (s, i) are of the form:

ẋ = • • • e ℓ (s, i) if φ ℓ (b) • • • s ′ = • • • Φj(s, i) if ϕ Z j (s, i) • • •
We assume that the conditions φ ℓ define a partition of the discrete state space, and that ∀s∃i : A(s, i) (i.e. the assertion does not constrain the state-space).

Furthermore the zero-crossing formulas ϕ Z j must be exclusive in order to guarantee determinism, i.e. only a single ϕ Z j may be activated at the same instant. Real languages let node main xi eps = (n,x) where assert 0<=xi && xi<=30 && -0.1<=eps && eps<=0.1 and der x = if on then xi-x+22 else xi-x init xi and on = (xi<=19) -> true every up(18-x+eps) | false every up(x-20) and n = 0 -> (last n)+1 every up(18-x+eps) and stop = false -> true every up(n-10) achieve this goal using if-then-else constructs or with the help of priorities, e.g. based on the order zero-crossings occur in the source code.

I(on, stop, n, x) = ¬stop ∧ n = 0 ∧ 0 ≤ x ≤ 30∧ (x ≤ 19 ∧ on ∨ x > 19 ∧ ¬on) A((on, stop, n, x), (ξ, ǫ)) = 0 ≤ ξ ≤ 30 ∧ -0.1 ≤ ǫ ≤ 0.1 ẋ = ξ -x + 22 if on ξ -x if ¬on (on ′ , stop ′ , n ′ , x ′ ) =    (ff, stop, n, x) if up(x -20) (tt, stop, n + 1, x) if up(18 -x + ǫ) (on, tt, n, x) if up(n -10) (a) Zelus thermostat (b) Intermediate data-flow model globally: 0 ≤ ξ ≤ 30 ∧ -0.1 ≤ ǫ ≤ 0.1 ¬on ẋ = ξ-x on ẋ = ξ-x+22 ¬stop ∧ n = 0 19 < x ≤ 30 0 ≤ x ≤ 19 up(x-20) up(18-x+ǫ) → n ′ = n+1 up(n-10) → stop ′ = tt on ∧ x ≤ 20 22-x ≤ ẋ ≤ 52-x on ∧ x ≥ 20 22-x ≤ ẋ ẋ ≤ 52-x ¬on ∧ x ≥ 17.9 -x ≤ ẋ≤ 30-x ¬on ∧ x ≤ 18.1 -x ≤ ẋ ≤ 30-x ¬stop ∧ n = 0 19 < x ≤ 30 0 ≤ x ≤ 19 tt 17.9 ≤ x ≤ 18.1∧ n ′ = n+1 ∧ q ′ = (n-10 ≤ 0) stop ′ = q ∧ (n-10 ≥ 0)∧ q ′ = (n-10 ≤ 0) tt x = 20
A second requirement is that ∀j : ϕ Z j ⇒ m up(zm), where up(z1), . . . , up(zM ) are the zero-crossings occurring in the program; this condition prevents from taking a discrete transition when no zero-crossing is activated.

Although hybrid system languages often include explicit automata representations, for uniformity of presentation we assume that they have first been transformed into data-flow equations, see [START_REF] Colaço | A conservative extension of synchronous data-flow with state machines[END_REF] for instance.

Example 1. Fig. 1a shows a variant of the classical thermostat example. The input xi represents the external temperature, the input eps models the inaccuracy of the temperature sensor 4 , the continuous state variable x is the room temperature, the discrete Boolean state variable on indicates the state of the heating system, and the discrete integer state variable n counts the number of times the temperature goes from below to above 18 degrees (modulo the uncertainty). At last, the state variable stop becomes true when "n reaches 10 from below". Fig. 1b shows its translation to our intermediate formalism. Observe that this translation factorizes the evolution of discrete variables according to the zero-crossing conditions.

Semantics of zero-crossings.

A zero-crossing is an expression of the form up(z) that becomes true when the sign of z(s, i), an arithmetic expression without tests, switches from negative to positive during an execution. Instead of just a valuation of variables of the form (s k , i k ) zero-crossings are interpreted on an execution fragment of the form (s k-1 , i k-1 ) → (s k , i k ), i.e. two consecutive configurations of an execution trace. We will use the notation (s k-1 , i k-1 , s k , i k ) for short. Several interpretations are possible which are discussed in §4. For now, we arbitrarily select the so-called "contact" semantics, formally defined as:

(s k-1 , i k-1 , s k , i k ) |= up(z(s, i)) iff z(s k-1 , i k-1 ) < 0 z(s k , i k ) ≥ 0 (1)
In other words, a zero-crossing up(z) is activated (and taken into account for computing the next step k+1) if the expression z was strictly negative in the previous step k -1 and evaluates to some positive value or zero in the current step k.

A zero-crossing formula, i.e. a logical combination of zerocrossings, ϕ Z (s, i) is activated iff it evaluates to true when interpreting the zero-crossings up(zm) occurring in ϕ Z using their corresponding constraints over a given (s k-1 , i k-1 , s k , i k ) as in [START_REF] Acary | Numerical Methods for Nonsmooth Dynamical Systems: Applications in Mechanics and Electronics[END_REF].

Semantics.

We define a trace semantics based on an ideal discretization of the continuous equations, following [START_REF] Benveniste | Divide and recycle: types and compilation for a hybrid synchronous language[END_REF]. This semantics uses the theory of non-standard analysis [START_REF] Lindstrøm | An invitation to nonstandard analysis[END_REF][START_REF] Robinson | Non-Standard Analysis[END_REF] to model the way typical simulators proceed, relying on a variable-step numerical integration solver (such as Sundials CVODE [START_REF] Hindmarsh | Sundials: Suite of nonlinear and differential/algebraic equation solvers[END_REF]). Such solvers are given an initial state x0, an ODE ẋ(t) = f (x(t)), and a finite set of zerocrossing expressions zj. Then they integrate the ODE until at least one of the zero-crossings is activated. When this happens, the control is given back to the main simulation loop, which executes one or several discrete execution steps before continuing integration.

According to this approach, an execution of a hybrid dataflow program is a trace (s0, i0)

→ (s1, i1) → (s2, i2) → . . . such that I(s0), →=→c ∪ → d and (s k , i k ) →c (s k+1 , i k+1 ) ⇐⇒ A(s k , i k )∧ ∃l, ∃∂ > 0 : φ ℓ (b k ) ∧ ∀j : ¬ (s k-1 , i k-1 , s k , i k ) |= ϕ Z j (s, i) (b k+1 , x k+1 ) = (b k , x k +e ℓ (s k , i k )•∂) (s k , i k ) → d (s k+1 , i k+1 ) ⇐⇒ A(s k , i k )∧ ∃j :    (s k-1 , i k-1 , s k , i k ) |= ϕ Z j (s, i) ∧ ∀j ′ < j : ¬ (s k-1 , i k-1 , s k , i k ) |= ϕ Z j ′ (s, i) s k+1 = Φj (s k , i k )
where ∂ is an infinitesimal (c.f. non-standard analysis).

A transition →c corresponds to an infinitesimal continuous-time evolution, which is possible only if no zero-crossing condition ϕ Z j has been activated in the previous execution step. A transition → d corresponds to a discrete transition triggered by the first enabled ϕ Z j . We pinpoint some properties of this formalism:

(1) Discrete transitions are always guarded by zero-crossings, and continuous modes are always defined by a Boolean expression over discrete variables, which are piecewise constant in continuous time. This is to go sure that a mode change (change of dynamics) can only happen on discrete transitions.

(2) Furthermore, discrete transitions are urgent, i.e. they must be taken at the first point in time possible.

(3) Zero-crossings may not only be triggered by continuous evolution, but also by discrete transitions. This is the case in Example 1: if the zero-crossing up(18x + ǫ) occurs when n = 9, n is first incremented to 10, activating the zero-crossing up(n -10) which makes stop become true. This feature can cause infinite sequences of discrete zero-crossings. Such a behaviour can be avoided by forbidding circular dependencies between states variables through zero-crossings in the source program.

Partitioned representation. The hybrid data-flow model we have defined does not have any concept of control structure. However, for pedagogical purpose, one can partition the state space to generate an explicit automaton which may be easier to understand, see Fig. 1c. When doing this, partial evaluation may be used to simplify expressions and removing infeasible transitions. This has been done on Fig. 1c.

Standardization. As already mentioned the semantics of the hybrid data flow model is based on non-standard analysis, which allows to give an unambiguous meaning to hybrid systems even if they contain Zeno behavior for instance.

However, the semantics of the output formalism of our translation, i.e. hybrid automata, relies on standard analysis. Hence non-standard behaviors need to be mapped to standard behaviors. This is called standardization: since each standard system has a non-standard representation, a non-standard system is standardizable if it is a non-standard representation of a standard system.

In the following we give some intuitions about the relationships between non-standard and standard analysis; we refer to [START_REF] Lindstrøm | An invitation to nonstandard analysis[END_REF][START_REF] Benveniste | The fundamentals of hyrid systems modelers[END_REF] for further details.

The set * N of non-standard positive integers is N augmented by infinitely large integers. The set * R of nonstandard reals contains R, but also (positive and negative) infinitely large and infinitesimally small numbers, and nonstandard infinitesimals ∂ are the inverse of infinite numbers. For each real number x, * R contains non-standard real numbers that are only infinitesimally away from x. The standardization operator for converting non-standard reals to standard reals st : * R → R identifies these equivalence classes of non-standard reals: ∀x ∈ R : ∀∂ : st(x + ∂) = x where ∂ is an infinitesimal ∈ * R.

W.r.t. continuous evolution, we have the following property: A non-standard sequence consisting of infinitesimal continuous steps (s0, i0) → . . . → (sn, in)

with n ∈ * N, x0 ∈ R p , xn ∈ R p ,
has the following standard meaning: assuming that the input sequence i0 → . . . → in forms a continuous function i : [0, δ] → I, the sequence s0 → . . . → sn corresponds to a continuous function s : [0, δ] → S with

x(δ ′ ) = x0 + δ ′ 0 e ℓ ((b0, x(t)), i(t))dt for δ ′ ∈ [0, δ], δ = st(n∂) ∈ R ≥0
, and I and S denote the input and state space respectively.

However, we can write programs that are not standardizable, i.e. non-standard and standard meaning differ: For example the program fragment b ′ = (x > 0) if up(x) with "crossing" semantics (see §4) gives us b ′ = tt in the non-standard interpretation, but b ′ = ff in the standard interpretation.

Naturally, we can only correctly translate standardizable programs.

LOGICO-NUMERICAL HYBRID AUTOMATA

Hybrid automata [START_REF] Alur | The algorithmic analysis of hybrid systems[END_REF][START_REF] Henzinger | The theory of hybrid automata[END_REF][START_REF] Henzinger | HyTech: A model checker for hybrid systems[END_REF] are a well-established formalism for modelling hybrid systems. Our definition is more general in the sense that we allow also Boolean variables and tests in the expressions appearing in the automata. Fig. 1d depicts an example of a hybrid automaton. Definition 1. A logico-numerical hybrid automaton (HA) is a directed graph defined by L, F, J, Σ 0 where -L is the finite set of locations, -: L → V is a function that returns for each location the flow relation V (s, ẋ) ∈ V relating the state variables and the time-derivatives ẋ of the numerical state variables, and -J ⊆ L×R×L defines a finite set of arcs between locations with the discrete transition relation R(s, s ′ ) ∈ R over the state variables s. -Σ 0 : L → S is a function that returns for each location the set of initial states S 0 ∈ S, which have to satisfy ∀ℓ :

∀s : Σ 0 (ℓ)(s) ⇒ ∃ ẋ : F (ℓ)(s, ẋ).
Further notations:

-

C ℓ (s) = ∃ ẋ : V (s, ẋ) is the staying condition of the flow V = F (ℓ). -G ℓ,ℓ ′ (s) = ∃s ′ : R(s, s ′ ) is the guard of the arc (ℓ, R, ℓ ′ ) ∈ J.
Semantics. We use the following definitions: Let T [0,δ] be the set of differentiable trajectories [0, δ] → R n . The function flowV returns the set of end states of trajectories τ ∈ T starting in the given state and that obey the flow relation V :

flow V (b, x) =        (b, x ′ ) ∃δ > 0, ∃τ ∈ T [0,δ] : τ (0) = x ∧ τ (δ) = x ′ ∧ ∀δ ′ ∈ [0, δ] : C(b, τ (δ ′ )) ∧ ∀δ ′ ∈ (0, δ) : V ((b, τ (δ ′ )), τ (δ ′ ))       
We define the concrete semantics in terms of an execution of a hybrid automaton, which is a (possibly) infinite trace (ℓ0, s0) → (ℓ1, s1) → (ℓ2, s2) → . . . with →=→c ∪ → d and

(ℓ, s) →c (ℓ ′ , s ′ ) ⇔ ℓ = ℓ ′ ∧ V = F (ℓ) ∧ s ′ ∈ flow V ({s}) (ℓ, s) → d (ℓ ′ , s ′ ) ⇔ ∃(ℓ, R, ℓ ′ ) ∈ J : R(s, s ′ ) ∧ C ℓ ′ (s ′ )
If we eliminate all Boolean variables by enumerating their valuations and encoding them with locations, the semantics above will be equivalent to the semantics of standard hybrid automata that deal only with numerical variables.

The concrete semantics of hybrid automata exhibit three kinds of non-determinism: -Non-determinism w.r.t. flow transitions, i.e. the choice between different continuous evolutions due to the differential inclusions defined by the vector field V . -Non-determinism w.r.t. flow and jump transitions: The choice between flow and jump transitions due to an overlapping of staying condition and guards. -Non-determinism w.r.t. jump transitions, which is the choice between several jump transitions.

SEMANTICS OF ZERO-CROSSINGS

The fundamental difference between the zero-crossing concept used in our input language and the combination of staying and jump conditions in our output language is that the activation of a zero-crossings depends on the history (i.e. a part of the past trajectory) whereas the truth value of staying and jump conditions only on the current state.

Continuous vs. discrete zero-crossings. As mentioned in §2, a zero-crossing can be activated in two ways: -It can be triggered by a continuous time evolution, as up(x -20) in Fig. 1c; in this case it is active during the second step of an execution fragment s i -→c s ′ i ′ -→ d s ′′ ; -It can be triggered by a discrete transition, as up(n -10) in Fig. 1c; in this case it is active during the second step of an execution fragment s i -→ d s ′ i ′ -→ d s ′′ ; Because a zero-crossing may depend on both discrete and continuous variables, the same zero-crossing up(e) can be triggered in both ways in an execution. We will use the terms continuous (resp. discrete) zero-crossing for indicating its source of activation.

Three semantics for zero-crossings. We consider an execution fragment

i k-1 --→ s k-1 i k -→ s k and we define z k = z(s k , i k ).
There are three natural choices for the semantics of zero-crossings:

-"At-zero" semantics :

z k-1 ≤ 0 ∧ z k ≥ 0 -"Contact" semantics : z k-1 < 0 ∧ z k ≥ 0 -"Crossing" semantics : z k-1 ≤ 0 ∧ z k > 0
Figs. 3b, 3e and 3h illustrate the activation of continuous zero-crossings for some typical trajectories according to each semantics.

The last two semantics are used in simulators. The zerocrossing semantics of Simulink is the disjunction of these semantics. In Modelica it is up to the programmer to choose between these two semantics.

We state the first option, because it fits better to the semantics of hybrid automata (as it does not involve strict inequalities).

Chattering behaviour. An issue specific to the "crossing" semantics is that it is possible to write programs that produce executions that contain periodic sequences of infinitesimal continuous evolutions with distinct dynamics. This happens for example when a trajectory chatters along a surface with opposed zero-crossings, like in the following example.

Example 2. (see Fig. 2)

I = (b∧x = -1∧y = 0) tt →            b ′ = ff if up(x) tt if up(-x) ẋ = 1 ẏ = 1 if b -1 if ¬b
In some cases it is possible to standardize such systems by identifing the chattering behavior and replace it by a socalled sliding mode [14, 32, 1], i.e. a dynamics that defines the corresponding trajectory "in" this surface. However, this is not feasible in the general case (i.e. a specification which does not correspond necessarily to a physical model). Thus, we will translate such programs into hybrid automata that allow chattering in their concrete semantics. (b) Equivalent sliding mode Figure 2: Sliding modes §5 focuses on the translation of continuous zero-crossings, whereas §6 will discuss the case of discrete zero-crossings, the translation of which is much less dependent on the choice of one of the three zero-crossing semantics. However, because of the limitations of the hybrid automata model, in all cases the translation will add behavior that is not present in the original program.

TRANSLATION OF CONTINUOUS ZERO-CROSSINGS

Simplest case: one zero-crossing, no inputs

We investigate here the translation of continuous zerocrossings of the form up(z(x)): for the sake of simplicity, we assume that there are neither inputs i nor discrete variables b in z. We consider the simple case of an origin location l1 with a single discrete transition s ′ = Φ(s) if up(z(x)) going from l1 to a location l2, such that φ1(b) ∧ (s ′ = Φ(s)) ⇒ φ2(b ′ ), see Fig. 3a. As the satisfaction of a zero-crossing depends on the history, the principle of the translation is to add locations to record the history of the continuous evolution.

"At-zero" semantics. The translation of "at-zero" semantics (z k-1 ≤ 0 ∧ z k ≥ 0) is depicted in Fig. 3c. The origin location is partitioned in two locations: there is a discrete transition from left to right, but not from right to left to force the urgency of the discrete transition when z = 0 is reached from below 0. The zero-crossing condition translates to z = 0. The rationale for the condition z = 0 is based on the assumption of continuity of the function z(t) = z(x(t)) and the urgency of the zero-crossing: z(t k-1 ) < 0 ∧ z(t k ) ≥ 0 with t k-1 < t k implies that there exists t ∈ (t k-1 , t k ] such that z(t) = 0.

φ1 φ2 s ′ = Φ(s) if up(z) (a) Single zero-crossing z t ∂ ∂ ∂ (b) Exact "at-zero" semantics φ1 ∧ z ≥ 0 φ1 ∧ z ≤ 0 φ2 tt z = 0 ∧ s ′ = Φ(s) (c) Translation according to "at-zero" semantics z t (d) Induced semantics z t (e) Exact "contact" semantics φ1 ∧ z ≥ 0 φ1 ∧ z ≤ 0 φ1 ∧ z ≤ 0 φ2 tt z < 0 z = 0 ∧ s ′ = Φ(s) (f) Translation according to "contact" semantics z t (g) Induced "contact" semantics z t ∂ ∂ ∂ (h) Exact "crossing" semantics φ1 ∧ z ≥ 0 φ1 ∧ z ≤ 0 φ1 ∧ 0 ≤ z ≤ ǫ φ2 tt tt 0 ≤ z ≤ ǫ ∧ s ′ = Φ(s) (i)
This translation induces two kinds of approximations in terms of executions: -We lose urgency for all trajectories but the second one in Fig. 3d. In case of the first trajectory the zero-crossing may be triggered in a dense interval of time. -We add a jump transition in the fourth trajectory because one is not able to distinguish whether the state z = 0 is reached from below or from above 0.

We will not consider any more the "at-zero" semantics in the sequel, as -to our knowledge -it is not used by any simulation tool.

"Contact" semantics. In order to translate the "contact" semantics defined as z k-1 < 0 ∧ z k ≥ 0, we split the original location into three locations as depicted on Fig. 3f. The two locations with the staying condition z ≤ 0 are connected by a transition guarded by z < 0: this is in order to check that the trajectory was actually strictly below zero before touching zero. This prohibits the triggering of the jump transition in the first, third and last trajectory in Fig. 3g. This induces the following approximation: -The loss of urgency for the fifth trajectory that touches (possibly several times) the line z = 0 from below. Observe, that the "at-zero" translation in Fig. 3c is actually a sound translation of the "contact" semantics, though with coarser approximations.

"Crossing" semantics. The "crossing" semantics (z k-1 ≤ 0 ∧ z k > 0) is more subtle to translate. By continuity of the function z(t) = z(x(t)) we can deduce that z(t) = 0 is valid at the zero-crossing point in standard semantics: by standardizing z(t) ≤ 0 ∧ z(t+∂) > 0 we get st(z(t)) = st(z(t+ ∂)) = 0.

However, we cannot simply reuse the "at-zero" translation in Fig. 3c, because it is not sound w.r.t. chattering behaviors: in Ex. 2 time cannot advance, because only discrete transitions can be taken. Since we do not rely on standardizing chattering behaviors we have to allow chattering in the standard semantics. For that reason we allow the trajectories to actually go beyond zero, but only up to a constant ǫ > 0 (see Fig. 3i). As a consequence, we have the following approximation: -Urgency is completely lost. In case of the second, third and last trajectories the zero-crossing may be triggered in a bounded time interval with a dense interval of values for z (see Fig. 3j). Observe, that this translation simulates the translations of the other two semantics.

Remark 1 (Choice of ǫ). Any translation involving an ǫ close to zero is not really well-suited for verification: computations with arbitrary-precision rationals become indeed

very expensive ( e.g. least common denominators become huge).

One zero-crossing with inputs

Now we investigate the translation of zero-crossings of the form up(z(x, i)), where the inputs i have to satisfy an assertion A(s, i), see §2. We assume that in the discrete infinitesimal semantics of §2 inputs tend to continuous trajectories (between two discrete transitions). Inputs allow us to introduce non-determinism in a model, as illustrated by Fig. 1. The principle of the translation remains the same as in the previous section and depicted on Fig. 3, except that the computation of jump and flow transition relations involves an existential quantification of the inputs i. The process is illustrated by Fig. 4.

We use the notation ψ = ¬ψ, where • denotes the topological closure operator. We have for instance (z ≤ 0) = z ≥ 0.

Considering the "contact" semantics and using the continuity of the function z(x(t), i(t)) during continuous evolution (see §2) the condition

∃i k-1 , i k : z(x k-1 , i k-1 ) < 0 ∧ A(s k-1 , i k-1 ) ∧ z(x k , i k ) ≥ 0 ∧ A(s k , i k ) ∧ s ′ = Φ(s k , i k ) is equivalent to ∃i k-1 , i k : z(x k-1 , i k-1 ) < 0 ∧ A(s k-1 , i k-1 ) ∧ z(x k , i k ) = 0 ∧ A(s k , i k ) ∧ s ′ = Φ(s k , i k )
which in turn is equivalent to

∃i : z(x k-1 , i) < 0 ∧ A(s k-1 , i) ∧ ∃i : z(x k , i) = 0 ∧ A(s k , i) ∧ s ′ = Φ(s k , i) (2)
-The first line of Eqn. (2) defines the new guard of the transition between the second and third locations of Fig 3f:

∃i : A(s, i) ∧ z(x, i) < 0 -
The second line gives us the new transition relation between the third and fourth locations of Fig. 3f:

R(s, s ′ ) = ∃i : A(s, i) ∧ z(x, i) = 0 ∧ s ′ = Φ(s, i)
-The new flow relation of the second and third locations is ∃i :

A(s, i) ∧ z(x, i) ≤ 0 ∧ φ1(b) ∧ ẋ = e1(s, i)
which induces the staying condition

ψ23(s) = ∃i : A(s, i) ∧ z(x, i) ≤ 0)
-The new flow relation of the first location of Fig. 3f is

V1(s, ẋ) = ∃i : A(s, i) ∧ z(x, i) ≥ 0 ∧ φ1(b) ∧ ẋ = e1(s, i)
The result is illustrated by Fig. 4b. One can strengthen the flow relation V1 by conjoining it with ψ23, so as to minimize the non-determinism between staying in the first location or jumping to the second location, as done in Fig. 4c. 5 5 We use the operator instead of ¬ in order to obtain a topologically closed flow relation. Example 3. Fig. 4b illustrates this translation on the original system of Fig. 4a, where b, x, y are state variables and ξ is a numerical input variable constrained by the assertion. The jump condition of the rightmost transition is obtained from ∃ξ :

A(x, y, ξ) = -0.1 ≤ ξ ≤ 0.1 ¬b b b ′ = tt y ′ = ξ if up(x+ξ) (a) Zero-crossing with input ξ ¬b ∧ x ≥ -0.1 ¬b ∧ x ≤ 0.1 ¬b ∧ x ≤ 0.1 b tt x < 0.1 -0.1 ≤ x ≤ 0.1 ∧ b ′ ∧ x ′ = x ∧ y ′ = -x (b) Translation according to "contact" semantics ¬b ∧ x ≥ 0.1 ¬b ∧ x ≤ 0.1 ¬b ∧ x ≤ 0.1 b tt x < 0.1 -0.1 ≤ x ≤ 0.1 ∧ b ′ ∧ x ′ = x ∧ y ′ = -x (
(-0.1 ≤ ξ ≤ 0.1 ∧ x+ξ = 0 ∧ b ′ = tt ∧ x ′ = x ∧ y ′ = ξ) = ∃ξ : (-0.1 ≤ x ≤ 0.1 ∧ x = -ξ ∧ b ′ ∧ x ′ = x ∧ y ′ = -x) = -0.1 ≤ x ≤ 0.1 ∧ b ′ ∧ x ′ = x ∧ y ′ = -
x that we obtain the non-trivial relation y = -x after the jump transition.

Logical combinations of zero-crossings

We consider here a discrete transition function of the form s ′ = Φ(s, i) if ϕ Z (s, i) where ϕ Z is a logical combination of zero-crossings up(z1), . . . , up(zM ) satisfying the assumption of §2.

Why do we need such logical combinations? Conjunctions and negations typically occur when combining two parallel equations s ′ i = Φi if up(zi) for i = 1, 2, which results in an equation

(s ′ 1 , s ′ 2 ) =    (Φ1, Φ2) if up(z1) ∧ up(z2) (Φ1, s2) if up(z1) ∧ ¬up(z2) (s1, Φ2) if up(z2) ∧ ¬up(z1) A specification of the form s ′ = Φ1 if up(z1) Φ2 else if up(z2) is similarly translated to s ′ = Φ1 if up(z1) Φ2 if ¬up(z1) ∧ up(z2)
Disjunctions allow to express that the same transition may be triggered by different zero-crossings:

s ′ = Φ if up(z1) ∨ up(z2)
Because successive graph refinements are cumbersome to describe, we reformulate the translation scheme of the previous sections by using additional discrete state variables to the system, rather than by introducing locations. This will make it easier to explain this generalization. We sketch this principle using the "contact" semantics (the translation for the general case will be presented in §7).

To encode locations, we add M discrete state variables q1 . . . qM of the enumerated type {above, below, ready} for each distinct zero-crossing up(zm) occuring in the zero-crossing formulas ϕ Z . -Their transition relations are defined as We can now build the global flow and discrete transition relations: R((q, s), (q

Rm = match qm with above → q ′ m ∈ {above, below} below → zm < 0 ∧ q ′ m = ready ∨ q ′ m = qm ready → zm = 0 ∧ q ′ m ∈ {above, below} ∨ q ′ m =
′ , s ′ )) = m Rm ∧ (¬H ∧ s ′ = s ∨ H ∧ s ′ = Φ) V ((q, s), ẋ) = m Cm ∧ ℓ (φ ℓ (b) ∧ ẋ = ėℓ (s)) (3) with H = ϕ Z [∀m : up(zm) ← Gm]
where e[x ← y] means that x is substituted by y in expression e.

In order to obtain an explicit automaton one has to enumerate the valuations of the discrete state variables q and to encode them into explicit locations (see §8).

It is interesting to mention that this translation keeps enough information in order to preserve urgency in case of conjunctions like s ′ = Φ if up(z1) ∧ up(z2) where the trajectory can move all around the intersection z1 = 0 ∧ z2 = 0 while not satisfying both zero-crossings at the same time.

TRANSLATION OF DISCRETE ZERO-CROSSINGS

Discrete zero-crossings are activated by discrete transitions. Discrete zero-crossings occur in so-called zero-crossing cascades, which are sequences of zero-crossings of which the first one is triggered by continuous evolution, whereas the others are discrete zero-crossings. Example 1 contains such a zero-crossing cascade, which is commented in §2 point [START_REF] Alur | The algorithmic analysis of hybrid systems[END_REF].

The translation explained in §5.1 is not sound for discrete zero-crossings, because we have supposed that the zerocrossings are activated by continuous evolution.

Principle of translation. The translation that we propose applies the same principle as above to encode the history of the execution into locations (using discrete state variables). We explain it using the "contact" semantics (again without inputs and logical combinations of zero-crossings). We consider s ′ = Φ if up(z) and we introduce a Boolean variable q d , which holds at each step k the value of z < 0 at step k -1.

-The evolution of q d is defined by the initial state q d = ff and the relation R d = ((q d ) ′ = (z < 0)); -The condition up(zm) is translated to the activation condition G d = (q d ∧ z ≥ 0); -The global transition relation R is generated as in Eqn. [START_REF] Alur | The algorithmic analysis of hybrid systems[END_REF].

Interrupting continuous evolution. The transitions as translated above are not urgent, i.e. the continuous states can evolve on intermediate states of a cascade. We need to prohibit this evolution explicitly if one of the discrete zerocrossings is activated. This is done by strengthening the global flow relation V (q, s, ẋ) with

V ′ = V ∧ G d .
In case of inputs, we have G d = (q d ∧ z(s, i) ≥ 0) and we take V ′ = V ∧ (∀i : G d ): the idea is that in a state (q, s), if the discrete zero-crossing is activated for any input (i.e. ∀i : G d ), then the continuous evolution is blocked. Otherwise, for some input, the discrete zero-crossing is not activated and the continuous evolution should be possible.

Remark 2. A zero-crossings can be both discrete and continuous, e.g. up(x + n). In this case it is translated twice: once as a continuous zero-crossing and a second time as a discrete one.

Remark 3 (Compressing Cascades). Zero-crossing cascades can be "compressed" into a single discrete transition triggered by a continuous zero-crossing by composing the discrete transitions forming the cascade. This is possible if there are no instantaneous cyclic dependencies between the variables. The advantage of this kind of preprocessing is that the translation does not have to deal with discrete zero-crossings. However, care must be taken w.r.t. safety verification, because this transformation does not preserve the set of reachable states (it removes intermediate states).

THE COMPLETE TRANSLATION

We give here the formulas for the complete translation of a hybrid data-flow program

I(s) , A(s, i) ∧            ẋ = • • • e ℓ (s, i) if φ ℓ (b) • • • s ′ = • • • Φj (s, i) if ϕ Z j (s, i) • • •
as defined in §2 to a hybrid automaton by combining all the concepts presented in §5 and §6.

We use the notation ζ σ m to denote the constraints induced by a zero-crossing up(zm), e.g.

ζ •=0 m = zm = 0 or ζ 0<•≤ǫ m = 0 < zm ≤ ǫ .
Discrete zero-crossings. For each discrete zero-crossing up(zm) we introduce a Boolean state variable

q d m . R d m = (q ′d m = ζ σ m ) G d m = (q d j ∧ ζ σ m ) σ σ "contact" • < 0 • ≥ 0 "crossing" • ≤ 0 • > 0
Continuous zero-crossings. For each continuous zerocrossing up(zm) we introduce a state variable q c m .

-Their transition relations are defined as follows:

θ σ "contact" • < 0 • = 0 "crossing" • = 0 0 ≤ • ≤ ǫ R c m = match q c m with above → q ′c m ∈ {above, below} below → ((q c m ) ′ = q c m ) ∨ ((q c m ) ′ = ready) ∧ ζ θ m ready → (q c m ) ′ ∈ {above, below} ∧ ζ σ m ∨ (q c m ) ′ = q c m -The activation conditions G c m are defined as G c m = (q c m = ready) ∧ ζ σ m σ "contact" • = 0 "crossing" 0 ≤ • ≤ ǫ -Using ψ = ℓ φ ℓ (b) ∧ ẋ = e ℓ (
s, i) we define the partial flow relations (containing the staying conditions):

σ "contact" • ≤ 0 "crossing" 0 ≤ • ≤ ǫ Vm = match q c m with above → ∃i : A(s, i) ∧ ζ •≥0 m ∧ ψ ∧ ∃i : A(s, i) ∧ ζ •≤0 m below → ∃i : A(s, i) ∧ ζ •≤0 m ∧ ψ ready → ∃i : A(s, i) ∧ ζ σ m ∧ ψ Transition relations. We define Gm = G c m ∨ G d m and Rm = R c m ∧ R d m
. Now, we can finally put things together and define the jump and flow transition relations: R((q, s), (q ′ , s ′ )) = ∃i :

       A(s, i) ∧ m Rm ∧ ¬ j Hj ∧ s ′ = s ∨ j Hj ∧ s ′ = Φj V ((q, s), ẋ) = m Vm((q, s), ẋ) ∧ ∀i : A(s, i) ∧ j H d j with Hj = ϕ Z j [∀m : up(zm) ← Gm]
. We obtain a hybrid automaton {ℓ0}, F, J, Σ 0 with -F (ℓ0) = V , -J = {(ℓ0, R, ℓ0)}, and -Σ 0 (ℓ0) = {(q, s) | q d = ff ∧ m q c m ∈ {above, below} ∧ I(s)} For the proofs of the complete translation we refer to [START_REF] Schrammel | From hybrid system data-flow to hybrid automata: A complete translation[END_REF].

DISCUSSION

We have presented the complete translation of a hybrid data-flow specification to a hybrid automaton. However, further preprocessing steps are necessary to enable verification using classical hybrid analysis methods.

Explicit representation. As explained in §5.3 we have chosen to present our translation by encoding the locations of the HA with N additional finite-state variables q. This results in a HA with a single location and a single self-loop jump transition. Of course, it is possible to expand this "compressed" representation into a more explicit one, such as shown in Figs. 3 and4. This is done by enumerating the valuations of these finite-state variables and by partitioning the system into these O(2 N ) states. As already mentioned in §2, partial evaluation may be used to simplify expressions and to remove infeasible jump transitions.

Convexification of staying conditions and guards.

The induced staying conditions C(s) and guards G(s) of jump transitions might be non-convex w.r.t. numerical constraints. For verification it is necessary to transform these conditions into the form k ∆ k with ∆ k = φ k (b) ∧ ϕ C k (s), where φ k (b) is an arbitrary formula over Boolean variables and ϕ C k (s) is a conjunction of numerical constraints. For staying conditions, the system has to be partitioned according to these ∆ k ; for guards, arcs are split w.r.t. the ∆ k . ∧( ẋ = 1-x) ∨ (¬b1 ∧ b2) ∧ (0 ≤ x ≤ 5) ∧ ( ẋ = 1) has to be transformed into (b1 ∨ ¬b2) ∧ (x ≤ 0) ∧ ( ẋ = 1-x) ∨ (b1 ∨ ¬b2) ∧ (x ≥ 5) ∧ ( ẋ = 1-x) ∨ (¬b1 ∧ b2) ∧ (0 ≤ x ≤ 5) ∧ ( ẋ = 1) Then, the system is going to be partitioned into three locations, one for each line.

Approximations during analysis. In §5.1 we have explained that the translation to hybrid automata loses several properties, like determinism and urgency, which may result in an overapproximation in terms of reachable states. Moreover, hybrid reachability analysis methods further approximate the reachable states with (finite disjunctions of) convex sets, such as convex polyhedra.

The translation with "contact" semantics involves strict inequalities. Thus, the analysis may benefit from the ability of representing open sets. A suitable abstract domain might be in this case convex polyhedra with strict inequalities [START_REF] Bagnara | Not necessarily closed convex polyhedra and the double description method[END_REF]. Otherwise, if the analysis can only handle closed sets, the translation with "contact" semantics (Fig. 3g) will behave like the one for "at-zero" semantics (Fig. 3d).

Preliminary experiments. We have implemented a prototype tool that makes use of the BddApron library [START_REF] Jeannet | Bddapron: A logico-numerical abstract domain library[END_REF] to handle logico-numerical formulas represented as MtBdds.

First experiments showed that -as expected -the major parameter affecting performance is the number of zerocrossings, which becomes apparent when making locations explicit as described at the beginning of this section. In the applications that we are targeting, i.e. synchronous controllers connected to their physical environment, zerocrossings are (1) those used for modeling the sampling of inputs and (2) those in the environment model. Since the number of (1) is usually small, the total number of zerocrossings inherently depends on the complexity of the environment model in practice.

CONCLUSION

We have presented a complete translation of a hybrid data-flow formalism to logico-numerical hybrid automata. In comparison to previously proposed translations, our translation handles zero-crossings.

To achieve this, we considered a simple yet expressive hybrid data-flow formalism to which large subsets of existing hybrid system languages can actually be reduced.

We discussed different choices of zero-crossing semantics and their possible translations to hybrid automata. Since hybrid automata are not as expressive as the source language, we can only provide sound over-approximations of the original semantics.

However, this is counterbalanced by the fact that existing hybrid verification tools such as HyTech [START_REF] Henzinger | HyTech: A model checker for hybrid systems[END_REF], PHaver [START_REF] Frehse | PHAVer: Algorithmic verification of hybrid systems past HyTech[END_REF] and SpaceEx [START_REF] Frehse | SpaceEx: Scalable verification of hybrid systems[END_REF] are all based on the standard hybrid automata model.

Though, these tools require to encode Boolean variables explicitly in locations. As this enumeration results in an exponential blow-up of the hybrid automaton size, we assume that this is a major bottleneck in verifying controllers with complex discrete state spaces jointly with their physical environment. Therefore future work will comprise the development of methods and tools for combining classical hybrid system analysis with implicit handling of Boolean variables in order to counter state space explosion. Our translation to logico-numerical hybrid automata lays the basis for such an approach.

Figure 1 :

 1 Figure 1: Translation of the Thermostat example described in Example 1

  Translation according to "crossing" semantics z ǫ t (j) Induced "crossing" semantics Notes: (1) The arrows pointing upwards indicate on the left-hand side the points where zero-crossings are activated, and on the right-hand side the points where the jump transition may be taken non-deterministically. The dotted trajectories indicate that the preceding transition is urgent. (2) When s does not appear in the jump condition of a HA, the equality s ′ = s is implicit. (3) The flow function ẋ = f c (s) in the first location in Fig. 3a, translates to the flow relation V1( ẋ, s) = (φ1(b) ∧ ẋ = f c (s)), not shown in the figures.

Figure 3 :

 3 Figure 3: Zero-crossing semantics of the hybrid data-flow language and their translations. From left to right: typical trajectories in the original semantics, proposed translation to hybrid automata, and their typical trajectories.

Figure 4 :

 4 Figure 4: Translation of a continuous zero-crossing with inputs, described in Example 3

  qm -The staying condition defined by the zero-crossing up(zm) is: Cm = match qm with above → zm ≥ 0 below → zm ≤ 0 ready → zm ≤ 0 -The activation condition Gm associated to the zero-crossing up(zm) is Gm = (qm = ready) ∧ (zm = 0)

Fig. 5 Figure 5 :

 55 Figure 5: Conjunction of two zero-crossings

Example 4 .

 4 The non-convex flow transition V(b1 ∨ ¬b2) ∧ non-convex numerical condition (x ≤ 0 ∨ x ≥ 5)

http://www.mathworks.com

http://www.modelica.org

Stateflow also allows to trigger discrete jumps by ordinary guards that are not interpreted as zero-crossings.

We do not use eps in the expression up(x-20), in order to show an example of a deterministic zero-crossing.

This work was supported by the Anr project Vedecy and the Inria large-scale initiative Synchronics.


Peter Schrammel
email: peter.schrammel@inrialpes.fr

Bertrand Jeannet
email: bertrand.jeannet@inrialpes.fr

Extending Abstract Acceleration Methods to Data-Flow Programs with Numerical Inputs 1

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 data-flow programs with Boolean and numerical variables, e.g. Lustre programs, firstly requires the enumeration of the Boolean states in order to obtain a control graph with numerical variables only. Secondly, acceleration methods have to deal with the non-determinism introduced by numerical input variables. In this article we address the latter problem by extending the concept of abstract acceleration of Gonnord et al. to numerical input variables.

Introduction

This paper considers the reachability analysis of synchronous programs manipulating Boolean and numerical variables, and more generally the reachability analysis of logico-numerical programs, that are symbolic automata combining Boolean and numerical variables. The applications of such a reachability analysis are for instance the verification of safety properties [START_REF] Halbwachs | Synchronous observers and the verification of reactive systems[END_REF] or model-based testing [START_REF] Jeannet | Symbolic test selection based on approximate analysis[END_REF].

Abstract interpretation and acceleration. Since the reachability problem is not decidable for logico-numerical programs, two main approaches have been studied: (i) Abstract interpretation techniques [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF][START_REF] Cousot | Abstract interpretation and application to logic programs[END_REF] compute only an overapproximation of the reachability set, but terminate always. (ii) Acceleration techniques [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] Bardin | Flat acceleration in symbolic model checking[END_REF] compute the exact reachability set in favorable cases, but without guarantee for termination. In both approaches, the set of reachable states is obtained by solving iteratively an equation of the form X = X 0 ∪ post(X) where X is a set of states, X 0 the initial set, and post the postcondition operator associated with the program.

Abstract interpretation is a classical method for analyzing programs with infinite state space. The key idea is to approximate sets of states X by an element Y of an abstract domain. A classical abstract domain for numerical invariants X ∈ ℘(R n ) is the domain of convex polyhedra P ol(R n ) [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF], that can be represented as a conjunction of linear inequalities. An approximation of the reachable set is computed by solving iteratively the equation Y = Y 0 ⊔ post(Y ) in the abstract domain. In order to ensure termination when the abstract domain contains infinitely increasing sequences, an extrapolation operator called widening is applied, which induces additional approximations.

The idea of acceleration is to accelerate cycles τ in the control structure of a program, by computing the effect of their transitive closure τ * on a set of states, see Fig. 1. 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 the method is semi-complete: One starts enumerating and accelerating non-elementary cycles (which form an infinite set) in the hope of converging after a finite number of steps to the smallest fixed point. 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].

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. Gonnord et al. [START_REF] Gonnord | Combining widening and acceleration in linear relation analysis[END_REF][START_REF] Gonnord | Accélération abstraite pour l'amélioration de la précision en Analyse des Relations Linéaires[END_REF] have proposed the concept of abstract acceleration which combines these approaches: Wherever possible, elementary loops are accelerated in the abstract domain, and in any other cases (nested loops, too expressive transitions) one resorts to the use of widening to guarantee the convergence of the approximated fixed point computation.

Abstract acceleration and logico-numerical programs. Acceleration techniques such as [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] consider purely numerical automata. There are two shortcomings of the abstract acceleration approach when applied to logiconumerical programs such as Lustre [START_REF] Caspi | LUSTRE: a declarative language for realtime programming[END_REF] data-flow programs:

(1) In order to reduce such a program to a purely numerical automaton, all possible valuations of Boolean state variables need to be enumerated and encoded in a control graph. This partitioning and partial evaluation process may lead to a combinatorial explosion of control locations. (2) The concept of input variables as encountered in Lustre programs requires an extension of the results of [START_REF] Gonnord | Combining widening and acceleration in linear relation analysis[END_REF][START_REF] Gonnord | Accélération abstraite pour l'amélioration de la précision en Analyse des Relations Linéaires[END_REF]. As opposed to Boolean input variables that can be encoded in an automaton by finite non-deterministic choices, numerical input variables demand a more specific treatment. This article especially addresses point 2, although point 1 is our ultimate goal.

Contributions and outline. Our contribution is to extend the abstract acceleration concept as introduced in [START_REF] Gonnord | Combining widening and acceleration in linear relation analysis[END_REF] to systems with numerical inputs, which raises some subtle points. In particular we show how to accelerate loops composed of a translation with resets and inputs, provided that the guard of the loop constrains separately state and input variables. Without this restriction indeed, one can emulate any affine transformation without inputs. After some preliminary notions in Section 2 about the considered program model, the operations on convex polyhedra and the general verification framework that we use for analysis, we recall the main results of abstract acceleration in Section 3. Section 4 details our contribution. We conclude in Section 6. An execution of such a system is a sequence

s 0 i 0 -→ s 1 i 1 -→ . . . s k i k -→ . . . such that init(s 0 ) and for any k ≥ 0, assert(s k , i k ) ∧ s k+1 = f (s k , i k ).
This program model corresponds for example to the output of the frontend compilation of synchronous data-flow programs like Lustre and includes various models of counter automata (by emulating locations using Boolean variables) [START_REF] Bardin | Flat acceleration in symbolic model checking[END_REF]. A control graph manipulating only numerical variables can be generated from this program model by performing 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 eliminating Boolean input variables by 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 paper the abstract domain of convex polyhedra for representing invariants on numerical variables. Besides classical operations (intersection, convex hull, assignments of variables by linear expressions, . . . ) described e.g. in [START_REF] Halbwachs | Verification of real-time systems using linear relation analysis[END_REF], we will use the following operations:

The time elapse operation [START_REF] Halbwachs | Verification of real-time systems using linear relation analysis[END_REF]

X ր D = {x + td | x ∈ X, d ∈ D, t ∈ R ≥0 } is practically implemented as follows: Let (V X , R X ) respectively (V D , R D ) be the systems of generators of the polyhedra X and D then (V X , R X ∪ V D ∪ R D ) is a system of generators of the polyhedron X ր D.
The Minkowski sum [START_REF] De Berg | Computational Geometry: Algorithms and Applications[END_REF] of two polyhedra X = X 1 + X 2 is defined as

X(x) = ∃x 1 , x 2 : (x = x 1 + x 2 ) ∧ X 1 (x 1 ) ∧ X 2 (x 2 ).

Overview of Acceleration and Abstract Acceleration

As mentioned in the introduction, the idea of acceleration (Fig. 1) is to replace a loop transition τ by a single transition τ * that computes the transitive closure of τ . Abstract acceleration [START_REF] Gonnord | Combining widening and acceleration in linear relation analysis[END_REF][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 its convex hull τ ⊗ (X) ⊇ τ * (X). 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 loop transition τ will have 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 (1)
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 if C is the zero matrix,

• a translation if C is the identity matrix,

• a translation with resets (or translation/reset) if C is a diagonal matrix with zeros and ones only,

• a periodic affine transformation if ∃p > 0 : C p = C 2p ,
• a general affine transformation otherwise. Existing acceleration methods cannot deal with general affine transformations. We will not discuss the case of periodic affine transformations, as it seems to be of limited practical interest.

In the context of abstract acceleration, [START_REF] Gonnord | Combining widening and acceleration in linear relation analysis[END_REF][START_REF] Gonnord | Accélération abstraite pour l'amélioration de la précision en Analyse des Relations Linéaires[END_REF] shows that translations

X d d G G(x -d) Fig. 2
. Acceleration of a translation loop starting from X (dark shadowed) resulting in τ ⊗ (X) (whole shadowed area).

x 1

x 2 X d 1 G d 2 X d 1 d 1 G d 2 G(x -Cd)
Fig. 3. Acceleration of a loop with translations/resets: On the left hand side, the application of τ (X) -here, with x ′ 1 = x1 + d1 and x ′ 2 = d2, yields a polyhedron (bold line including arrow) containing the reset values. The accelerated transition gives τ ⊗ (S) (shadowed) on the right hand side.

(Fig. 2) and translations with resets (Fig. 3) can be accelerated as follows, with X denoting a convex polyhedron and G(x) = (Ax ≤ b) an affine guard (which is also a convex polyhedron):

Theorem 3.1 Let τ be a translation G → x ′ = x+d. The convex polyhedron τ ⊗ (X) = X ⊔ (X ⊓ G) ր d ⊓ G(x -d) is a convex over-approximation of τ * (X). Theorem 3.2 Let τ be a translation with resets G → x ′ = Cx + d. The convex polyhedron τ ⊗ (X) = X ⊔ τ (X) ⊔ (τ (X) ⊓ G) ր Cd ⊓ G(x -Cd) is a convex over-approximation of τ * (X).
Remark 3.3 Theorem 3.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 obtained formula.

Remark 3.4 Ideally, τ ⊗ (X) as defined in Theorems 3.1 and 3.2 should be the best over-approximation 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 τ : [START_REF] Abdulla | Using forward reachability analysis for verification of lossy channel systems[END_REF][START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF], whereas the best overapproximation of τ * (X) = {1, 3, 5} is the interval [START_REF] Abdulla | Using forward reachability analysis for verification of lossy channel systems[END_REF][START_REF] Caspi | LUSTRE: a declarative language for realtime programming[END_REF]. This is because the operations involved in τ ⊗ (X) manipulate dense sets and do not take into account arithmetic congruences. We will not improve on this in this work, but we will point out in our proofs where this dense approximation takes place.

x 1 ≤ 4 → x ′ 1 = x 1 + 2. τ ⊗ (X) =
These theorems can be applied on a control graph by dividing locations with a single self-loop (as shown in Fig. 1). If there are several self-loops in a location then the cases where guards overlap and where they are disjoint must be distinguished, which results in a more elaborate division of the location. [START_REF] Gonnord | Accélération abstraite pour l'amélioration de la précision en Analyse des Relations Linéaires[END_REF] gives a range of methods for dealing with more complex cases.

Abstract Acceleration with Numerical Inputs

We now extend numerical abstract acceleration w.r.t. numerical input variables y. This means that we consider transitions of the form

A L 0 J x y ≤ b k Ax+Ly≤b ∧ Jy≤k → x ′ = C T x y + u Cx+Ty+u (2)
Note that the 0 in the matrix of the guard does not imply a loss of generality.

A fundamental observation is that any general affine transformation without inputs Ax ≤ b → x ′ = Cx + d can be expressed as a "reset with inputs" (Ax ≤ b ∧ y = Cx + d) → x ′ = y. This means that there is no hope to get precise acceleration for such resets 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 when the constraints on the state variables do not depend on the inputs, i.e. when L = 0 in Eqn. ( 2) and the guard is of the form Ax ≤ b ∧ Jy ≤ k. We call the resulting guards simple guards. Otherwise, we provide in Section 4.3 a weaker over-approximation of the exact result for general guards. First of all, assume that in a translation without inputs d is not constant, but constrained to be inside a convex polyhedron D. Then Theorem 3.1 can be generalized to such polyhedral translations.

Proposition 4.1 Let τ be a transition G → x ′ = x + d with G(x) = (Ax ≤ b), d ∈ D and D a convex polyhedron. The set τ ⊗ (X) = X ⊔ τ (X ⊓ G) ր D is a convex over-approximation of τ * (X).
Note that τ (X) can be implemented by standard polyhedra operations:

τ (X) = (X ⊓ G)+D. x ′ ∈ k≥1 τ k (X) ⇔ ∃k ≥ 1, ∃x 0 ∈ X, ∃d 1 , . . . , d k ∈ D : x ′ = x 0 + k j=1 d j ∧ G(x 0 ) ∧ ∀k ′ ∈ [1, k-1] : G(x 0 + k ′ j=1 d j ) ⇔ ∃k ≥ 1, ∃x 0 ∈ X, ∃d, d k ∈ D, ∃x k-1 : x k-1 = x 0 + (k-1)d ∧ G(x 0 ) ∧ G(x k-1 ) ∧ x ′ = x k-1 + d k (because D and G are convex) ⇒ ∃α ≥ 0, ∃x 0 ∈ X ⊓ G, ∃d, d ′ ∈ D, ∃x ′′ : x ′′ = x 0 + αd ∧ x ′ = x ′′ + d ′ ∧ G(x ′′ ) (dense approximation) ⇔ ∃x ′′ ∈ (X ⊓ G) ր D ⊓ G, ∃d ′ ∈ D : x ′ = x ′′ + d ′ ⇔ x ′ ∈ (X ⊓ G) ր D ⊓ G + D
We conclude by observing that (X⊓G)

ր D ⊓G +D = τ (X⊓G) ր D .2
Mind that the only approximation takes place in the line (⇒) where the integer coefficient k-1 ≥ 0 is replaced by a dense coefficient α ≥ 0. This is the technical explanation of Remark 3.4.

Remark 4.2 One might think that Theorem 3.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(x -d),
but there is a subtle difference: This formula computes the correct set for all states reachable within G, but for the last step crossing the border of G it allows only those vectors d having been used for the previous iterations, whereas actually there is a choice among all d ∈ D.

The following proposition reduces translations with inputs to generalized translations:

Proposition 4.3 A translation with inputs and a simple guard τ is equivalent to a polyhedral translation without inputs defined by

Ax ≤ b ∧ d ∈ D → x ′ = x + d D = {d | ∃y : d = Ty + u ∧ Jy ≤ k}
Note that D can be computed by standard polyhedra operations.

Proof.

x ′ ∈ τ (X) ⇔ ∃x, ∃y :

Ax ≤ b ∧ Jy ≤ k ∧ x ′ = x + Ty + u ⇔ ∃x, ∃y, ∃d : Jy ≤ k ∧ d = Ty + u ∧ Ax ≤ b ∧ x ′ = x + d ⇔ ∃x, ∃d ∈ D : Ax ≤ b ∧ x ′ = x + d with D = {d | ∃y : Jy ≤ k ∧ d = Ty + u} 2 Schrammel and Jeannet d 1 d 2 y 1 1 D Jy ≤ k x 1 x 2 1 1 X τ ⊗ (X) G
= {(x 1 , x 2 ) | 0 ≤ x 1 ≤ x 2 ≤ 1} and the transition τ : x 1 + x 2 ≤ 4 1 ≤ y ≤ 2 → x ′ 1 = x 1 + 2y -1 x ′ 2 = x 2 + y
. Eliminating the inputs as in Proposition 4.3 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}.
Remark 4.6 In analogy to Theorem 3.1, we could consider the formula X ⊔ ((((X ⊓ G) ր D) ⊓ (G + D)). In order to justify this, we extend the proof of Proposition 4.1 continuing at the label (dense approximation):

⇔ ∃α ≥ 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 ′ )) ⇒ x ′ ∈ (X ⊓ G) ր D ∧ x ′ ∈ (G + D) using {x | ∃d ∈ D ∧ G(x -d)} = {z + d | d ∈ D ∧ G(z)} = (G + D).
But it can be observed that for the translation of example 4.5 the latter formula results in an over-approximation (see Fig. 5) as compared to the result in Fig. 4. This reflects the additional approximation steps in the proof.

Translations/Resets with inputs and simple guards

These are defined by A 0 0 J

x y ≤ b k → x ′ = C T x y + u where C is a diagonal matrix with C i,i ∈ {0, 1}.
Notations. Let C ′ = I -C with I the identity matrix. Any vector x can be decomposed in x = x t + x r with x t = Cx and x r = C ′ x. We extend such notations to sets: X t = {x t | x ∈ X} and X r = {x r | x ∈ X}. If I denotes the set of dimensions, I t = {i ∈ I | C i,i = 1} and I r = I \I t are the set of translated and reset dimensions. Any set X can be approximated by the Minkowski sum X t + X r , which can also be seen as the Cartesian product of X projected on the subspace of translated dimensions and X projected on the subspace of reset dimensions.

This case can be handled in a way similar to Section 4.1: We combine Theorem 3.2 and Proposition 4.3 reducing translations/resets with inputs to generalized translations/resets without inputs. Mind, however, that remark 3.3 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.7 . Let τ be a translation with resets

G → x ′ = Cx + d with G(x) = (Ax ≤ b), d ∈ D and D a convex polyhedron. The set τ ⊗ (X) = X ⊔ τ (X) ⊔ τ (τ (X) ⊓ G) t ր D t + D r is a convex over-approximation of τ * (X).
Proof. The formula is trivially correct for 0 or 1 iterations, so, it remains to show that for the case of k ≥ 2 iterations our formula yields an overapproximation of k≥2 τ k (X).

x ′ ∈ k≥2 τ k (X) ⇔ ∃k ≥ 2, ∃x 0 ∈ X, ∃d 1 . . . d k ∈ D, ∃x 1 . . . x k :            x ′ = x k ∧ ∀k ′ ∈ [1, k] : x k ′ i = x 0 i + k ′ j=1 d j i for i ∈ I t x k ′ i = d k ′ i for i ∈ I r ∧ G(x) ∧ ∀k ′ ∈ [1, k-1] : G(x k ′ ) ⇔ ∃k ≥ 2, ∃x 0 ∈ X, ∃d 1 . . . d k ∈ D, ∃x 1 . . . x k : x ′ = x t + ( k j=1 d t j ) + d r k ∧ G(x) ∧ ∀k ′ ∈ [1, k-1] : G(x t + ( k ′ j=1 d t j ) + d r k ′ ) ⇒ ∃k ≥ 2, ∃x 0 ∈ X ⊓ G, ∃d 1 , d k ∈ D, ∃d t 2 . . . d t k-1 ∈ D t , ∃d r 2 . . . d r k-1 ∈ D r , ∃x 1 . . . x k :            x 1 = x t 0 + d 1 ∧ ∀k ′ ∈ [2, k -1] : x k ′ = x t 1 + ( k ′ j=2 d t j ) + d r k ′ ∧ x ′ = x t k-1 + d k ∧ ∀k ′ ∈ [1, k-1] : G(x k ′ ) (D approximated by the sum (D t + D r ) for k ′ ∈ [2, k -1]) x 1 x 2 1 1 X G x 1 x 2 1 1 X G Fig. 6
. Translation/reset with inputs: Example 4.9. Left hand side: τ (X) (dark shadowed) and ((τ (X) ⊓ G) t ր D t ) + D r (whole shadowed area). Right hand side: τ (((τ (X) ⊓ G) t ր D t ) + D r ) (dark shadowed) and τ ⊗ (X) (whole shadowed area).

⇔ ∃k ≥ 2, ∃x 0 ∈ X ⊓ G, ∃d 1 , d k ∈ D, ∃d t ∈ D t , ∃d r 2 . . . d r k-1 ∈ D r , ∃x 1 . . . x k :      x 1 = x t 0 + d 1 ∧ x k-1 = x t 1 + (k-2)d t + d r k-1 ∧ G(x 1 ) ∧ G(x k-1 ) ∧ x ′ = x t k-1 + d k (because D t and G are convex) ⇒ ∃α ≥ 0, ∃x 0 ∈ X ⊓ G, ∃d 1 , d ′ ∈ D, ∃d t ∈ D t , ∃d r ∈ D r , ∃x ′′ : x 1 = x t 0 + d 1 ∧ x ′′ = x t 1 + αd t + d r ∧ G(x 1 ) ∧ G(x ′′ ) ∧ x ′ = x ′′t + d ′ (dense over-approximation) ⇔ ∃α ≥ 0, ∃x 1 ∈ τ (X) ⊓ G, ∃d ′ ∈ D, ∃d t ∈ D t , ∃d r ∈ D r , ∃x ′′ : x ′′ = x t 1 + αd t + d r ∧ G(x ′′ ) ∧ x ′ = x ′′t + d ′ ⇔ ∃x ′′ ∈ (τ (X) ⊓ G) t ր D t + D r ⊓ G, ∃d ′ ∈ D, x ′ = x ′′t + d ′ ⇔ x ′ ∈ (τ (X) ⊓ G) t ր D t + D r ⊓ G t + D
The last expression is equal to τ (τ (X) ⊓ G) t ր D t + D r . 2

Theorem 4.8 The accelerated transition τ ⊗ for a translation/reset with inputs and a simple guard τ can be computed by applying Proposition 4.7 with D defined as in Proposition 4.3.

Example 4.9 Consider the polyhedron

X = {(x 1 , x 2 ) | 0 ≤ x 1 ∧ 1 ≤ x 2 ∧ x 1 + x 2 ≤ 2} and the transition τ : 2x 1 + 2x 2 ≤ 7 0 ≤ y ≤ 1 → x ′ 1 = x 1 + y + 1 x ′ 2 = y . Eliminating the inputs yields D = {(d 1 , d 2 ) | 1 ≤ d 1 ≤ 2 ∧ d 1 -d 2 = 1} and D t = {(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 ∧ 2x 1 -2x 2 ≤ 9 ∧ 2x 1 +11x 2 ≤ 22 ∧ x 1 ≥ 0}, see Fig. 6.
Schrammel and Jeannet

x 1 x 2 1 1 X G Fig. 7
. Example 4.10: Accelerated transition τ ⊗ (X) using the weakened guard G (result shadowed).

x 1

x 2 1 1 Fig. 8. Example 4.10: comparison between convex hull of the exact result (dark grey), our method (grey), and widening with no delay and 3 (!) descending iterations (light grey)

Weakening general guards to simple guards

As discussed at the beginning of Section 4, allowing constraints on both state and input variables in guards (L = 0 in Eqn. ( 2)) makes acceleration very difficult. Our solution is to weaken the guard G(x, y) = Ax + Ly ≤ b ∧ Jy ≤ k by the simple guard (or cartesian product) Ḡ = (∃y : G)

A ′ x≤b ′ ∧ (∃x : G) J ′ y≤k ′
and to apply Theorems 4.4 and 4.8. This trivially results in a sound over-approximation because a weaker guard is used for abstract acceleration.

Example 4.10 Consider the polyhedron

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

2x 1 + x 2 + y ≤ 6 x 2 -y ≤ 2 0 ≤ y ≤ 1 → x ′ 1 = x 1 + y + 1 x ′ 2 = x 2 + 1 .
The weakened guard is Ḡ = (2x

1 +x 2 ≤ 6 ∧ x 1 +x 2 ≤ 4 ∧ x 2 ≤ 3) ∧ (0 ≤ y ≤ 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. 7. 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. 8.

Comparison with widening

The standard widening operator for convex polyhedra and refinements of it like limited widening [START_REF] Halbwachs | Verification of real-time systems using linear relation analysis[END_REF] 4 may sometimes lead to good results. In this section, we compare the acceleration and the widening approaches on Examples 4.9 and 4.10. Analyzing such a program using widening after a number N of initial steps resorts to computing the limit of the sequences

X l 0 l τ ⊗ X ′ l τ
Y 0 = X Z 0 = Y N Y n+1 = X ⊔ τ (Y n ) for n < N Z n+1 = Z n ∇(Z n ⊔ τ (Z n ))
in which X n , Y n , Z n are associated with location l on Fig. 9. The technical properties of the widening operator ∇ guarantee that the sequence (Z n ) n≥0 converges in a finite number of steps to Z ∞ [START_REF] Cousot | Abstract interpretation and application to logic programs[END_REF], which is an over-approximation of the reachable valuations at location l. This result may be improved by computing the first elements of the sequence W 0 = Z ∞ , W n+1 = X ⊔ τ (W n ), which does not necessarily converge.

Translation/reset with inputs and simple guard If we compute the sequences defined above in the context of Example 4.9, we obtain with N = 0

Z ∞ = Z 1 = {(x 1 , x 2 ) | x 1 ≥ 0} W 1 = {x 1 ≥ 0 ∧ x 2 ≥ 1 ∧ x 1 +x 2 ≥ 1 ∧ x 2 ≤ 2} W ∞ = W 2 = τ ⊗ (X)
Delaying widening by one step (N = 1) improves the result for Z ∞ and makes the sequence (W n ) n≥0 converge in only one step:

Z ∞ = Z 1 = {x 1 ≥ 0 ∧ x 2 ≥ 1 ∧ x 1 +x 2 ≥ 1} W ∞ = W 1 = τ ⊗ (X)
In both cases Z ∞ is clearly much less precise than the result obtained by acceleration: neither x 1 nor x 2 get upper bound (to be compared with Fig. 6).

One or two descending iterations allow to get the same result as the one obtained by acceleration. However, it should be pointed out that if this loop is a program fragment, for instance embedded in an outer loop as in Fig. 10, it is not possible any more to apply a descending iteration in the middle of an ascending iteration (otherwise convergence is not guaranteed). Moreover, the acceleration technique is more efficient computationally (in particular it does not require convergence tests), and it has a monotonic behavior, which is not the case of widening.

Example 5.1 To illustrate these points, we consider the program depicted on Fig. 10 in which the inner loop τ is adapted from Example 4.9:

τ : 2x 1 + 2x 2 ≤ p 0 ≤ y ≤ 1 → x ′ 1 = x 1 +y+1 x ′ 2 = y p ′ = p , X = (x 1 , x 2 , p) 0 ≤ x 1 ∧ 1 ≤ x 2 x 1 +x 2 ≤ 2 ∧ p = 1
In both cases we apply widening on location l with a delay N = 1, and we perform one descending iteration after convergence of the ascending iteration. Without acceleration, we obtain a very weak invariant:

Z ∞ = {(x 1 , x 2 , p) | x 1 ≥ 0 ∧ p ≥ 1} W ∞ = W 1 = Z ∞
With acceleration we obtain much better results:

Z ′ ∞ = Z ∞ ∩ {(x 1 , x 2 , p) | x 1 +x 2 ≥ 1 ∧ x 1 -x 2 ≤ 4 ∧ x 1 +5x 2 ≤ 10} W ′ ∞ = W ′ 1 = Z ′ ∞ ∩ {(x 1 , x 2 , p) | p ≤ 20}
One can also consider widening with thresholds, that keeps in the result of the widening operation the subset of a fixed set of threshold constraints that are satisfied by both of its arguments. In the case of Example 4.9, a natural threshold constraint set is defined by the postcondition of the guard of τ by the body of τ , which is just τ

(⊤) = {(x 1 , x 2 ) | 0 ≤ x 2 ≤ 1}.
Using it with N = 0 one obtains the same Z ∞ as with standard widening applied with N = 1. On Example 5.1 and with the same threshold set extended with {p ≤ 21}, the results are improved but are still less precise than those obtained by combining acceleration and widening (in particular the descending iteration does not converge).

Translation with inputs and non-simple guard

In the context of Example 4.10, we obtain with N = 0:

Z ∞ = Z 1 = {(x 1 , x 2 ) | x 1 +x 2 ≥ 1} W 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} . . . W 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)
Again Z ∞ is very unprecise, but here the descending iteration does not converge (even if we use widening with thresholds), see Fig. 8 for W 3 . If we use N = 1, then Z ∞ is more precise, and

W ∞ = W 1 = τ ⊗ (X).
These results are just small experiments, but they illustrate the sensitiveness of widening (if we delay it, it might improve the result, but this is not guaranteed either because it is not monotonic) and the fact that if the loop is part of a more complex program, the result might be much less precise.

Conclusion

We have presented an extension of abstract acceleration to numerical inputs. 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. Our methods are ready for use in purely numerical automata by adopting the partitioning methods from [START_REF] Gonnord | Accélération abstraite pour l'amélioration de la précision en Analyse des Relations Linéaires[END_REF] for treating more complex cycles than the case of single self-loops that we have presented in this article. Moreover, limiting ourselves to convex guards and inputs that are contained in convex polyhedra is not a theoretical restriction of our methods, since nonconvex polyhedra can always be decomposed in convex ones.

Acceleration vs. Widening. From a theoretical point of view acceleration has -in contrast to widening -some advantageous properties that underpin its utility as an auxiliary technique for treating loops: First, a better precision can be obtained since it directly exploits information from the program. Second, the number of iterations in fixed point computation decreases, because accelerating transitions effectively removes loops in the control graph. Furthermore, widening is not a monotonous operator, whereas acceleration is, which makes approximations more regular and predictable. Practical experience has to be gained in order to estimate the degree of improvement attained by these properties. Nonetheless, we have to resort to widening for non-accelerable transitions in order to ensure convergence. Future work. As mentioned in the introduction, finding an appropriate control graph is the second issue (we have not dealt with in this article) in applying acceleration to logico-numerical programs, such as synchronous dataflow programs without explicit control flow. On the one hand the control graph should allow for a reasonably precise reachability analysis, on the other hand it should enable the use of abstract acceleration of numerical variables, while remaining sufficiently symbolic w.r.t. Boolean variables in order to prevent a combinatorial explosion. Our idea is to heuristically identify sets of states which behave like timed or linear hybrid automata, such that abstract acceleration can be applied.

Another direction is the extension to input variables of some results of [START_REF] Gonnord | Accélération abstraite pour l'amélioration de la précision en Analyse des Relations Linéaires[END_REF] on the combined acceleration of several self-loops around the same location.

Fig. 1 .

 1 Fig. 1. Simple loop transition (left) and accelerated transition (right).

4. 1

 1 Translations with inputs and simple guardsThese are defined by A 0

Fig. 4 .

 4 Fig. 4. Translation with inputs: Example 4.5: The left hand side shows the transformation of the inputs: Jy ≤ k ∧ d = Ty + u (bold line) is projected on variables d. The shadowed area in the right figure is the result of the accelerated transition τ ⊗ (X).

Fig. 5 . 6 . 4 . 4

 5644 Fig.5. Precision loss in example 4.5 when using the approximate formula according to remark 4.6.

Fig. 4

 4 left. After translation of X by D (Fig.4right) we obtain the polyhedron {

Fig. 9 .Fig. 10 .

 910 Fig. 9. Analysis with acceleration (left) and with widening (right) for Examples 4.9 and 4.10

Proof. In the proof, the guard G is seen alternatively as a predicate or a set.

Limited widening is also called widening with thresholds[START_REF] Cousot | Comparing the Galois connection and widening/narrowing approaches to abstract interpretation[END_REF].

 [START_REF] Abdulla | Using forward reachability analysis for verification of lossy channel systems[END_REF]This work was supported by the INRIA large-scale initiative Synchronics.