IEEE Robotics & Automation Magazine - September 2011 - 29

Formal Verification of Hybrid Automata
Of particular importance in the verification of hybrid systems
is the reachable set, which consists of all the states that can be
reached under the dynamical evolution starting from a given
initial state set. In the following, given a hybrid automaton H,
we will distinguish between two kinds of reachable sets:
l Finite-time reachable set: given a set of states X0 and a
time point t, we denote with ReachSetH (X0 , t) the set
of all states that can be reached from X0 by a finite
trajectory with the total time length t.
l Infinite-time reachable set: given a set of states X0 , we denote
with ReachSetH (X0 ) the set of all states that can be
reached from X0 by a trajectory of arbitrary time length.
Finite-time and infinite-time reachability are the main tools
to verify properties of hybrid automata. Indeed, checking
safety properties (i.e., "something bad never happens")
reduces to the infinite-time reachability problem. Suppose
we wish to verify that a safety property u holds for a hybrid
automaton H; in other words, that u remains true for all possible executions starting from a set X0 of initial states. Then
we only need to prove that ReachSetH (X0 ) Sat(u),
where Sat(u) is the set of states where u is true. Finite-time
reachability can be used to verify timed safety properties, that
is, whether the property u is true at some execution time t.
Finally, by pairing finite-time and infinite-time reachability,
also timed stability properties can be verified, by checking
whether u is always true after some execution time t.
Other properties, such as liveness (i.e., "something good
eventually happens") and general stability properties (i.e.,
"the system eventually reaches the good region and never
leaves it"), require more complex techniques to be verified,
based on transformations on the model [6], [19].
In this article, we concentrate on the verification of the
following properties for the automatic puncturing test case:
1) The force applied to the patient by the end effector is always
less than a given threshold, except for the puncturing subtask. This can be formally stated by the following property:
Always(:Puncturing ! kfk < fmax ),
where f is the force component of the combined force/
torque vector h, and it can be verified by proving that,
for all states in ReachSetH (X0 ), if the location is different from Puncturing then kfk < fmax .
2) The task is feasible, and the position of the needle at the
end of the task is always inside the target region R4 . In the
most general case, this is a liveness property, and thus it
can be very hard to verify. To simplify the verification
procedure, we impose the task to be completed before a
maximum time tmax . In this simplified case, the property
can be formally stated as a timed safety property:
Always(t ¼ tmax ! (Stop ^ x 2 R4 )),
and formally verified by proving that, for all states in
ReachSetH (X0 , tmax ), the location is Stop and position
of the end effector is such that x 2 R4 .

In particular, we study the dependence of the truth of
these properties from the value of a particular design
parameter, namely, the uncertainty on the position of
the patient. Unfortunately, the reachability problem is not
decidable in general; there is no algorithm that can compute ReachSetH (X0 ) in an exact way without imposing
strong restrictions on the dynamics of the automaton [13].
Nevertheless, formal verification methods can be applied
to hybrid automata also in the general case. Suppose we
can compute an overapproximation S to ReachSetH
(X0 ), that is, a set S ReachSetH (X0 ). Then if S is a subset of Sat(u), so is the reachable set, and automaton H
respects the property. Conversely, if we can compute an
underapproximation S to ReachSetH (X0 ) (that is, a set
S ReachSetH (X0 )) that turns out to contain at least
one point outside Sat(u), we have proven that our hybrid
automaton H does not respect the safety property u. For
these reasons, many tools for reachability analysis of general hybrid automata are based on approximation techniques. The challenge is to find the best approximations.
Ariadne
Ariadne is a development environment to construct algorithms for hybrid system verification [2]-[4], jointly developed by The Centrum voor Wiskunde en Informatica
(Amsterdam), the University of Maastricht, University of
Verona, University of Udine, and company PARADES/
ALES (Rome). Given a hybrid automaton H and an initial
set X0 , it can compute two kinds of approximations to the
reachable set:
l an outer approximation O of the reachable set using upper
semantics, for both finite-time and infinite-time evolutions. Formally, a closed set O such that the closure of
ReachSetH ðX0 Þ is strictly contained in the interior of O
l an e-lower approximation Le of the reachable set using
lower semantics, for both finite-time and infinite-time
evolutions. Formally, Le is an open set where for every
point x 2 Le , there exists a point y 2 ReachSetH (X0 )
such that k x À y k< e.
The reachability algorithm of Ariadne takes as inputs the
hybrid automaton, initial set, and some numerical parameters, particularly a grid that sets the desired precision of the
results, an integration step to control the accuracy of the
approximations, and, for lower evolution, the value of e.
Then it proceeds as follows:
1) If the initial set X0 is larger than a grid cell, outer
approximate it on the grid, and let W be the obtained
set of cells. Otherwise, let W ¼ fX0 g.
2) Extract a new working cell W from W :
l Compute
an approximation of the continuous
evolution R(W, t) and final set F(W, t) for a time step t.
l If F(W, t) is outside the invariant of the current location, discard it.
l Check if some discrete transition is active in R(W, t). If
this is the case, compute an approximation of the
discrete evolution D(R(W, t)) for all active transitions.
SEPTEMBER 2011

IEEE ROBOTICS & AUTOMATION MAGAZINE

Table of Contents for the Digital Edition of IEEE Robotics & Automation Magazine - September 2011