Math. Control Signals Systems (2000) 13: 1±21 ( 2000 Springer-Verlag London Limited
Mathematics of Control, Signals, and Systems
O-Minimal Hybrid Systems* Gerardo Lafferriere,y George J. Pappas,z and Shankar Sastryz Abstract. An important approach to decidability questions for veri®cation algorithms of hybrid systems has been the construction of a bisimulation. Bisimulations are ®nite state quotients whose reachability properties are equivalent to those of the original in®nite state hybrid system. In this paper we introduce the notion of o-minimal hybrid systems, which are initialized hybrid systems whose relevant sets and ¯ows are de®nable in an o-minimal theory. We prove that o-minimal hybrid systems always admit ®nite bisimulations. We then present speci®c examples of hybrid systems with complex continuous dynamics for which ®nite bisimulations exist. Key words. Hybrid systems, Bisimulations, Model theory, O-minimality, Decidability.
1. Introduction Hybrid systems consist of ®nite state machines interacting with di¨erential equations. Various modeling formalisms, analysis, design, and control methodologies, as well as applications, can be found in [AHS], [AKNS1], [AKNS2], [GNRR], [HS], and [M1]. The theory of formal veri®cation is one of the main approaches for analyzing properties of hybrid systems. The system to be analyzed is ®rst modeled as a hybrid automaton, and the desired property is expressed using a formula from some temporal logic. Then model checking or deductive algorithms are used in order to guarantee that the system model indeed satis®es the desired property. Veri®cation algorithms are essentially reachability algorithms which check whether trajectories of the hybrid system can reach certain undesirable regions of the state space. Since hybrid systems have in®nite state spaces, decidability of veri®cation algorithms is very important. An important approach to decidability
* Date received: June 9, 1998. Date revised: June 28, 1999. This research was supported by DARPA under Grant F33615-98-C-3614. y Department of Mathematical Sciences, Portland State University, Portland, Oregon 97207, U.S.A.
[email protected]. z Department of Electrical Engineering and Computer Sciences, University of California at Berkeley, Berkeley, California 94720, U.S.A. fgpappas,
[email protected].
1
2
G. La¨erriere, G. J. Pappas, and S. Sastry
results for hybrid systems is the construction of special ®nite state quotients of the original in®nite state system called bisimulations. Bisimulations are reachabilitypreserving quotient systems in the sense that checking a property on the quotient system is equivalent to checking the property on the original system. Even though the focus of this paper is on reachability properties, bisimulations preserve many other complex properties expressible in branching time logics. In this approach, showing that an in®nite state hybrid system has a ®nite state bisimulation is the ®rst step in proving that veri®cation procedures are decidable. In [AD] a ®nite bisimulation was explicitly constructed for timed automata, and as a result reachability questions for such systems are decidable. Timed automata were the basis for showing that reachability for other classes of hybrid systems is decidable even though they do not admit a ®nite bisimulation themselves (multirate, initialized rectangular automata). These results as well as some undecidable questions are described in [ACH ], [AD], [H1], [HKPV], and the references therein. Computing ®nite bisimulations is clearly related to the problem of obtaining discrete abstractions of continuous systems which has been considered among others in [ASL], [CKN], and [RO] as well as in [CW2]. The common approach to obtaining bisimulations has been to utilize an algorithm which re®nes an initial partition of the state space until it becomes compatible with the system dynamics and the property to be preserved. Using this approach, there are three main issues that must be resolved: 1. When does the algorithm terminate after a ®nite number of iterations? 2. When does the resulting partition consist of a ®nite number of equivalence classes? 3. Are all the steps of the algorithm constructive? Resolving all three issues results in a decidable problem. Attacking the ®rst two issues has been solved either by explicitly providing an equivalence relation which is checked to be a bisimulation (timed automata), or by transforming the problem to one for which a bisimulation is known to exist (multirate, rectangular automata). The third issue is typically tackled using quanti®er elimination techniques from mathematical logic. In this paper we tackle the ®rst two issues for a large class of new hybrid systems. The third issue has been recently addressed in [LPY]. In order to answer the ®rst two questions, we need to identify classes of sets and ¯ows of vector ®elds with ®nite, global intersection properties. This is provided by the concept of ominimal (or order-minimal ) theories in mathematical logic [PS], [vdD], [vdDM1], [vdDM2], [W]. Using this concept, we introduce the notion of o-minimal hybrid systems which are initialized hybrid systems whose relevant sets (guards, resets, etc.) and ¯ows are de®nable in an o-minimal theory. We then prove that o-minimal hybrid systems always admit ®nite bisimulations. Examples show that relaxing the notion of o-minimality quickly leads into pathological situations. We list various o-minimal theories and the corresponding hybrid systems that are de®nable in them. This list captures hybrid systems with more complex continuous dynamics than those of timed automata but with more restrictive discrete dynamics. In addition to generating more classes of hybrid systems with ®nite bisimula-
O-Minimal Hybrid Systems
3
tions, the importance of this paper can be summarized by the following: 1. The results presented provide a uni®ed framework for decidability analysis of hybrid systems. 2. Generation of more o-minimal theories immediately leads to new classes of o-minimal hybrid systems. 3. Constructive results within o-minimal theories immediately lead to decidability results. By providing a purely model theoretic framework, we also extend the planar results of [LPS1] and [LPS2]. The outline of the paper is as follows: In Section 2 we review the notion of bisimulations of transitions systems. In Section 3 we de®ne a general class of hybrid systems and describe the bisimulation algorithm as it applies to hybrid systems. Section 4 presents the notion of o-minimality from model theory which is used in Section 5 in order to de®ne o-minimal hybrid systems and prove the main theorem. In Section 6 we list various classes of o-minimal hybrid systems, and ®nally Section 7 contains some conclusions. 2. Bisimulations of Transition Systems We adopt here the terminology of [H1] slightly modi®ed for our purposes. A transition system T
Q; S; !; QO ; QF consists of a (not necessarily ®nite) set Q of states, an alphabet S of events, a transition relation ! J Q S Q, a set QO J Q of initial states, and a set QF J Q of ®nal states. A transition
q1 ; s; q2 A s ! is denoted as q1 ! q2 . The transition system is ®nite if the cardinality of Q is ®nite and it is in®nite otherwise. A region is a subset P J Q. Given s A S we de®ne the predecessor Pres
P of a region P as s
Pres
P fq A Q j b p A P and q ! pg:
2:1
Given an equivalence relation @ J Q Q on the state space one can de®ne a quotient transition system as follows. Let Q=@ denote the quotient space. For a region P we denote by P=@ the collection of all equivalence classes which intersect P. The transition relation !@ on the quotient space is de®ned as follows: for s s Q1 ; Q2 A Q=@, Q1 !@ Q2 i¨ there exist q1 A Q1 and q2 A Q2 such that q1 ! q2 . The quotient transition system is then T=@
Q=@; S; !@ ; QO =@; QF =@. Given an equivalence relation @ on Q, we call a set a @-block if it is a union of equivalence classes. De®nition 2.1. The equivalence relation @ is a bisimulation of T i¨ QO ; QF are @-blocks and for all s A S and all @-blocks P, the region Pres
P is a @-block. In this case the systems T and T=@ are called bisimilar. We also say that a partition is a bisimulation when its induced equivalence relation is a bisimulation. A bisimulation is called ®nite if it has a ®nite number of equivalence classes. Bisimulations are very important because bisimilar transition
4
G. La¨erriere, G. J. Pappas, and S. Sastry
systems preserve reachability properties in addition to other more complex properties expressible in branching time logics [H1]. Therefore, checking properties on the bisimilar transition system is equivalent to checking properties of the original transition system. This is very useful in reducing the complexity of various veri®cation algorithms where Q is ®nite but very large. In addition, if T is in®nite and T=@ is a ®nite bisimulation, then veri®cation algorithms for in®nite systems are guaranteed to terminate. This approach was successfully applied to timed automata [AD]. It should be noted that the notion of bisimulation is analogous to the notion of dynamic consistency [CW1], [CW2], [PLS]. If @ is a bisimulation, it can be easily shown that if p @ q, then B1: p A QF i¨ q A QF , and p A QO i¨ q A QO , s
s
B2: if p ! p 0 , then there exists q 0 such that q ! q 0 and p 0 @ q 0 . Based on the above characterization, given a transition system T, the following algorithm computes increasingly ®ner partitions of the state space Q. If the algorithm terminates, then the resulting quotient transition system is a ®nite bisimulation. The state space Q=@ is called a bisimilarity quotient. Algorithm 1 (Bisimulation Algorithm for Transition Systems) Set: Q=@ fQO X QF ; QO nQF ; QF nQO ; Qn
QO W QF g while: bP, P 0 A Q=@ and s A S such that q 0 P X Pres
P 0 0 P set: P1 P X Pres
P 0 , P2 PnPres
P 0 re®ne: Q=@
Q=@nfPg W fP1 ; P2 g end while: Notice that each time the partition Q=@ is re®ned, the transitions are updated to account for the newly subdivided sets. When checking speci®c properties, such as reachability to the set QF , one might simplify the algorithm by starting with a coarser partition, for example, fQF ; QnQF g. In general one should include in the initial partition all additional sets relevant to the veri®cation problem of interest (such as safe or unsafe regions). The larger the initial class of sets the more di½cult it is for the algorithm to terminate. 3. Bisimulations of Hybrid Systems We focus on transition systems generated by the following class of hybrid systems. De®nition 3.1.
A hybrid system is a tuple H
X ; X0 ; XF ; F ; E; I ; G; R where:
X XD XC is the state space with XD fq1 ; . . . ; qn g and XC a manifold. X0 J X is the set of initial states. XF J X is the set of ®nal states. F : X ! TXC assigns to each discrete location q A XD a vector ®eld F
q; . E J XD XD is the set of edges (which induce discrete transitions as shown below).
O-Minimal Hybrid Systems
5
I : XD ! 2 XC assigns to each location a set I
q J XC called the invariant. G : E ! XD 2 XC assigns to e
q1 ; q2 A E a guard of the form fq1 g U,
U J I
q1 .
R : E ! XD 2 XC assigns to e
q1 ; q2 A E a reset of the form fq2 g V ,
V J I
q2 .
Trajectories of the hybrid system H originate at any
q; x A X0 and consist of either continuous evolutions or discrete jumps. Continuous trajectories keep the discrete part of the state constant, and the continuous part evolves according to the vector ®eld F
q; as long as (the continuous part of ) the trajectory remains inside the invariant set I
q. If the trajectory exits I
q, then a discrete transition is forced. If, during the continuous evolution, a state
q; x A G
e is reached for some e A E, then a discrete transition induced by e is enabled. The state of the hybrid system may then instantaneously jump from
q; x to any
q 0 ; x 0 A R
e and the continuous part of the trajectory then evolves according to the vector ®eld F
q 0 ; . Notice that even though the continuous evolution is deterministic, the discrete evolution may be nondeterministic. The discrete transitions allowed in our model are more restrictive than those in initialized rectangular automata [ACH ], [AD], [PV]. In rectangular automata, the continuous dynamics are decoupled and each component of the continuous part of the state may be either reset nondeterministically to an interval or remain the same. If, however, the dynamics of a particular component changes, then the reset map cannot be the identity map on that component. In this paper we restrict the reset maps in order to allow complex and fully coupled dynamics. Finally, we assume that our hybrid system model is nonblocking, that is, from every state either a continuous evolution or a discrete transition is possible. Example 3.2. A typical hybrid system is shown in Fig. 1. The state space is fQ1; Q2g R2 . The initial states are of the form fQ1g f
x; y A R2 j 0 < x < 1; 1 < y < 2g. The discrete dynamics consists of two transitions along the edges e1
Q1; Q2 and e2
Q2; Q1. Within location Q1, the continuous variables x and y evolve according to a di¨erential equation as long as
x; y A I
Q1 f
x; y A R2 j x U 5g. Once x > 5, a discrete transition along e1 is forced and x, y are nondeterministically reset to values in ®xed sets. The system then
Fig. 1. A typical hybrid automation.
6
G. La¨erriere, G. J. Pappas, and S. Sastry
evolves according to the vector ®eld associated with Q2. The evolution from that point on is similar. We would like to ®nd out whether the system will reach the set of ®nal states fQ2 g f
x; y A R2 j x < 5g. Every hybrid system H
X ; X0 ; XF ; F ; E; I ; G; R generates a transition system T
Q; S; !; QO ; QF by setting Q X , QO X0 , QF XF , S E W ftg, e
t
and !
6e A E ! W ! where: e
Discrete Transitions:
q; x !
q 0 ; x 0 for e A E i¨
q; x A G
e and
q 0 ; x 0 A R
e. t Continuous Transitions:
q1 ; x1 !
q2 ; x2 i¨ q1 q2 and there exists d V 0 and a curve x : 0; d ! M with x
0 x1 , x
d x2 and for all t A 0; d it satis®es x 0 F
q1 ; x
t and x
t A I
q1 . The continuous t transitions are time-abstract transitions, in the sense that the time it takes to reach one state from another is ignored. Having de®ned the cont e tinuous and discrete transitions ! and ! allows us to de®ne formally Pret
P and Pree
P for e A E and any region P J X using (2.1). Furthermore, the structure of the discrete transitions allowed in our hybrid system model result in Pree
P
q G
e
if if
P X R
e q, P X R
e 0 q,
3:1
for all e A E and regions P. Therefore, if the sets R
e and G
e are blocks of any partition of the state space, then no partition re®nement is necessary in the bisimulation algorithm due to any discrete transitions. This fact, in a sense, decouples the continuous and discrete components of the hybrid system. In turn, this implies that the initial partition in the bisimulation algorithm should contain the invariants, guards, and reset sets, in addition to the initial and ®nal sets. This allows us to carry out the algorithm independently for each location. More precisely, de®ne for any region P J X and q A XD the set Pq fx A XC :
q; x A Pg. For each location q A XD consider the ®nite collection of sets Aq fI
q;
X0 q ;
XF q g W fG
eq ; R
eq : e A Eg;
3:2
which describes the initial and ®nal states, guards, invariants, and resets associated with location q. Let Sq be the coarsest partition of XC compatible with the collection Aq (by compatible we mean that each set in Aq is a union of sets in Sq ). The (®nite) partition Sq can be easily computed by successively ®nding the intersections between each of the sets in Aq and their complements. We de®ne
q; Sq to be the set ffqg P j P A Sq g. These collections
q; Sq will be the starting partitions of the bisimulation algorithm. In addition, since by de®nition Pret
P applies to regions P J X , but not to its continuous projection Pq , we de®ne for Y J XC the operator Preq
Y
Pret
fqg Y q . The general bisimulation algorithm for transition systems then takes the following form for the class of hybrid systems that are considered in this paper.
O-Minimal Hybrid Systems
7
Algorithm 2 (Bisimulation Algorithm for Hybrid Systems) Set: X =@ 6q
q; Sq for: q A XD while: bP, P 0 A Sq such that q 0 P X Preq
P 0 0 P Set: P1 P X Preq
P 0 ; P2 PnPreq
P 0 re®ne: Sq
Sq nfPg W fP1 ; P2 g end while: end for: It is clear from the structure of the bisimulation algorithm that the iteration is carried out independently for each discrete location. In order for the above algorithm to terminate, the partition re®nement process must terminate for each discrete location q A XD . It therefore su½ces to look at one continuous slice of the hybrid system at a time and see whether we can construct a ®nite bisimulation that is consistent with all relevant sets of each location q as well as with the trajectories of the vector ®eld F
q; . The following example shows that, even in apparently simple situations, Algorithm 2 does not terminate. Example 3.3.
Consider the hybrid system with only one discrete location q and 1 1 let F be the linear vector ®eld x on R2 . Assume the partition of R2 1 1 consists of the following three sets (see Fig. 2): P1 f
x; 0 : 0 U x U 4g, P2 f
x; 0 : 4 U x < 0g, P3 R2 n
P1 W P2 . The trajectories of F are spirals moving away from the origin. The ®rst iteration of the algorithm partitions P2 into P4 P2 X Preq
P1 f
x; 0 : x1 U x < 0g and P2 nPreq
P1 . Here x1 < 0 is the x-coordinate of the ®rst intersection point of the spiral through
4; 0 with P2 . The second iteration subdivides P1 into P5 P1 X Preq
P4 f
x; 0 : 0 U x U x2 g
Fig. 2.
Algorithm 2 does not terminate.
8
G. La¨erriere, G. J. Pappas, and S. Sastry
and P1 nPreq
P4 where x2 > 0 is the x-coordinate of the next point of intersection of the spiral with P1 . This process continues inde®nitely since the spiral intersects P1 in in®nitely many points, and therefore the algorithm does not terminate. From the above example it is clear that the critical problem one must investigate is how the trajectories of F
q; interact with the sets Sq for a single location q. This requires that the trajectories of the vector ®eld F
q; have ``nice'' intersection properties with such sets. Since the goal is to obtain ®nite partitions, it will become important that we restrict the study to classes of sets with global ``®niteness'' properties, for example, sets with ®nitely many connected components. In the next section we identify such classes of sets and vector ®elds using the concept of o-minimality from model theory. 4. Model Theory This section provides a brief introduction to mathematical logic and model theory. A clear expository survey of model theoretic results that are relevant to this paper is [M2]. For a more detailed treatment of model theory the reader is referred to [H2] and [vD]. 4.1. Languages and Formulas A language is a set of symbols separated into three groups: relations, functions, and constants. The sets L0 f s > 0 such that gx
s B S n
S0 W W Si 1 and gx
t A S n
S0 W W Si 1 . If gx
s A Sj for some j U i 1 and gx
s A S for all s U s U t, then Lemma 5.5 would imply that gx
t A Sj which is not true. Therefore there exists s, s U s < t, such that gx
s B S. We set si s. If gx
t A Si , then we set ti t. Otherwise, there exist t 0 > s 0 > t such that gx
s 0 B S n
S0 W W Si 1 and gx
t 0 A S n
S0 W W Si 1 . Since x A Si1 , gx
s B S n
S0 W W Si , and t 0 > s we must have gx
t 0 B S n
S0 W W Si . Therefore gx
t 0 A Si and we set ti t 0 . By the inductive hypothesis there exist t~1 > ~s1 > > t~i 1 > ~si 1 > 0 such that ggx
ti
~sj B S, ggx
ti
t~j A Sj , for j 1; . . . ; i 1. Setting sj ~sj ti , tj t~j ti for j 1; . . . ; i 1 we get the desired conclusion. 9 The last lemma together with Lemma 5.4 proves that if x A Si , then Gx X S has at least i connected components. This, in turn, proves the claim.
O-Minimal Hybrid Systems
15
Notice that Lemmas 5.4 and 5.5 together imply that if x A Si , then Gx X Si has exactly one connected component. By carrying out the subdivision into the sets Si for all S A P we obtain a new ~ of Rn with the property ®nite partition P ~ and each trajectory g of F such that g
t0 ; g
t1 A S we (P) For each S A P, have g
t A S for all t with t0 U t U t1 . In particular, for each x A S, the set Gx X S has exactly one connected component. ~ the number of sets in P ~ and write P ~ fSi : i 1; . . . ; rg. We denote by r r
P We introduce two functions, I and C, acting on pairs of sets, de®ned by I
A; B A X Pre
B; C
A; B AnPre
B: It is clear that if A and B are de®nable, then I
A; B and C
A; B are de®nable. Notice also that for each A; B the sets I
A; B; C
A; B form a partition of A. For each i, 1 U i U r, consider all the partitions of Si de®ned by I
Si ; Q
Sj1 ; Q
Sj2 ; . . . ; Q
Sjk 1 ; Sjk ;
5:1
C
Si ; Q
Sj1 ; Q
Sj2 ; . . . ; Q
Sjk 1 ; Sjk ;
5:2
where Q is either I or C and 1 U j l U r for l 1; . . . ; k and k U r. This is a ®nite collection of ®nite partitions. We let B denote the coarsest partition of Rn compatible with all such partitions. Claim. B is a bisimulation. The intuitive basis for this proof is the fact that the partitions constructed so far are done ``along the ¯ow of F.'' That is, two sets in B which are subsets of the ~ cannot be connected by a trajectory of F. same set in P To prove the claim ®rst notice that the sets in B are (®nite) intersections of sets of the form (5.1) or (5.2). Notice also that by construction B is a re®nement of P. ~ be written as To check the bisimulation property let B A B, B J Si A P, m
B 7 Pl ; l1
where each Pl is of the form (5.1) or (5.2). We want to prove ®rst that m
Pre
B 7 Pre
Pl : l1
m
5:3
The inclusion Pre
B J 7l1 Pre
Pl is straightforward. For the other one let m x A 7l1 Pre
Pl . For each l there exists tl V 0 such that gx
tl A Pl . Each set Pl is of the form I
Si ; Al or C
Si ; Al for some Al 's. Hence, gx
tl A Si for all l. We
16
G. La¨erriere, G. J. Pappas, and S. Sastry
now want to show that indeed gx
tl A B for all tl . Consider the following property of a set A: ~ then, for all s with g
s A S, (Q) For any trajectory g of F, if g
s0 A A J S A P, g
s A A. We show that if a set A has Property (Q), then so do I
S 0 ; A and C
S 0 ; A for ~ Let g
s0 A I
S 0 ; A J S 0 . Then g
s0 A S 0 and there exists t V s0 such any S 0 A P. ~ By Propthat g
t A A. If g
t A S 0 , then we have S S 0 since both belong to P. 0 erty (Q) g
s A A J Pre
A for all s such that g
s A S . Therefore g
s A I
S 0 ; A for all such s. On the other hand, if g
t B S 0 , then A X S 0 J S X S 0 q. Let g
s A S 0 . By Property (P) applied to S 0 we get that s U t. However, then g
s A Pre
A X S 0 as desired. The proof for C
S 0 ; A is analogous. Proceeding by induction it is easy to show that the sets Pl have Property (Q) and this completes the proof of (5.3). Notice also, that Pre
A W B Pre
A W Pre
B for all sets A, B. To complete the proof that B is a bisimulation we only need to show that for ~ the set S X Pre
Pl is a union of sets in B. The set each l, and each set S A P, S X Pre
Pl I
S; Pl is of the form (5.1) with k U r 1. If k < r 1 we already know that I
S; Pl is a union of sets in B. We only need to consider the case k r 1. There are two possibilities for I
S; Pl : 1. There are two or more occurrences of C in I
S; Pl . 2. There are r 1 occurrences of I in I
S; Pl , and, therefore, at least one ~ is repeated as an argument of I. Si A P In case 1 the following two formulas, and boolean algebra, show how to rewrite I
S; Pl either with fewer terms or using only I: C
S3 ; C
S2 ; S1 C
S3 ; S2 W I
S3 ; I
S2 ; S1 ;
5:4
C
S3 ; I
S2 ; S1 C
S3 ; S2 W I
S3 ; C
S2 ; S1 :
5:5
Both formulas can be proved with arguments similar to the ones above, relying on Property (P). We give the proof of formula (5.4), the other one is analogous. That the left side is included in the right side does not require any special property of the sets Si . Indeed, x A C
S3 ; C
S2 ; S1 S3 nPre
S2 nPre
S1 means x A S3 5
Et V 0
gx
t B S2 4
gx
t A S2 5bt 0 V t
gx
t 0 A S1 : Therefore, if, for all t V 0, gx
t B S2 , then x A S3 nPre
S2 . On the other hand, if there is t V 0 such that gx
t A S2 and t 0 V t such that gx
t 0 A S1 , then x A Pre
S2 X Pre
S1 I
S3 ; I
S2 ; S1 and the inclusion is proved. For the other inclusion, ®rst notice that C
S3 ; S2 S3 nPre
S2 J S3 n Pre
S2 nPre
S1 C
S3 ; C
S2 ; S1 . Let now x A I
S3 ; I
S2 ; S1 . So x A S3 and there exist t 0 V t V 0 such that gx
t A S2 and gx
t 0 A S1 . To show the desired inclusion we need to show that, for all t 00 V 0, gx
t 00 B S2 nPre
S1 . We do so by contradiction. Suppose there exists t 00 V 0 such that gx
t 00 A S2 nPre
S1 . Since gx
t 0 A S1 and gx
t 00 B Pre
S1 we must have t 00 > t 0 . Moreover, using gx
t A S2 , gx
t 00 A S2 , t U t 0 U t 00 , and property (P) applied to S2 we get gx
t 0 A S2 . Since
O-Minimal Hybrid Systems
17
the Si 's form a partition and gx
t 0 A S1 X S2 we also get S1 S2 . However, then S2 nPre
S1 q which contradicts gx
t 00 A S2 nPre
S1 . This concludes the proof of the inclusion and of formula (5.4). Finally, we consider case 2. If the two occurrences of the same Si are consecutive, then the expression may be rewritten with fewer terms (I
Si ; I
Si ; A I
Si ; A for any set A). If the occurrences of Si alternate with a di¨erent Sj , then we use Property (P) to conclude that I
S; Pl q (since I
Si ; I
Sj ; Si q for i 0 j). This concludes the proof that B is a bisimulation. 9 In the next section we list various classes of o-minimal hybrid systems. 6. Classes of O-Minimal Hybrid Systems In this section we apply Theorem 5.3 to several special classes of o-minimal hybrid systems. For each o-minimal theory of Table 1, we provide examples of de®nable, o-minimal hybrid systems. 6.1. Rlin
R;
