In [10, 11] we proposed a technique to approximate Hybrid Automata (HA) with Polynomial HA. The idea was to replace functions appearing in formulae with their Taylor Polynomials. Here we extend this technique to HA with formulae admitting integral functions. We prove that we get over-approximations of the original HA. We study the conditions ensuring that: 1. the “distance” between the formulae of the original HA and its approximation get close to 0 when increasing the degree of the Taylor polynomial (syntactical approximation), 2. the “distance” between the configurations reached in n steps by the two HA get close to 0 when increasing the degree of the Taylor polynomial (semantic approximation).
Hybrid automata [
As an example, the HA in Fig. 1 models a controller of a tank. The controller continuously senses the level of water and fills or empties it, aiming to keep the level between m and M litres (M > m). The water level, represented by variable x, varies with time depending on input/output flows. When the controller fills the tank (state in), the flow rate depends on time y, and is 1 cos(y2) litres/second. Thus, after a time t the water level is increased by R t 1 cos(y2) dy, as modeled by activity function in. When the controller emp0 ties the tank (state out), the flow rate at time y is y2. Thus, after a time t the water level is decreased by R0y y2 dt = 31 t3, as modeled by activity function out. x = M ' out out x;x0 2 [m;M] & %M^ x = x0 = x x = m ^ x0 = x $ -'in
in x;x0 2 [m;M] & out x0 = x R0t y2 dy %
In this example it is relevant to solve integrals by finding their
antiderivatives. Unfortunately, it is well known that the integration problem is ”difficult”,
and in many cases impossible. For instance the antiderivative is non elementary
for the filling flow function 1 cos(y2) we consider. Indeed the antiderivatives
cannot be expressed by an algebraic expression of rationals, exponentials,
logarithms, absolute values and trigonometric functions. A classical practical
example of non elementary antiderivative function is given by the Gauss integral
error Rab ex2 dx. Therefore this problem cannot be considered a problem with
restricted impact. Moreover in [
Our work is inspired by the necessity of using integrals in modeling real problems with HA, meanwhile dealing with the problem of managing and solving integrals, which is in general hard and even impossible for non elementary antiderivatives.
HA are usually used to prove safety properties (i.e. properties requiring that a
given set of bad configurations cannot be reached). The decidability of
reachability problem (i.e. whether or not a given configuration can be reached) becomes
determinant. Unfortunately, for most classes of HA, reachability is undecidable
[
The notion of approximation is then strengthened in [
In [
In this section we recall the formalism of Hybrid Automata (see, e.g., [
A vector of dimension n over a set U is a tuple ~u = (u1; : : : ; un) in U n. By ~ui we denote the ith element ui . We denote by ~u (u) the vector (u1; : : : ; un; u) 2 U n+1. Then, for ~u = (u1; : : : ; un) and ~v = (v1; : : : ; vm), we denote by ~u ~v the vector (u1 : : : ; un; v1; : : : ; vm) in U n+m. A space over U n is a set of vectors in U n.
We assume a finite set of real variables X ranged over by x; y; z; w; : : :. Each x 2 X can assume values in Dom(x) IR. An evaluation over X is a mapping v : X ! IR s.t. v(x) 2 Dom(x) for x 2 X. For an evaluation v, a variable y and a real c 2 Dom(x), the evaluation v[y := c] is defined by v[y := c](x) = v(x), for x , y, and v[y := c](y) = c. For vectors ~x = (x1; : : : ; xn) over Xn and ~u = (u1; : : : ; un) with ui 2 Dom(xi ), we write v[~x := ~u] for v[x1 := u1] : : : [xn := un]. Then, v(x1; : : : ; xm) denotes the vector (v(x1); : : : ; v(xm)) 2 IRm. We denote by ~X the vector (x1; : : : ; xjXj) over XjXj. Finally, we write [~X := ~u] to denote the evaluation v s.t. v(~X) = ~u.
We assume a set of function symbols F, together with an arity mapping r : F ! IN that assigns to each f 2 F its rank r(f ). If r(f ) = 0 then f is called a constant. We assume a unique interpretation I associating to each function symbol f 2 F a continuous function I (f ) : Dom(f ) ! IR s.t. Dom(f ) IRr(f ). Being I unique, sometimes with abuse of notation we use f for I (f ). In order to build polynomials with rational coefficients, we require that F contains the constant symbol q with I (q) = q for all q 2 Q, and symbols +, , denoting, resp., binary summation, binary multiplication and unary negation over reals.
– (F; X) contains all basic formulae of the form
Z u1 ln
! ! f g1(w1); : : : ; gr(f )(wr(f )) dwin : : : dwi1 ax, where: n 0 and, whenever n > 0, then l1; u1; : : : ; ln; un 2 X [ Q; w1; : : : ; wr(f ) 2 X n fl1; u1; : : : ; ln; ung and fi1; : : : ; ing f1; : : : ; r(f )g; g1; : : : ; gr(f ) 2 F are polynomial functions s.t. Dom(wi ) Dom(gi ); f 2 F with Dom(f ) g1(Dom(w1)) : : : gr(f )(Dom(wr(f )));
is a comparison operator in f<; ; =; ; >g; x 2 X and a 2 f0; 1g; [min(l; r); max(l; r)] Dom(wij ) for l 2 Dom(lj ); r 2 Dom(uj ); j = 1; : : : ; n. – : is in (X; F) whenever is in (X; F); – 1 _ 2 and 1 ^ 2 are in (X; F) whenever both 1 and 2 are in (X; F); – 8y: and 9y: are in (X; F) whenever y 2 X and is in (X; F).
In [
We write v j= to denote that the evaluation v satisfies the formula . Relation j= is defined inductively as follows: – v j= Rlu1 : : : Rlun f g1(w1); : : : ; gr(f )(wr(f )) dwin : : : dwi1 1 n ax iff Z v(u1) 0 0Z v(un)
BBB: : : BB
B v(l1) @B @B v(ln) 1 1 I (f ) I (g1)(e1); : : : ; I (gr(f ))(er(f )) dwin CCCC : : :CCC dwi1
A AC
I (a)v(x) where either ej = wj , if j 2 fi1; : : : ; ing, or ej = v(wj ), otherwise. – v j= : iff v 6j= (namely v j= does not hold). – v j= 1 ^ 2 (resp. v j= 1 _ 2) iff v j= 1 and v j= 2 (resp. v j= 1 or v j= 2). – v j= 8y: (resp. v j= 9y: ) iff v[y := c] j= for all (resp. for some) c 2 Dom(y).
For a formula 2 (F; X), let ~ denote the set fv : X ! IR j v j= g of the evaluations satisfying . Two formulae 1; 2 are equivalent iff ~ 1 = ~ 2.
the form Q1y1: : : : Qmym: , where: (i) Qi 2 f8; 9g for i = 1; : : : ; m; (ii) contains neither quantifiers nor negations; (iii) contains only relations in f<; g; (iv) all basic formulae in are of the following form, for n r(f ) and z1; : : : ; zn 2 X: Z z1 0 : : :
Z zn 0
! ! f g1(w1); : : : ; gr(f )(wr(f )) dwn : : : dw1 ax.
lent to that can be constructed from .
E.g. R4z ey dy w is equivalent to the normal form 9x: R0x ey+4dy w^z 4 = x.
Definition 3. An Hybrid Automaton (HA for short) H over X and F is a tuple of the form H = h init; Q; q0; T ; Acti, where: – init 2 (F; X) is the initial condition. – Q is a finite set of states, and q0 2 Q is the initial state. – T Q (F; fx1; : : : ; xjXj; x10; : : : ; xj0Xjg) Q is a finite set of transitions. Variables x10; : : : ; x0X represent the values taken by x1; : : : ; xjXj after the firing of a transition.
j j – Act : Q ! (F; fx1; : : : ; xjXj; t; x10; : : : ; xj0Xjg) is the activity function assigning to each state q a formula Act(q). Variable t represents time elapsing. 1 Then, H is a Polynomial Hybrid Automaton (PHA for short) iff init, Act(q) for all states q and for each transition (q; ; q0) are all polynomial formulae. Example 1. The tank controller represented in Fig. 1 has two states: in state in the controller fills the tank, in state out the controller empties the tank. The jump condition x = m ^ x0 = x (resp. x = M ^ x0 = x) ensures that the jump from out to in (resp. from in to out) happens when the level of the water is m (resp. M), and the firing of the transition does not cause any change in the water level.
In state in, the water flow rate at time y is 1 cos(y2). Hence, staying in in for
t units of time causes a water level growing of R0t 1 cos(y2) dy. This is modelled
by the activity function in, which can be written in normal form in several
ways. Let 0 be the formula x M ^ x m ^ x0 M ^ x0 m, or x; x0 2 [m; M] for
short. Given the functions f ; g s.t. f (y) = 1 cos(y2) and g(y) = cos(y2), we can
write in in the two following ways, which are semantically equivalent:
1
in
0 ^ x0 x = z ^
f (y) dy = z
2
in
1 Note that invariants can be expressed by means of universal quantifiers (see [
In state out, the water flow rate at time y is y2. Hence, staying in state out for t units of time causes a water level decrement of R0t y2 dy. This is modelled by the activity function out 0 ^ x x0 = z ^ R0t y2 dy = z. Obviously R0t y2 dy = t33 . Therefore in this case no approximation is necessary.
A configuration of an HA H is a pair (q;~u), with q 2 Q and ~u = (u1; : : : ; ujXj) a vector in IRjXj representing that each variable xi has value ui . H can evolve from (q;~u) to (q0;~u0), written (q;~u) ! (q0;~u0), by an activity or transition step. An activity step describes the evolution from (q;~u) due to remaining in q and passing of time. In time units, Act(q) takes H to a new evaluation of the variables: if
0 and [~X := ~u; t := ;~X0 := ~u0] j= Act(q), then (q;~u) ! (q;~u0).
A transition step describes the evolution from (q;~u) due to a transition from q: if (q; ; q0) 2 T and [~X := ~u;~X0 := ~u0] j= , then (q;~u) ! (q0;~u0): A run is a sequence of (activity and transition) steps (q0; u~0) ! : : : ! (qi ; u~i ) : : : with q0 the initial state and [~X := u~0] 2 ~ init. A configuration (q;~u) is reachable in n steps iff there is a run (q0; u~0) ! : : : ! (qn; u~n) : : : s.t. qn = q and u~n = ~u. A configuration is reachable iff it is reachable in n steps for some n 0.
A region R of a HA H is a set of configurations. The region reachable by H from a region R is denoted Post(R; H). Formally: Post(R; H) = f(q0;~u0) j 9(q;~u) 2 R such that (q;~u) ! (q0;~u0)g. Let Postn(H) denote either the region f(q0; u~0) j [~X := u~0] 2 ~ initg, if n = 0, or the region Post(Postn 1(H); H), if n > 0. Moreover, let Post(H) denote the region Sn2IN Postn(H). The following result is folklore. Theorem 1. For each n 2 IN, a configuration (q;~u) is reachable in n steps iff (q;~u) 2 Postn(H). Hence (q;~u) is reachable iff (q;~u) 2 Post(H).
The following result follows from Tarski’s results [
Theorem 2. If H is polynomial and n 2 IN then (q;~u) 2 Postn(H) is decidable.
The ith derivative of f 2 F wrt. coordinate jth is denoted Dij f . Let Ck denote the set of the functions that are derivable k times, namely f 2 Ck iff Dj11 : : : Djrr((ff)) f exists whenever j1 + : : : + jr(f ) = k.
Definition 4. Assume a function f 2 Ck and a vector ~v 2 Dom(f ). The polynomial of Taylor of degree k for f wrt. ~v is defined by
Pk(f ; w~;~v) =
X j1+:::+jr(f ) k
jr(f ) f )(~v) (w1 v1)j1 : : : (wr(f ) vr(f ))jr(f ) (Dj11 : : : Dr(f ) j1! : : : jr(f )! where w~ is the vector of variables (w1; : : : ; wr(f )). For ~u 2 Dom(f ), the value rk(f ;~u;~v) defined by rk(f ;~u;~v) = f (~u) Pk(f ;~u;~v) is called the remainder.
The intuition is that Pk(f ; w~;~v) is a polynomial that approximates f (w~), and the error of the approximation in ~u 2 Dom(f ) is given by rk(f ;~u;~v). This error is quantified by the following result, known as Lagrange Remainder Theorem. Theorem 3 (Lagrange). For a function f 2 Ck+1, a convex set S Dom(f ) and two vectors ~u;~v in S, there exists a vector~z on the segment linking ~u and ~v s.t.: rk(f ;~u;~v) =
X j1+:::+jr(f )=k+1
jr(f ) f )(~z) (u1 v1)j1 : : : (ur(f ) vr(f ))jr(f ) (Dj11 : : : Dr(f ) .
Our aim is to give an upper bound to jrk(f ;~u;~v)j, under suitable hypothesis. Definition 5. A function f 2 Ck+1 is analytic in S Dom(f ) if there are two constants C, L s.t., for all j1; : : : ; jr(f ) with j1 + + jr(f ) k + 1 and~z 2 S, we have jr(f ) f )(~z)j L Cj1+:::+jr(f ) : j(Dj11 : : : Dn
Example 2. Trigonometric functions are analytic. For instance, for the function sin(x) it is sufficient to take the constants L = C = 1. Exponential and logarithmic functions are analytic in finite intervals. For instance, for function e2x and interval [0; 10], it is sufficient to take the constants C = 2 and L = e20.
Let us assume an analytic function f 2 Ck+1. Then, for Cˆ and Lˆ the minimal values satisfying the condition of Def. 5, for any k we denote with C(f ; k) the value Lˆ Cˆ k+1. Moreover, let Rk(f ; w~;~v) denote the polynomial over w~ defined by Rk(f ; w~;~v) =
C(f ; k) (r(f ))k+1 Qjr(=f1)((wj vj )2 l k+21 m + 1)
j kr(+f1) k!
By definition, Rk(f ;~u;~v) is an upper bound to jrk(f ;~u;~v)j for all ~u 2 Dom(f ).
Moreover, Rk(f ;~u;~v) gets close to 0 when k tends to the infinity. Formally:
Proposition 2 ([
From jrk(f ;~u;~v)j Rk(f ;~u;~v), f (~u) = rk(f ;~u;~v) + Pk(f ;~u;~v) and monotonicity of the integral we get the following result.
Proposition 3. Let f 2 F be analytic and ~v 2 Dom(f ). Then for all vectors ~e = (g1(w1); : : : ; gn(wn)) (gn+1(cn+1); : : : ; gr(f )(cr(f ))) with cn+1; : : : ; cr(f ) 2 IR, and r1; : : : ; rn 2 IR s.t. g([0; r1]) g([0; rn]) fgn+1(cn+1)g fgr(f )(cr(f ))g Dom(f ), we have Z r1 0
! ! f (~e) dwn : : : dw1
Z r1 : : :
Z rn
! ! Pk(f ;~e;~v) Rk(f ;~e;~v) dwn : : : dw1.
If we replace f (g1(w1); : : : ; gr(f )(wr(f ))) with Pk(f ; (g1(w1); : : : ; gr(f )(wr(f ));~v) Rk(f ; (g1(w1); : : : ; gr(f )(wr(f ));~v) in a basic formula, by Prop. 3 we get a less demanding formula, provided the operator is in f<; g, like in normal forms. 4
Approximations of HA are obtained by weakening formulae [
from H by replacing each formula in H with a formula 0 s.t. ~ ~ 0.
We aim to give a notion of approximation for HA respecting Def. 6. We start with a notion of approximation for normal forms inspired by Prop. 3.
appears in is derivable k +1 times and is analytic, then the approximation of of degree k is the set of formulae denoted A( ; k) defined inductively wrt. as follows: 1. If R0z1 : : : R0zn f (g1(w1); : : : ; gr(f )(wr(f ))) dwn : : : dw1 ax, then either A( ; k) is the singleton f g, if f is a polynomial, or A( ; k) contains all the formulae k;~v
Z z1 0 : : :
Z zn 0
! ! Pk(f ; g(w~);~v) Rk(f ; g(w~);~v) dwn : : : dw1 ax with g(w~) = (g1(w1); : : : ; gr(f )(wr(f ))) and ~v 2 Dom(f ); 2. If 1 ^ 2 then A( ; k) = f k1 ^ k2 j k1 2 A( 1; k) and 3. If 1 _ 2 then A( ; k) = f k1 _ k2 j k1 2 A( 1; k) and 4. If 9y: 0 then A( ; k) = f9y: k0 j k0 2 A( 0; k)g; 5. If 8y: 0 then A( ; k) = f8y: k0 j k0 2 A( 0; k)g. 2 k 2 A( 2; k)g; 2 k 2 A( 2; k)g;
Let us prove that all formulae in A( ; k) are less demanding than .
for all 0 2 A( ; k).
and k 2 IN s.t. A( ; k) is defined, then ~ ~ 0 Proof (sketch). By structural induction over . The proof of the base case follows from Prop. 3, the inductive steps are standard.
From the approximation of normal forms we get an approximation of HA.
An immediate corollary of Thm. 4 states that Def. 8 respects Def. 6.
of H according to Def. 6.
Example 3. Let us consider the tank controller H of Ex. 1 where in i2n. The set A(H; 4) contains the automaton obtained from H by approximating function g in in by choosing the real 0 as vector ~v. ( out does not change since all functions are polynomial). Since Dwk( cos(w)) = Dwk cos(w) = cos(w + k 2 ), it h(yo32!l)d3s tchoast(4P 42(c)os(;y4y2!)24; 0=) 1 +cyo24s(0)2y48 .cMoso(r2e)ov(eyr2,)R14(ccooss;(y22; 02))= (Cy22(!c)2os; 4co)s((3y12)2602+1) . Now, C(cos; 4) = maxfj cos(w + 4 2 )j : w 2 Dom(g)g = 1, therefore we have that 2 in 4;0
Hk 2 A(H; k) it holds that Postn(H) Postn(Hk).
Proof (sketch). By Thm. 4 and the monotonicity of Post.
Thm. 5 gives us a sound method for showing that H cannot reach some bad configuration (q;~u) in n steps. In fact, by Thm. 2 it is computable if (q;~u) can be reached in n steps by a PHA Hk in A(H; k). By Thm. 5 if (q;~u) cannot be reached in n steps by Hk then it cannot be reached in n steps by H as well. 5
In order to limit the error introduced by the approximation, Def. 6 is
strengthened in [
Given two vectors ~u = (u1; : : : ; un) and ~v = (v1; : : : ; vn) in IRn, let d(~u;~v) denote their distance d(~u;~v) = p(u1 v1)2 + : : : + (un vn)2.
Given a vector ~v and a real > 0, let N(~v; ) denote the space of vectors f~u j d(~v;~u) g. Then, for a space S IRn and a real 0, the neighborhood of ray of space S is the set of spaces N(S; ) = fS0 S j 8~v0 2 S0 9~v 2 S s.t. d(~v;~v0) g.
(F; X) iff fv(~X) j v 2 ~ 0g 2 N(fv(~X) j v 2 ~ g; ). 2
tained from H by replacing each formula in H with a formula 0 s.t. 0 is an -approximation of .
Our aim is to study the conditions over formulae in H ensuring that, for
any > 0, there exists some k0 2 IN s.t. for all k > k0 we have that the set A(H ; k)
contains only -approximations for H . In [
we have that Dom(x) = [lx; rx], for suitable rationals lx; rx 2 Q, and for each function f in we have that Dom(f ) = [l1; r1] : : : [lr(f ); rr(f )], for suitable rationals l1; r1; : : : ; lr(f ); rr(f ) 2 Q. 5.1
Syntactical Analysis of the Error First of all let we give the intuition why for bounded normal formulae with comparison operator we have that and for all > 0 there exists some k0 s.t. for all k > k0, A( ; k) contains only -approximations of .
Consider a normal form R0d f (x; y)dx 0. All formulae in A( ; k) are of the form R0d P(f ; (x; y); (cx; cy )) Rk(f ; (x; y); (cx; cy )) dx 0 for a vector (cx; cy ) 2 Dom(f ). Since is bounded, we can split Dom(R0d f (x; y)dx) (which is a function over variable y) in m closed intervals S1; : : : ; Sm of size strictly < . Let i1; : : : ; il 2 f1; : : : ; mg be the indexes s.t. no evaluation in ~ maps y to Si1 [ : : : [ Sil , namely there is no u 2 Si1 [ : : : [ Sil satisfying R0d f (x; u)dx 0. It is enough to show that no evaluation vk in any ~ k with k 2 A( ; k) maps y to Si1 [ : : : [ Sil . In fact, if vk(y) 2 Sj with j < fi1; : : : ; ing, by the definition of j1; : : : ; jl there is some v 2 ~ with v(y) 2 Sj and, since the size of Sj is bounded by , we infer vk(y) v(y) < .
Hence the target is to show that there exists some k0 s.t. for all k > k0 we have that for all u 2 Si1 [ : : : [ Sil the following inequality holds:
P(f ; (x; u); (cx; cy )) Rk(f ; (x; u); (cx; cy )) dx > 0. (1) Since Si1 [ : : : [ Sil is a closed set, R0d f (x; u)dx is a continuous function (which follows by the continuity of f ), and the comparison symbol guarantees that R0d f (x; u)dx is strictly positive in Si1 [: : :[Sil , we can define # = minfR0d f (x; u)dx j u 2 Si1 [ : : : [ Sil g. Since [0; d] Si1 [ : : : [ Sil is a closed set, we can define ek = maxfRk(f ; (u0; u); (cx; cy ))) j u0 2 [0; d] ^ u 2 Si1 [ : : : [ Sil g. By Prop. 2.2 we can find a k0 s.t. for all k > k0, ek < #=(2 d). Assume k > k0. We show Eq. 1 by = = >
0 Z d
0 Z d
0 Z d
0 Z d 0 (P(f ; (x; u); (cx; cy )) Rk(f ; (x; u); (cx; cy )))dx (P(f ; (x; u); (cx; cy )) ekdx (P(f ; (x; u); (cx; cy )) + rk(f ; (x; u); (cx; cy )) rk(f ; (x; u); (cx; cy )) ekdx f (x; u) rk(f ; (x; u); (cx; cy )) ekdx
f (x; u) ek ekdx f (x; u) f (x; u)dx # f (x; u)dx
f (x; u)dx = 0 with the first inequality by the definition of ek and the monotonicy of the integral, the second by jrk(f ; (x; u); (cx; cy ))j Rk(f ; (x; u); (cx; cy )) and the definition of ek, the third by ek < 2#d , and the last inequality by the definition of #.
Z z1 0 : : :
Z zn 0
! ! f (g1(w1); : : : ; gr(f )(wr(f ))) dwn : : : dw1 ax in is such that is , then, for each > 0, there exists some k0 s.t. for each k > k0, the set A( ; k) contains only -approximations for .
The result above can be immediately extended to automata.
contains only -approximations for H. 5.2 Semantical Analysis of the Error Our aim is to measure how close the behaviors of the PHA in A(H; k) and the behavior of H are.
Definition 12. Let 0. The neighborhood of ray of a region R is the set of regions N(R; ) = fR0 R j 8(q0;~u0) 2 R0: 9 (q;~u) 2 R: q = q0 and d(~u;~u0) g.
Under the hypothesis of Thm. 6, for all n 2 IN, if k tends to the infinity, then the behavior of length at most n of each PHA Hk 2 A(H; k) gets close to the behavior of H, in the sense that Postn(Hk) is in a neighborhood of Postn(H) of ray arbitrarily small. This comes from the fact that Postn(Hk) can be expressed by means of a formula by using existential quantifications.
Postn(Hk) 2 N(Postn(H); ) for all Hk 2 A(H; k). In this paper we have defined syntactical over–approximations for Hybrid Automata enriched with integrals. The approximation is based on Taylor polynomials. We have also studied their syntactical and semantical convergence w.r.t. the original specifications.
As future work we will also study under–approximations based on the same
technique. The idea is to define the under–approximation of degree k of a
formula by using the polynomial which approximates the reminder to
increasing the Taylor polynomial. Moreover we can extend our work with function
variables by following the theory developed in [