=Paper=
{{Paper
|id=Vol-1698/CS&P2016_13_Lanotte&Tini_Extending-Taylor-Approximation-to-Hybrid-Systems-with-Integrals
|storemode=property
|title=Extending Taylor Approximation to Hybrid Systems with Integrals
|pdfUrl=https://ceur-ws.org/Vol-1698/CS&P2016_13_Lanotte&Tini_Extending-Taylor-Approximation-to-Hybrid-Systems-with-Integrals.pdf
|volume=Vol-1698
|authors=Ruggero Lanotte,Simone Tini
|dblpUrl=https://dblp.org/rec/conf/csp/LanotteT16
}}
==Extending Taylor Approximation to Hybrid Systems with Integrals==
https://ceur-ws.org/Vol-1698/CS&P2016_13_Lanotte&Tini_Extending-Taylor-Approximation-to-Hybrid-Systems-with-Integrals.pdf
Extending Taylor Approximation to Hybrid
Automata with Integrals
Ruggero Lanotte1 and Simone Tini1
University of Insubria (IT)
Abstract. 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 condi-
tions 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).
1 Introduction
Hybrid automata [1, 2] (HA, for short) are a widely studied model for hybrid
systems [13], i.e. systems with discrete and continuous state changes. HA ex-
tend classic finite state machines with continuously evolving variables, and ex-
hibit two kinds of state changes: discrete jump transitions, occurring instanta-
neously, and continuous flow transitions, occurring while time elapses. The two
kinds of transitions are guarded by jump conditions and activity functions, resp.,
which are formulae expressing constraints on the source and target value of the
variables. Extensions to HA are considered to deal with particular scopes. As an
example in [12, 8] HA are extended with data structures to face with safety and
security problems. But most of hybrid system applications is modelling and
verifying systems where digital computational processes interact with analog
physical ones. In this setting, integrals have several applications. In physics and
engineering, where hybrid systems are widely used, we mention: work and im-
pulse, electromagnetism, first moment and center of mass, application in fluid
mechanics.
As an example, the HA in Fig. 1 models a controller of a tank. The con-
troller 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, repre-
sented 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(y 2 ) litres/second. Thus, after a time t the water level is increased by
Rt
0
1−cos(y 2 ) dy, as modeled by activity function φin . When the controller emp-
ties the tank (state out), the 2
R yflow rate at time y is y . Thus, after a time t the
2 1 3
water level is decreased by 0 y dt = 3 t , as modeled by activity function φout .
x = m ∧ x0 = x
' $ ' $ R
out in t
- φin ≡ x0 = x + 0 1 − cos(y 2 ) dy
φout φin
x=M- Rt
x, x0 ∈ [m, M] x, x0 ∈ [m, M] φout ≡ x0 = x − 0 y 2 dy
& % & %
x = M ∧ x0 = x
Fig. 1. The tank controller
In this example it is relevant to solve integrals by finding their antideriva-
tives. 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(y 2 ) we consider. Indeed the antiderivatives
cannot be expressed by an algebraic expression of rationals, exponentials, log-
arithms, absolute values and trigonometric functions. A classical practical ex-
ample of non elementary antiderivative function is given by the Gauss integral
Rb 2
error a ex dx. Therefore this problem cannot be considered a problem with re-
stricted impact. Moreover in [14] it is showed that the integration problem is
undecidable for functions with a non elementary antiderivative.
Our work is inspired by the necessity of using integrals in modeling real
problems with HA, meanwhile dealing with the problem of managing and solv-
ing 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 reachabil-
ity problem (i.e. whether or not a given configuration can be reached) becomes
determinant. Unfortunately, for most classes of HA, reachability is undecidable
[7] and the introduction of integrals complicates this analysis. However, for
some classes of HA, computing the successors (or predecessors) of configura-
tions sets is reasonably efficient, and, therefore, reachability in a limited number
of steps is decidable. For instance for Polynomial HA computing the successors
of configuration sets is decidable [15]. A methodology proposed in [6] fills this
gap: the idea is to over-approximate an HA H with another HA H 0 s.t. com-
puting the successors of configuration sets for H 0 is decidable and the compu-
tations of H 0 are a superset of the set of all the possible computations of H.
Hence, if we prove that a bad configuration cannot be reached by H 0 then we
can infer that it cannot be reached by the original H. In [6] it is required that
the approximation H 0 is in the class of the Linear HA, for which the successors
of configuration sets are computable.
The notion of approximation is then strengthened in [6] by -approximation,
which is motivated by the need to limit the error introduced by the approxima-
tion. In [6] an asymptotically complete approximation operator, called ratio-
nally rectangular phase-portrait approximation, is given which approximates any
jump condition or activity function by a predicate satisfied by all points lying
in a space consisting of a products of intervals with rational endpoints.
In [10, 11] over-approximations are based on replacing functions over vari-
ables with their Taylor polynomial. Since Taylor polynomials allow us to ap-
proximate functions and integrals, in the present paper we extend our tech-
nique in [10, 11] to over-approximate HA with integrals. In detail, given any
HA H and k ∈ IN, A(H, k) is the set of the Polynomial HA (for which succes-
sors of configuration sets is decidable) that are obtainedR u by replacing in jump
−
conditions and activity functions of H each integral l f (~x)dx with a polyno-
mial based on Taylor polynomial theory. The resulting polynomial HA over-
approximates the original one according to [6]. We study the conditions en-
suring that our approximation is asymptotically complete, in the sense that,
for each > 0 there exists some k0 s.t., for all k > k0 , A(H, k) contains only -
approximations for H. This analysis of the error is syntactic, meaning that it
does not consider the behaviour of H and its approximation. We consider also
semantic analysis of the error and study conditions ensuring that, when k tends
to the infinity, the behaviour of any Hk ∈ A(H, k) gets close to the behaviour of
H.
2 Hybrid Automata
In this section we recall the formalism of Hybrid Automata (see, e.g., [13]).
− −
A vector of dimension n over a set U is a tuple ~u = (u1 , . . . , un ) in U n . By ~u i we
−
denote the i th element ui . We denote by ~u ⊕ (u) the vector (u1 , . . . , un , u) ∈ 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 ∈ X can assume values in Dom(x) ⊆ IR. An evaluation over X is a mapping
v : X → IR s.t. v(x) ∈ Dom(x) for x ∈ X. For an evaluation v, a variable y and a real
c ∈ 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 ∈ Dom(xi ), we write v[~x := ~u ] for v[x1 := u1 ] . . . [xn :=−un ]. Then, v(x1 , . . . , xm )
denotes the vector (v(x1 ), . . . , v(xm )) ∈ IRm . We denote by ~X the vector (x1 , . . . , x|X| )
− − − −
over X|X| . 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 ∈ 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 ∈ 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 polyno-
mials with rational coefficients, we require that F contains the constant symbol
q with I(q) = q for all q ∈ Q, and symbols +, ·, − denoting, resp., binary summa-
tion, binary multiplication and unary negation over reals.
Definition 1. The set Φ(F, X) of the formulae over F and X is the least set s.t.:
– Φ(F, X) contains all basic formulae of the form
Z u1 Z un
! !
... f g1 (w1 ), . . . , gr(f ) (wr(f ) ) dwin . . . dwi1 ∼ ax, where:
l1 ln
• n ≥ 0 and, whenever n > 0, then l1 , u1 , . . . , ln , un ∈ X ∪ Q;
• w1 , . . . , wr(f ) ∈ X \ {l1 , u1 , . . . , ln , un } and {i1 , . . . , in } ⊆ {1, . . . , r(f )};
• g1 , . . . , gr(f ) ∈ F are polynomial functions s.t. Dom(wi ) ⊆ Dom(gi );
• f ∈ F with Dom(f ) ⊆ g1 (Dom(w1 )) × . . . × gr(f ) (Dom(wr(f ) ));
• ∼ is a comparison operator in {<, ≤, =, ≥, >};
• x ∈ X and a ∈ {0, 1};
• [min(l, r), max(l, r)] ⊆ Dom(wij ) for l ∈ Dom(lj ), r ∈ 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);
– ∀y. φ and ∃y. φ are in Φ(X, F) whenever y ∈ X and φ is in Φ(X, F).
The subset of polynomial formuale is obtained by restricting to (i) those f ∈ F that
are polynomial functions s.t. Dom(f ) is a product of intervals with bounds in Q ∪
{±∞}, (ii) those variables x ∈ X s.t. Dom(x) is an interval with bounds in Q ∪ {±∞}.
In [11] we restricted to basic formulae of Def. 1 with n = 0, i.e. general
continuous function without integrals. The definition of basic formulae could
appear restrictive at first glance. We argue that Def. 1 gives us expressiveness
and flexibility by some examples:
1. By existential quantification, arbitrary expressions be compared. For in-
stance, ex+sin y ≤ x/(y 2 + 1) is expressed by ∃z. (ex+sin y ≤ z ∧ x/(y 2 + 1) = z).
2. By existential quantification, we give to the user as much freedom as possi-
ble in choosing the functions to be approximated. For instance, for f , g ∈ F,
− −
we can rewrite a formula h(~x) ∼ ax with h = f ◦ g by ∃y. g(~x) = y ∧ f (y) ∼ ax.
In the first case the function f ◦ g is approximated, in the second case f and
g are approximated separately, e.g. in order to approximate the exponential
and the sin separately, the formula ∃z. (ex+sin y ≤ z ∧ x/(y 2 + 1) = z) in item 1
can be rewritten as ∃z1 .∃z2 . (ez1 ≤ z2 ∧ x + sin y = z1 ∧ x/(y 2 + 1) = z2 ).
3. Also arbitrary expressions dealing R y with integrals
Ry can be compared. For
instance, the expression h(x) + x f (z)dz = x g(z)dz can be expressed by
Ry Ry
∃w1 ∃w2 . x f (z)dz = w1 ∧ x g(z)dz = w2 ∧ h(x) + w1 = w2 .
4. Expressions
R y with integrals can be arguments of functions.R For instance,
y
cos x f (z)dz > 0 can be expressed by ∃w. cos(w) > 0 ∧ x f (z)dz = w,
R5 R3 R3 R5
and 0 f x, 0 g(y)dy dx ≤ 7 by ∃z. 0 g(y)dy = z ∧ 0 f (x, z)dx ≤ 7.
5. We can deal also with general bounds for integrals. For instance the formula
R ex Rz
4
f (y)dy ≤ x can be expressed by ∃z. 4
f (y)dy ≤ x ∧ ex = z.
We write v |= φ to denote that the evaluation v satisfies the formula φ. Relation
|= is defined inductively as follows:
R u R u
– v |= l 1 . . . l n f g1 (w1 ), . . . , gr(f ) (wr(f ) ) dwin . . . dwi1 ∼ ax iff
1 n
Z v(u1 ) Z v(un )
. . .
I(f ) I(g1 )(e1 ), . . . , I(gr(f ) )(er(f ) ) dwin . . . dwi1 ∼ I(a)v(x)
v(l1 ) v(ln )
where either ej = wj , if j ∈ {i1 , . . . , in }, or ej = v(wj ), otherwise.
– v |= ¬φ iff v 6|= φ (namely v |= φ does not hold).
– v |= φ1 ∧φ2 (resp. v |= φ1 ∨φ2 ) iff v |= φ1 and v |= φ2 (resp. v |= φ1 or v |= φ2 ).
– v |= ∀y. φ (resp. v |= ∃y. φ) iff v[y := c] |= φ for all (resp. for some) c ∈ Dom(y).
For a formula φ ∈ Φ(F, X), let ~φ denote the set {v : X → IR | v |= φ} of the
evaluations satisfying φ. Two formulae φ1 , φ2 are equivalent iff ~φ1 = ~φ2 .
Definition 2. The subset of the normal forms in Φ(F, X) contains the formulae of
the form Q1 y1 . . . . Qm ym . φ, where: (i) Qi ∈ {∀, ∃} for i = 1, . . . , m; (ii) φ contains
neither quantifiers nor negations; (iii) φ contains only relations in {<, ≤}; (iv) all
basic formulae in φ are of the following form, for n ≤ r(f ) and z1 , . . . , zn ∈ X:
Z z1 Z zn
! !
... f g1 (w1 ), . . . , gr(f ) (wr(f ) ) dwn . . . dw1 ∼ ax.
0 0
Proposition 1. Given any formula φ ∈ Φ(X, F), there exists a normal form equiva-
lent to φ that can be constructed from φ.
Rz Rx
E.g. 4 ey dy ≤ w is equivalent to the normal form ∃x. 0 ey+4 dy ≤ 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 ∈ Φ(F, X) is the initial condition.
– Q is a finite set of states, and q0 ∈ Q is the initial state.
– T ⊆ Q × Φ(F, {x1 , . . . , x|X| , x10 , . . . , x|X|
0
}) × Q is a finite set of transitions. Variables
0 0
x1 , . . . , x|X| represent the values taken by x1 , . . . , x|X| after the firing of a transition.
– Act : Q → Φ(F, {x1 , . . . , x|X| , t, x10 , . . . , x|X|
0
}) 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(y 2 ). Hence, staying in in for
Rt
t units of time causes a water level growing of 0 1−cos(y 2 ) 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 ∈ [m, M] for
short. Given the functions f , g s.t. f (y) = 1 − cos(y 2 ) and g(y) = − cos(y 2 ), we can
write φin in the two following ways, which are semantically equivalent:
Zt Zt
1 0 0 2 0 0
φin ≡ φ ∧ x − x = z ∧ f (y) dy = z φin ≡ φ ∧ x − x − t = z ∧ g(y) dy = z
0 0
1 Note that invariants can be expressed by means of universal quantifiers (see [11]).
However, when non-polynomial functions are approximated by their Taylor
polynomials, in the former case we approximate f and in the latter g.
In state out, the water flow rate at time y is y 2 . Hence, staying in state out for
Rt
t units of time causes a water level decrement of 0 y 2 dy. This is modelled by
Rt Rt 3
the activity function φout ≡ φ0 ∧ x − x0 = z ∧ 0 y 2 dy = z. Obviously 0 y 2 dy = t3 .
Therefore in this case no approximation is necessary.
− −
A configuration of an HA H is a pair (q, ~u ), with q ∈ Q and ~u = (u1 , . . . , u|X| ) a
vector in IR|X| representing that each variable xi has value ui . H can evolve from
− − − −
(q, ~u ) to (q0 , ~u 0 ), written (q, ~u ) → (q0 , ~u 0 ), by an activity or transition step. An ac-
−
tivity 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 := ~u 0 ] |= Act(q), then (q, ~u ) → (q, ~u 0 ).
−
A transition step describes the evolution from (q, ~u ) due to a transition from q:
− − − − − −
if (q, φ, q0 ) ∈ T and [~X := ~u , ~X0 := ~u 0 ] |= φ, then (q, ~u ) → (q0 , ~u 0 ).
−− −−
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 ] ∈ ~φ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) = {(q0 , ~u 0 ) | ∃(q, ~u ) ∈
− − − −
R− such that (q, ~u ) → (q0 , ~u 0 )}. Let Postn (H) denote either the region {(q0 , u~0 ) |
−−
[~X := u~0 ] ∈ ~φinit }, if n = 0, or the
S region Post(Post
n−1
(H), H), if n > 0. Moreover,
n
let Post(H) denote the region n∈IN Post (H). The following result is folklore.
− −
Theorem 1. For each n ∈ IN, a configuration (q, ~u ) is reachable in n steps iff (q, ~u ) ∈
− −
Postn (H). Hence (q, ~u ) is reachable iff (q, ~u ) ∈ Post(H).
The following result follows from Tarski’s results [15] and from the fact that
the antiderivative of a polynomial is a polynomial.
−
Theorem 2. If H is polynomial and n ∈ IN then (q, ~u ) ∈ Postn (H) is decidable.
3 Taylor Approximation
The i th derivative of f ∈ F wrt. coordinate j th is denoted Dij f . Let Ck denote the
j jr(f )
set of the functions that are derivable k times, namely f ∈ Ck iff D11 . . . Dr(f ) f
exists whenever j1 + . . . + jr(f ) = k.
−
Definition 4. Assume a function f ∈ Ck and a vector ~v ∈ Dom(f ). The polynomial
−
of Taylor of degree k for f wrt. ~v is defined by
j j −
(D11 . . . Dr(f ) f )(~v) · (w1 − v1 )j1 . . . (wr(f ) − vr(f ) )jr(f )
r(f )
− −
X
k ~ ,~v) =
P (f , w
j1 ! · . . . · jr(f ) !
j1 +...+jr(f ) ≤k
− − − −
where w~ is the vector of variables (w1 , . . . , wr(f ) ). For ~u ∈ 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 ∈ 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 ∈ 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.:
j j −
(D11 . . . Dr(f ) f )(~z) · (u1 − v1 )j1 . . . (ur(f ) − vr(f ) )jr(f )
r(f )
− −
X
k
r (f , ~u ,~v) = .
j1 ! · . . . · jr(f ) !
j1 +...+jr(f ) =k+1
− −
Our aim is to give an upper bound to |rk (f , ~u ,~v)|, under suitable hypothesis.
Definition 5. A function f ∈ 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 ∈ S, we have
j jr(f ) −
|(D11 . . . Dn f )(~z)| ≤ L · C j1 +...+jr(f ) .
Then, f is analytic if f is analytic in Dom(f ) and Dom(f ) is convex.
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 logarith-
mic 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 ∈ Ck+1 . Then, for Ĉ and L̂ the minimal
values satisfying the condition of Def. 5, for any k we denote with C(f , k) the
− −
~ ,~v) denote the polynomial over −w
value L̂· Ĉ k+1 . Moreover, let Rk (f , w ~ defined by
l m
Qr(f ) 2· k+1
− −
C(f , k) · (r(f ))k+1 · j=1 ((wj − vj )
2 + 1)
Rk (f , w
~ ,~v) = j k
k+1
r(f )
!
− − − − −
By definition, Rk (f , ~u ,~v) is an upper bound to |rk (f , ~u ,~v)| for all ~u ∈ Dom(f ).
− −
Moreover, Rk (f , ~u ,~v) gets close to 0 when k tends to the infinity. Formally:
− −
Proposition 2 ([11]). Let f ∈ F be analytic. Then, for all ~u ,~v ∈ Dom(f ) we have:
− − − − − −
(1) |rk (f , ~u ,~v)| ≤ Rk (f , ~u ,~v), and (2) limk→∞ Rk (f , ~u ,~v) = 0.
− − − − − − − − −
From |rk (f , ~u ,~v)| ≤ 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 ∈ F be analytic and ~v ∈ Dom(f ). Then for all vectors ~e =
(g1 (w1 ), . . . , gn (wn ))⊕(gn+1 (cn+1 ), . . . , gr(f ) (cr(f ) )) with cn+1 , . . . , cr(f ) ∈ IR, and r1 , . . . , rn ∈
IR s.t. g([0, r1 ]) × · · · × g([0, rn ]) × {gn+1 (cn+1 )} × · · · × {gr(f ) (cr(f ) )} ⊆ Dom(f ), we have
Z r1 Z rn ! ! Z r1 Z rn ! !
− k −− k −−
... f (~e) dwn . . . dw1 ≥ ... P (f ,~e,~v) − R (f ,~e,~v) dwn . . . dw1 .
0 0 0 0
−
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 de-
manding formula, provided the operator ∼ is in {<, ≤}, like in normal forms.
4 Approximation of Hybrid Automata
Approximations of HA are obtained by weakening formulae [6].
Definition 6 ([6]). An HA H 0 is an approximation of an HA H if H 0 is obtained
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.
Definition 7. For a normal form φ ∈ Φ(X, F) and k ∈ IN, if each f ∈ F \ {+, ·, −} that
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:
R z R z
1. If φ ≡ 0 1 . . . 0 n f (g1 (w1 ), . . . , gr(f ) (wr(f ) )) dwn . . . dw1 ∼ ax, then either A(φ, k)
is the singleton {φ}, if f is a polynomial, or A(φ, k) contains all the formulae
Z z1 Z zn ! !
−−−−−− − −−−−−− −
−
φk,~v ≡ ... k ~ ~ k ~ ~
P (f , g(w), v) − R (f , g(w), v) dwn . . . dw1 ∼ ax
0 0
−−−−−−
~ = (g (w ), . . . , g (w )) and ~−v ∈ Dom(f );
with g(w) 1 1 r(f ) r(f )
2. If φ ≡ φ1 ∧ φ2 then A(φ, k) = {φk1 ∧ φk2 | φk1 ∈ A(φ1 , k) and φk2 ∈ A(φ2 , k)};
3. If φ ≡ φ1 ∨ φ2 then A(φ, k) = {φk1 ∨ φk2 | φk1 ∈ A(φ1 , k) and φk2 ∈ A(φ2 , k)};
4. If φ ≡ ∃y. φ0 then A(φ, k) = {∃y. φk0 | φk0 ∈ A(φ0 , k)};
5. If φ ≡ ∀y. φ0 then A(φ, k) = {∀y. φk0 | φk0 ∈ A(φ0 , k)}.
Let us prove that all formulae in A(φ, k) are less demanding than φ.
Theorem 4. For a normal form φ and k ∈ IN s.t. A(φ, k) is defined, then ~φ ⊆ ~φ0
for all φ0 ∈ A(φ, k).
Proof (sketch). By structural induction over φ. The proof of the base case fol-
lows from Prop. 3, the inductive steps are standard.
From the approximation of normal forms we get an approximation of HA.
Definition 8. Assume an HA H s.t. A(φ, k) is defined for each formula φ in H. The
approximation of degree k for H is the set of the PHA denoted A(H, k) that are
obtained from H by replacing each formula φ in H with some formula in A(φ, k).
An immediate corollary of Thm. 4 states that Def. 8 respects Def. 6.
Corollary 1. Given any HA H and k ∈ IN, all PHA in A(H, k) are approximations
of H according to Def. 6.
2
Example 3. Let us consider the tank controller H of Ex. 1 where φin ≡ φin . The
set A(H, 4) contains the automaton obtained from H by approximating func-
−
tion g in φin by choosing the real 0 as vector ~v. (φout does not change since all
functions are polynomial). Since Dw (− cos(w)) = −Dwk cos(w) = − cos(w + k · π2 ), it
k
(y 2 )2
holds that P 4 (cos, y 2 , 0) ≡ − cos(0) − cos( π2 ) · (y 2 )1 − cos(2 · π2 ) · π
2! − cos(3 · 2 ) ·
2
(y )3 2
(y ) 4 y 4 y 8 2 6
(y ) +1
π 4 2
3! − cos(4 · 2 ) · 4! = −1 + 2 − 24 . Moreover, R (cos, y , 0) = C(cos, 4) · 120 .
π
Now, C(cos, 4) = max{| − cos(w + 4 · 2 )| : w ∈ Dom(g)} = 1, therefore we have that
Zt
2
y 4 y 8 y 12 + 1
φin ≡ φ0 ∧ x 0 − x − t = z ∧ −1 + − + dy = z.
4,0
0 2 24 120
The behaviour of any PHA Hk in A(H, k) approximates the behaviour of H,
meaning that any configuration reachable by H is reachable also by Hk , in the
same number of steps.
Theorem 5. Given any HA H and k, n ∈ IN, if A(H, k) is defined, then, for all PHA
Hk ∈ 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 Analysis of the Error
In order to limit the error introduced by the approximation, Def. 6 is strength-
ened in [6] by the notion of -approximation, which requires that any vector
satisfying a formula φ0 of the approximation H 0 must be “close” to at least one
vector satisfying the corresponding formula φ in the original HA H. We refor-
mulate this notion in terms of a notion of neighborhood of a space in IRn .
− − − −
Given two vectors ~up= (u1 , . . . , un ) and ~v = (v1 , . . . , vn ) in IRn , let d(~u ,~v) denote
− −
their distance d(~u ,~v) = (u1 − v1 )2 + . . . + (un − vn )2 .
− −
Given a vector ~v and a real > 0, let N(~v, ) denote the space of vectors
− − −
{~u | d(~v, ~u ) ≤ }. Then, for a space S ⊆ IRn and a real ≥ 0, the neighborhood of ray
− − − −
of space S is the set of spaces N(S, ) = {S 0 ⊇ S | ∀~v 0 ∈ S 0 ∃~v ∈ S s.t. d(~v,~v 0 ) ≤ }.
Definition 9.− A formula φ0 ∈ Φ(F, −
X) is an -approximation of a formula φ ∈
Φ(F, X) iff {v(~X) | v ∈ ~φ0 } ∈ N({v(~X) | v ∈ ~φ}, ).
Definition 10 ([6]). An HA H 0 is an -approximation of an HA H if H 0 is ob-
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 ∈ IN s.t. for all k > k0 we have that the set A(H, k)
contains only -approximations for H. In [11] we argued that formulae of the
−
form f (~x) ∼ c with ∼∈ {<, >} should be avoided, since they describe open sets. In
[11] we argued also that we can manage only formulae constraining variables
within bounded intervals, thus avoiding variables that can tend to the infinity.
Definition 11. A normal form φ ∈ Φ(F, X) is bounded iff for any variable x in φ
we have that Dom(x) = [lx , rx ], for suitable rationals lx , rx ∈ Q, and for each func-
tion f in φ we have that Dom(f ) = [l1 , r1 ] × . . . × [lr(f ) , rr(f ) ], for suitable rationals
l1 , r1 , . . . , lr(f ) , rr(f ) ∈ 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 φ.
Rd
Consider a normal form φ ≡ 0 f (x, y)dx ≤ 0. All formulae in A(φ, k) are of
Rd
the form 0 P(f , (x, y), (cx , cy )) − Rk (f , (x, y), (cx , cy )) dx ≤ 0 for a vector (cx , cy ) ∈
Rd
Dom(f ). Since φ is bounded, we can split Dom( 0 f (x, y)dx) (which is a function
over variable y) in m closed intervals S1 , . . . , Sm of size strictly < . Let i1 , . . . , il ∈
{1, . . . , m} be the indexes s.t. no evaluation in ~φ maps y to Si1 ∪ . . . ∪ Sil , namely
Rd
there is no u ∈ Si1 ∪ . . . ∪ Sil satisfying 0 f (x, u)dx ≤ 0. It is enough to show that
no evaluation vk in any ~φk with φk ∈ A(φ, k) maps y to Si1 ∪ . . . ∪ Sil . In fact, if
vk (y) ∈ Sj with j < {i1 , . . . , in }, by the definition of j1 , . . . , jl there is some v ∈ ~φ
with v(y) ∈ 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 ∈ Si1 ∪ . . . ∪ Sil the following inequality holds:
Z d
P(f , (x, u), (cx , cy )) − Rk (f , (x, u), (cx , cy )) dx > 0. (1)
0
Rd
Since Si1 ∪ . . . ∪ Sil is a closed set, 0 f (x, u)dx is a continuous function (which
follows by the continuity of f ), and the comparison symbol ≤ guarantees that
Rd Rd
0
f (x, u)dx is strictly positive in Si1 ∪. . .∪Sil , we can define ϑ = min{ 0 f (x, u)dx |
u ∈ Si1 ∪ . . . ∪ Sil }. Since [0, d] × Si1 ∪ . . . ∪ Sil is a closed set, we can define
ek = max{Rk (f , (u 0 , u), (cx , cy ))) | u 0 ∈ [0, d] ∧ u ∈ Si1 ∪ . . . ∪ Sil }. 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
Zd
(P(f , (x, u), (cx , cy )) − Rk (f , (x, u), (cx , cy )))dx
0
Zd
≥ (P(f , (x, u), (cx , cy )) − ek dx
0
Zd
= (P(f , (x, u), (cx , cy )) + rk (f , (x, u), (cx , cy )) − rk (f , (x, u), (cx , cy )) − ek dx
0
Zd Zd
k
= f (x, u) − r (f , (x, u), (cx , cy )) − ek dx ≥ f (x, u) − ek − ek dx
0 0
Zd Zd Zd Zd
ϑ
> f (x, u) − dx = f (x, u)dx − ϑ ≥ f (x, u)dx − f (x, u)dx = 0
0 d 0 0 0
with the first inequality by the definition of ek and the monotonicy of the inte-
gral, the second by |rk (f , (x, u), (cx , cy ))| ≤ 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 ϑ.
Theorem 6. Given any bounded normal form φ ∈ Φ(F, X) s.t. each subformula
Z z1 Z zn ! !
... f (g1 (w1 ), . . . , gr(f ) (wr(f ) )) dwn . . . dw1 ∼ ax
0 0
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.
Corollary 2. Given any HA H s.t. each formula in H satisfies the hypothesis of
Thm. 6, then, for each > 0, there exists some k0 s.t. for each k > k0 the set A(H, k)
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, ) = {R0 ⊇ R | ∀(q0 , ~u 0 ) ∈ R0 . ∃ (q, ~u ) ∈ R. q = q0 and d(~u , ~u 0 ) ≤ }.
Under the hypothesis of Thm. 6, for all n ∈ IN, if k tends to the infinity, then
the behavior of length at most n of each PHA Hk ∈ 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.
Theorem 7. Consider an HA H s.t. each formula in H satisfies the hypothesis of
Thm. 6. For each > 0 and n ∈ IN, there exists some k0 s.t., for all k > k0 , we have
Postn (Hk ) ∈ N(Postn (H), ) for all Hk ∈ A(H, k).
6 Conclusion and Future Works
In this paper we have defined syntactical over–approximations for Hybrid Au-
tomata enriched with integrals. The approximation is based on Taylor polyno-
mials. 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 for-
mula φ by using the polynomial which approximates the reminder to increas-
ing the Taylor polynomial. Moreover we can extend our work with function
variables by following the theory developed in [4, 5]. Finally, our results can be
used to study cyber physical attacks ([9]) by using tools like as Ariadne ([3])
based on Taylor theory.
References
1. R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P. H. Ho, X. Nicollin,
A. Olivero, J. Sifakis, S. Yovine. The Algorithmic Analysis of Hybrid Systems. Theor.
Comput. Sci. 138(1) (1995) 3–34.
2. R. Alur, T. A. Henzinger, P. H. Ho. Automatic Symbolic Verification of Embedded
Systems. IEEE Trans. Software Eng. 22(6) (1996) 181–201.
3. A. Balluchi, A. Casagrande, P. Collins, A. Ferrari, T. Villa, A. L. Sangiovanni-
Vincentelli. Ariadne, a Framework for Reachability Analysis of Hybrid Automata.
Proc. Int. Symp. on Mathematical Theory of Networks and Systems, 2006.
4. V. Castiglioni, R. Lanotte, S. Tini. A Function Elimination Method for Checking
Satisfiability of Arithmetical Logics. Proc. of the 23th International Workshop CS&P
2014, CEUR Workshop Proceedings 1269, pp. 46–57 (2014).
5. V. Castiglioni, R. Lanotte, S. Tini. A Function Elimination Method for Checking
Satisfiability of Arithmetical Logics. Fundamenta Informaticae 143: 51–71 (2016).
6. T. A. Henzinger, P. H. Ho, H. Wong-Toi. Algorithmic Analysis of Nonlinear Hybrid
Systems. IEEE Trans. Automat. Contr. 43(4) (1998) 540-554.
7. T. A. Henzinger, P. W. Kopke, A. Puri, P. Varaiya. What’s Decidable About Hybrid
Automata? J. Comput. Syst. Sci. 57(1) (1998) 94–124.
8. R. Lanotte. Expressive Power of Hybrid Systems with Real Variables, Integer Vari-
ables and Arrays. J. Autom. Lang. Comb. 12 (3): 373–405 (2007).
9. R. Lanotte, M. Merro, R. Muradore, L. Viganó. A Formal Approach to Cyber-
Physical Attacks. Submitted for publication.
10. R. Lanotte, S. Tini. Taylor Approximation for Hybrid Systems. Proc. Hybrid Sys-
tems: Computation and Control, LNCS 3114, Springer, Berlin, 1999, pp. 402–416.
11. R. Lanotte, S. Tini. Taylor Approximation for Hybrid Systems. Information and
Computation 205(11): 1575-1607 (2007).
12. R. Lanotte, A. Maggiolo-Schettini, S. Tini. Information flow in hybrid systems. ACM
Trans. Embedded Comput. Syst. 3 (4): 760–799 (2004).
13. A. Pnueli and J. Sifakis (Eds.), Special Issue on Hybrid Systems, Theor. Comput. Sci.
138(1) (1995).
14. D. Richardson. Some Undecidable Problems Involving Elementary Functions of a
Real Variable. J. Symbolic Logic 33 (1968), no. 4, 514-520.
15. A. Tarski. A Decision Method for Elementary Algebra and Geometry. University of
California Press, Berkeley, California, 1951.