1: \section{Introduction}
2: Hybrid systems combine discrete and continuous dynamics. The
3: dynamics of the continuous variables within a discrete state
4: are specified by differential equations or differential
5: inclusions. An important problem in the analysis and sysnthesis
6: of such systems is the so called {\em reachability problem},
7: which asks, for two sets of configurations of a given hybrid system,
8: say $\xcal_1$ and $\xcal_2$, where a configuration consists of
9: discrete and continuous components, whether or not there is a
10: hybrid trajectory with the initial configuration in $\xcal_1$
11: and the final configuration in $\xcal_2$. A hybrid trajectory
12: may be described as a trajectory of configurations consisting
13: of discrete state jumps and smooth arcs, where each arc evolves
14: according to the continuous dynamics of a discrete state, with
15: the starting and end points of each arc satisfying the jump
16: conditions of discrete transitions. A more precise definition is
17: presented in Sec. 2, which provides a concise introduction to
18: hybrid systems and the reachability problem.
19: \\
20:
21:
22:
23: The reachability problem is undecidable for certain classes
24: of linear hybrid systems (i.e., hybrid systems having linear
25: trajectories within each discrete state and linear or constant
26: reset maps, also called {\em constant slope hybrid systems})
27: \cite{Alur95, Kesten-JIC99}, although in some cases decidability
28: results have been obtained \cite{Laff99a,Laff99b} (see also
29: \cite{Kesten-JIC99}). Therefore, for a general hybrid system,
30: a reasonable alternative appears to be to find semi-decision
31: procedures for the reachability problem
32: \cite{Henzinger-IEEE-AC98,Pappas-IEEE-CDC00,ABDM-IEEE00}.
33: A computational approach to this problem also requires
34: finding the set of states reached by the continuous variables
35: evolving according to the dynamics of a discrete state. In this
36: paper, we consider the problem of computing and representing the
37: reach sets of the continuous variables within a discrete state
38: when the dynamics of the continuous variables are specified by
39: differential equations with initial conditions belonging to
40: a specified initial set.
41: \\
42:
43: In this context, various methods have been proposed in the literature
44: for finding reach sets of continuous variables \cite{DM98,LTS,V98}.
45: In Sec. 3, we describe a method for computing the reach sets based
46: on the idea that a subset of the boundary of the initial set may
47: be found, such that it is sufficient to compute the solutions with
48: the initial points lying in that set. This method is similar to that
49: in \cite{DM98} (and also to some extent to that described in \cite{LTS}).
50: In particular, we present a schematic algorithm, which is somewhat
51: more general in its scope than that in \cite{DM98} and simpler
52: compared to that in \cite{LTS}.
53: \\
54:
55:
56: % Formal analysis and verification of properties such as
57: % {\em safety, liveness, eventuality,} etc., often requires
58: % finding the set of phases reached by the continuous variables
59: % evolving according to the dynamics of a discrete state.
60:
61: Besides these algorithms for reach set computation, an
62: equally important issue the representation of the reach
63: sets for manipulating the sets efficiently. This requires
64: representation of the reach sets in terms of more convenient
65: sets such as, for example polyhedral or subalgebraic sets,
66: that are simple to represent and easy to handle for practical
67: purposes. However, since the representing class of sets may not
68: contain a member that exactly equals the reach set, we may have
69: to find approximations to the reach sets by those that belong
70: to the representing class. (See, for example, \cite{V98,ABDM00}
71: for approximation with polyhedra, and \cite{KV00} for approximation
72: using ellipsoids). Typically, over-approximations may be used
73: for verifying whether a safety requirement may potentially
74: be violated by any of the behaviours starting from a given
75: initial set, while under-approximations are needed for
76: characterizing a set of states from which a desirable
77: property is always achievable. We describe in Sec. 4 a
78: method for over-approximating the reach sets by polyhedra
79: when the dynamics are specified by linear differential
80: equations and the initial set is a polyhedron. These
81: algorithms are illustrated with some simple examples
82: in Sec. 5, while Sec. 6 concludes the paper.
83:
84: