9512.net

甜梦文库

甜梦文库

当前位置：首页 >> >> # Reachability verification for hybrid automata

Reachability Veri cation for Hybrid Automata

Thomas A. Henzinger1 ? and Vlad Rusu2 ??

1 EECS Department, University of California, Berkeley, CA 2 SRI International, Computer Science Laboratory, Menlo Park, CA

rusu@csl.sri.com tah@eecs.berkeley.edu

Abstract. We study the reachability problem for hybrid automata.

Automatic approaches, which attempt to construct the reachable region by symbolic execution, often do not terminate. In these cases, we require the user to guess the reachable region, and we use a theorem prover (Pvs) to verify the guess. We classify hybrid automata according to the theory in which their reachable region can be de ned nitely. This is the theory in which the prover needs to operate in order to verify the guess. The approach is interesting, because an appropriate guess can often be deduced by extrapolating from the rst few steps of symbolic execution.

Keywords: hybrid automata, reachability veri cation, theorem proving.

1 Introduction

Hybrid automata are a speci cation and veri cation model for hybrid systems ACH+ 95], systems that involve mixed continuous and discrete evolutions of variables. The problem that underlies the safety veri cation for hybrid automata is reachability : can an unsafe state be reached from an initial state by executing the system? The traditional approach to reachability attempts to compute the set of reachable states by successive approximation, starting from the set of initial states and repeatedly adding new reachable states. This computation can be automated and is guaranteed to converge in some special cases KPSY93, AD94, ACH+ 95, HKPV95, RR96], for which the reachability problem is decidable. In general, however, this approach, which we call reachability construction, may not be automatable or may not converge. It is for this reason that in this paper, we pursue a di erent approach, called reachability veri cation. In reachability veri cation, the user guesses the set of reachable states, and then a theorem prover is applied to verify the guess. A guess has the form of a logical formula, which is true exactly for the states that are guessed to be reachable. We classify hybrid automata as to what logical

This research was supported in part by the ONR YIP award N00014-95-1-0520, by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the AFOSR contract F49620-93-1-0056, by the ARO MURI grant DAAH-04-96-1-0341, by the ARPA grant NAG2-892, and by the SRC contract 95-DC-324.036. ?? Supported by Lavoisier grant of the French Foreign A airs Ministry and by SRI.

?

theory su ces to de ne the set of reachable states. The formula to be guessed must lie in this theory, and the veri cation part amounts to a proof in this theory. Hence, the simpler the theory, the more constrained the guess and the easier the veri cation. In some cases|for example, the case of additive-inductive hybrid automata, where the set of reachable states is de nable in a decidable subtheory of (IR; IN; +; )| the veri cation part is often completely automatic. The reachability veri cation approach is interesting because when successive approximation does not converge, a suitable guess can often be found by studying and extrapolating the rst few iterations of successive approximation. In this way, some automatic heuristics can be developed to aid the guessing part. The rest of the paper is organized as follows. In Section 2, we present the hybrid automaton model, the reachability construction method, and the reachability veri cation method. We restrict our attention to linear hybrid automata, for which reachability construction can be automated and has been implemented in veri cation tools such as HyTech AHH96]. In Section 3, we classify linear hybrid automata according to the theory in which the set of reachable states is de nable. For example, all linear hybrid automata for which reachability construction converges are polyhedral, as their reachable region can be de ned in (IR; +; ). We give examples of linear hybrid automata whose reachable regions are quite simple yet non-polyhedral (e.g., additive-inductive), as well as examples of linear hybrid automata whose reachable regions are quite complex (e.g., most naturally expressed using trigonometric functions). We also present a restricted subclass of additive-inductive automata for which the reachable region can be computed algorithmically, even though reachability construction does not necessarily terminate. Finally, in Section 4 we describe an embedding of hybrid automata into the theorem prover Pvs ORR+ 96], and apply the reachability veri cation method to some well-known examples for which reachability construction fails.

2 Linear Hybrid Automata and Reachability Analysis

Hybrid automata ACH+ 95] are nite automata enriched with a nite set of realvalued variables. In each location, the variables evolve continuously according to di erential activities, as long as the location's invariant remains true; then, when a transition guard becomes true, the control may proceed to another location, and reset some of the variables to new values. We restrict our attention to a simple class of hybrid automata, allowing only straight-line activities and resets of variables to zero. More general feature can be approximated in the simpler framework, with additional locations, transitions, and variables HHWT98]. Below (Figure 1) is an example of a linear hybrid automaton. It has the three locations s1 , s2 , s3 and the three variables x, y, z . The automaton starts at location s1 with variable x set to 0 and variables y; z set to 1, and control can remain at location s1 while the invariant x y is true. Here, x increases with slope 1 (x = 1) and y remains constant at 1 (y = 0). Thus, control can stay _ _ at s1 for at most 1 time unit, until x reaches 1. When this condition becomes

true, control leaves s1 by taking a transition. Here, the only available transition is the one that leads to s2 , which is enabled when x = y. Then, control goes to location s2 , where x decreases (x = ?1), and stays there until x reaches 0. _ When this happens, the transition from s2 to s3 is enabled and control goes to s3 , by assigning variable z to 0 in the process. The process continues likewise at location s3 .

z x=0 y=1 z=1 x y x=1 _ y=0 _ z=0 _ s1

=1

x=y

x 0 x= 1 _ y=0 _ z=0 _ s2

?

x=0 z := 0

z 1 x=0 _ y=1 _ z=1 _ s3

Figure 1. Example of a linear hybrid automaton

Syntax of linear hybrid automata. A convex linear predicate is a system of

linear inequalities over given variables. A linear predicate is a nite disjunction of convex linear predicates. A linear hybrid automaton consists of the following elements: { a nite set X = fx1; x2 ; : : : ; xn g of variables; { a nite set L of locations; { a nite multiset of transitions T L L; { for each location l 2 L: an invariant Inv (l ), which is a convex linear predicate on the variables; an activity Act (l ), which is a tuple of di erentials laws (on law per variable) of the form x = A(l; x). Here, A(l; x) is a rational constant, also _ called the slope of variable x at location l; an initial condition Init (l ), which is a convex linear predicate on the variables; { for each transition t 2 T : a guard Guard (t ), which is a convex linear predicate on the variables; a reset Reset (t ), which is a set of variables Reset (t ) X .

Semantics. The semantics of hybrid automata builds upon the following preliminary notions. A valuation is a function v : X ! IR that associates a real number v(x) to each variable x 2 X . Given a variable valuation v and a linear predicate P over the variables, we say v satis es P , written P (v) = true, if by replacing in P each variable x with its value v(x), one obtains a true

statement. In particular, if valuation v satis es the invariant of location l (respectively, the guard of transition t) we write Inv (l )(v) = true (respectively, Guard (t )(v) = true). Given a valuation v and a subset Y X of variables, we write v Y := 0] for the valuation that assigns 0 to all variables in Y , and agrees with v on all variables in X n Y . Given a valuation v, a location l 2 L, and a non-negative real 2 IR+ , we write v +l for the valuation that assigns to each variable x in X the value v(x) + A(l; x) , where A(l; x) is the slope of variable x at location l. The semantic features of a hybrid automaton are the following: { a state is a pair (l; v), where l is a location and v a valuation such that Inv (l )(v) = true; { for a non-negative real 2 IR+ , there is a continuous step of duration between two states (l; v) and (l; v0 ) denoted (l; v) ! (l; v0 ), if v0 = v +l ; { for a transition a = (l; l0) 2 T , there is a discrete step of label a between two a states (l; v) and (l0 ; v0 ) denoted (l; v) ! (l0 ; v0 ), if Guard (t )(v) = true and 0 = v Reset (t ) := 0]; v { a run is a nite sequence of continuous and discrete steps (l0; v0) ! (l1; v1 ) ! ! (lm ; vm ) such that the rst state (l0 ; v0 ) is initial; i.e., v0 satis es the initial condition Init(l0 ). A state is reachable if it coincides with the last state of a run. A linear region is a pair hl; P i, where l is a location and P is a linear predicate on the automaton variables. A state (s; v) satis es the linear region hl; P i if s = l and v satis es P . In this case we also say that the region hl; P i contains the state (s; v). The reachability problem for linear hybrid automata is: given a linear hybrid automaton A and a set R of linear regions, is there a reachable state of A that is contained in some region in R. We discuss below two kinds of approaches to this problem. execution of the hybrid automaton. It consists in successively approximating the reachable region, starting from the initial region, and iterating successor operations until the computation converges. There are two kinds of successors. ~ The continuous successor of a region hl; P i is the region hl; Pl i that contains all the states that can be reached from states satisfying hl; P i, by a single ~ continuous step. The predicate Pl is obtained by extension of P at location l. Suppose P is a linear predicate over the variables x1 ; : : : ; xn , and that variable xi evolves in location l by the law xi = ki (for all i 2 f1; : : : ; ng); then, the _ extension of P at location l is described by the following predicate:

Reachability construction ACH+95]. This method performs a symbolic

~ Pl = 9

0:P (x1 ? k1 ; : : : ; xn ? kn )

(1)

It can be shown that the elimination of the existential quanti er in formula (1) can be performed, and it again produces a linear predicate in variables x1 ; : : : ; xn : the continuous successor of a linear region is still a linear region.

The discrete successor of a linear region hl; P i by a transition (l; l0) 2 T is the ~ region hl0 ; P(l;l ) i that contains all the states that can be reached from states ~ satisfying hl; P i, by a single discrete step. The predicate P(l;l ) is obtained from 0 ). Suppose that P is a linear predicate over P by projection over transition (l; l variables x1 ; : : : ; xn , and transition (l; l0) resets the variables xi1 ; xi2 ; : : : ; xip ; then, the projection of P over transition (l; l0 ) can be described by the following predicate:

0 0

~ P(l;l ) = (xi1 = 0 ^ xi2 = 0 ^

0

^ xip = 0) ^ 9xi1 :9xi2 : : : 9xip :P (x ; : : : ; xn )

1

(2)

It can be shown that the elimination the existential quanti ers in formula (2) can be performed, and it again produces a linear predicate in variables x1 ; : : : ; xn . Thus, the discrete successor of a linear region is still a linear region. Reachability construction consists in iterating the following Post procedure:

Input: set A of linear regions. Output: set B of linear regions, initially empty. For each linear region hl; P i in the set A, for each transition (l; l0 ) with origin l: { let P be the intersection of P with the guard of transition (l; l0) { let P be the projection of P over transition (l; l0) { let P be the intersection of P with the invariant of l0 { let P be the extension of P at state l0 { let P be the intersection of P with the invariant of l0 { add hl0; P i to set B.

1 2 1 3 2 4 3 5 4 5

We denote by Postk (I ) the set of regions obtained by applying k times the ~ Post operation to the set of initial regions I = fhl; Init (l )l ^ Inv (l )ijl 2 Lg, and W Postk (I ). This is also called by Post (I ) the countably in nite union k2I N the reachable region, and it represents all the reachable states of the hybrid automaton. Once Post (I ) is computed, the reachability problem for a set of linear regions R can be solved by checking if the intersection Post (I ) \ R is non-empty. We call reachability construction the process of computing the sequence I , Post (I ), Post2 (I ) : : : of sets of regions. If, for some k 2 IN , it is the case that Postk+1 (I ) Postk (I ), then reachability construction terminates in nitely many steps, and Post (I ) = Postk (I ). This does not happen in general for linear hybrid automata HKPV95]. Some subclasses for which reachability construction terminates have been identi ed, such as timed automata, initialized rectangular hybrid automata1,and others KPSY93, AD94, ACH+ 95, HKPV95, RR96]. For these classes, the reachability problem is decidable. Reachability construction is the procedure implemented in symbolic model-checking tools like HyTech AHH96].

1 For these classes, termination is achieved by slightly modifying the automaton.

Reachability veri cation. We de ne a new approach to the reachability prob-

lem, called the reachability veri cation method. This method can succeed in cases when reachability construction fails. Reachability veri cation consists of two steps: rst, to guess the reachable region; second, to verify that the guess is correct. In many cases (some of which are presented in Sections 3 and 4), a suitable guess can be found using the simple heuristic described below, and the veri cation can be performed by induction, using a theorem prover. It appears that when reachability construction does not terminate, the reachable region of a hybrid automaton can still behave in a regular manner. As an example, consider the hybrid automaton in Figure 1. By studying the reachability construction over a few iterations (performed in this situation by the tool HyTech), it can be seen that the reachable region is described by the following set of regions: fhs1 ; 9i 2 IN:(i 1 ^ x i ^ y = i ^ z = 1)i; hs2 ; 9i 2 IN:(i 1 ^ x i ^ y = i ^ z = 1)i; (3) hs3 ; 9i 2 IN:(i 1 ^ x = 0 ^ y = z + i ^ i y i + 1)ig The above expression involves a quanti er over a new natural-number variable i. Thus, a simple heuristic to guess the reachable region is to observe a few iterations of reachability construction, and to search for a reachable region of the form 9i1 2 IN : : : 9iq 2 IN:R(i1 ; : : : ; iq ); that is, the reachable region involves some new natural-number variables i1 ; : : : ; iq in addition to the automaton variables. A typical situation is to guess a reachable region written using only one natural-number variable j , which represents the number of iterations of the Post procedure. In this case, we call the guessed region directly inductive, and proving that the guess is correct amounts to prove that for all j 2 IN , Postj (I ) = R(j ). This can be performed by induction using a theorem prover. In particular, we ~ need to show the two following proof obligations: R(0) = fInit (l )l ^ Inv (l ) j l 2 Lg for the base step, and 8j 2 IN:Post (R(j )) = R(j + 1) for the induction step. As we shall see in Section 3, these proof obligations can often be discharged automatically. In other situations the guessed region may not be directly inductive, but it can be made so by introducing new variables and constraints. For instance, the reachable region de ned by expression (3) is not directly inductive, since the natural-number variable i does not represent the number of iterations. But this region becomes directly inductive by adding the constraints j = 3i, j = 3i + 1, and j = 3i + 2 respectively to the three regions in the set (3). That is, we de ne the sets of regions R(j ) = fhs1 ; 9i 2 IN:(j = 3i ^ i 1 ^ x i ^ y = i ^ z = 1)i; hs2 ; 9i 2 IN:(j = 3i + 1 ^ i 1 ^ x i ^ y = i ^ z = 1)i; hs3; 9i 2 IN:(j = 3i + 2^ i 1 ^ x = 0 ^ y = z + i ^ i y i + 1)ig and now the \guess" 9j 2 IN:R(j ) is directly inductive, with j representing the number of iterations. Finally, even in situations when the guess is not (or cannot be transformed into) directly inductive, a useful approach is to prove that it is an invariant of the system. This can often be done automatically and it is often enough in practice for proving safety properties. We present sample proofs in Section 4.

We now give a classi cation of hybrid automata according to the theory in which their reachable region can be written nitely. The less expressive this theory, the less interactive theorem proving is needed for doing reachability veri cation.

3 Reachable Region Classi cation

The rst class that we de ne contains in particular all the hybrid automata for which reachability construction terminates. De nition 3.1 (polyhedral hybrid automata). A linear hybrid automaton is polyhedral if its reachable region can be expressed as a set of pairs fhl; Pli j 2 Lg such that for each location l 2 L, Pl is a formula of the theory2 (IR; +; ). 2 We say a linear hybrid automaton is nitely constructible if its reachability construction terminates: i.e., for some k 2 IN , Post (I ) = Postk (I ). While all nitely constructible hybrid automata are polyhedral, the converse is not true: it is easy to construct a hybrid automaton such that for all k 2 IN , Postk (I ) is the closed interval 0; k]; thus, the reachable region Post (I ) is the interval 0; 1), but reachability construction does not converge in nitely many steps. The class of nitely constructible hybrid automata includes the timed automata AD94] and the initialized rectangular hybrid automata HKPV95] (with some minor modi cations to force the reachability construction to terminate) as well as some other restricted classes KPSY93, RR96].

De nition 3.2 (additive-inductive hybrid automata). A linear hybrid automaton is additive-inductive if its reachable region can be expressed as a set of pairs fhl; Pl i j l 2 Lg such that for each location l 2 L, Pl is a formula of the theory (IR; IN; +; ) in which all natural-number variables are outermost existentially quanti ed. 2

For instance, the hybrid automaton in Figure 1 is additive-inductive: we have seen that its reachable region (3) involves the real variables x; y; z and the natural-number variable i, which is outermost existentially quanti ed.

Proposition 3.3. The class of polyhedral hybrid automata is strictly included

in the class of additive-inductive hybrid automata. Proof. The inclusion is obvious (since any formula of (IR; +; ) is also a formula of (IR; IN; +; )). Let us show that the inclusion is strict. For this, consider the hybrid automaton in Figure 1. We have seen that it is additive-inductive, and let us suppose it is nitely constructible, thus polyhedral by a previous observation. Then, formula (4) 9i 2 IN:(i 1 ^ x i ^ y = i ^ z = 1) can be also expressed in the theory (IR; +; ); that is, the set of triples (x; y; z ) satisfying (4) constitute a nite union of convex polyhedra P1 ; : : : ; PN in IR3 . Since (4) is the countably 2 Whenever we de ne a logical theory, we allow (unless explicitly restricted) arbitrary rst-order quanti cation and boolean connectives.

in nite union i2I (i 1 ^ x i ^ y = i ^ z = 1), it follows that at least one of N the convex polyhedra Pj coincides with the union of in nitely many polyhedra of the form (5) (x i ^ y = i ^ z = 1). This is not possible, because the union of polyhedra of the form (5) is not convex (they are all disjoint). 2 Suppose the user can guess a reachable region like in De nition 3.2 (using the simple heuristic of extrapolating from the rst few reachability steps) and that furthermore the guess is directly inductive (cf. end of Section 2). Then, verifying that the guess is correct can be done by induction in a completely automatic manner. Indeed, both the base and the inductive steps of the proof require computing the extension and projection operations (cf. equations (1), (2) of Section 2) for formulas of the theory (IR; IN; +; ). This amounts to proving nitely many implications of the form 8x 2 IRn :8i 2 IN m :9y 2 IR:'(x; i; y) ) (x; i; y). Proving such an implication can be done automatically, by eliminating the existential quanti ers on the real variables using the Fourier-Motzkin algorithm Zie95] (transforming the universal quanti ers into existential ones by taking the negation of the formula whenever necessary). At the end we are left with a formula of Presburger arithmetic, which is decidable. In the situation where the guessed region is not directly inductive, one can still attempt make it directly inductive as indicated in Section 2, by introducing new variables (one of which represents the iteration number) and new constraints connecting the existing and the new variables. Finally, even when a guess is not directly inductive, it can be useful (as an invariant of the system) to prove safety properties. We demonstrate these approaches in Section 4 on some well-known examples. We now de ne a class of linear hybrid automata whose reachable region can be de ned in terms of natural and real numbers, using addition and multiplication. Consider the theory (IR; IN; +; I I ; I I ; ) of reals and naturals N N N R with multiplication between naturals I I , multiplication between naturals and N N reals I I , and inequality. Any formula in this theory is a boolean combination N R of linear inequalities in the real variables, with polynomial coe cients in the natural-number variables; for example, (n3 ? 1) x + m y + n 0, where x; y are real variables and m; n are natural-number variables.

W

De nition 3.4 (multiplicative-inductive hybrid automata). A linear hybrid automaton is multiplicative-inductive if its reachable region can be expressed as a set of pairs fhl; Pli j l 2 Lg such that for all location l 2 L, Pl is a formula

of the theory (IR; IN; +; I I ; I I ; ) with all the natural-number variables N N N R outermost existentially quanti ed. 2 The linear hybrid automaton3 in Figure 2 is multiplicative inductive: it can be shown easily that the reachable region at location s1 is de ned by the formula (6) 9n 2 IN:(n 1 ^ x = 1 ^ n y = 1 ^ v = 0 ^ u = 0), where x; y; u; v are real variables, and n is a natural-number variable.

3 In Figure 2, activities x = y = u = v = 0 at all locations are not represented. _ _ _ _

u

v

? 1 := + 1 := +

;u u ;x x s

y

s

1

x u

= := 0

y

2

u

u

= ^ =1 := 0 := 0

v x ;v

s

3

included in the class of multiplicative-inductive hybrid automata. Proof. The proof of this proposition is based on the following observations. Given two predicates ' and on the real variables x1 ; : : : ; xn , we identify ' and with the sets of points in IRn that they respectively de ne. We de ne the maximal distance ('; ) between ' and as follows: if ' or are empty then ('; ) is a special value ?; otherwise, ('; ) is the lowest upper bound of the set of distances in IRn between a point satisfying ' and a point satisfying . Consider now an additive-inductive hybrid automaton, a location l of the automaton, and the formula 9i1 2 IN : : : 9iq 2 IN:'(x1 ; : : : xn ; i1 : : : iq ) that de nes the reachable region of the automaton at location l. Without restricting the generality, it is possible to suppose that formula ' is a convex linear predicate in variables x1 ; : : : ; xn ; i1 ; : : : ; iq . We de ne a sequence ('m )m 1 of linear predicates by the relation 'm (x1 ; : : : ; xn ) = '(x1 ; : : : xn ; m : : : ; m); i.e., the sequence of predicates ('m )m 1 is obtained by replacing in formula ' all integer variables by the value m. Thus, any predicate in the sequence ('m )m 1 is a convex linear predicate on x1 ; : : : ; xn ; that is, any predicate 'm is a convex polyhedron in IRn . We now de ne the sequence ( m )m 1 by m = ('m ; 'm+1 ) for all m 1. We show that the sequence ( m )m 1 can behave in one of three possible manners. In the rst case, there are in nitely many polyhedra 'm that are empty and thus for in nitely many m 1, m =?. Otherwise, there exists an index M 1 such that for all m M , all polyhedra 'm are non-empty. Then it can be shown that for all m M , each vertex of 'm+1 is obtained from some vertex of 'm by translation by some constant vector w 2 IRn . The vector w depends on the vertex but not on the index m. If all such vectors w are 0, then we have the second case: for all m M , the polyhedra 'm are equal, and hence the sequence ( m )m M is constant. Otherwise, at least one vector w is not 0 and we have the third case: for all m M , m jwj > 0 (where jwj denotes the length of vector w). Consider now the hybrid automaton in Figure 2 and suppose that it is additive-inductive. We have seen that the formula (6) 9i 2 IN:(i 1 ^ x = 1 ^ i y = 1 ^ v = 0 ^ u = 0) represents the reachable region of this hybrid automaton at location s3 . We apply the previous constructions: we obtain the sequence of predicates 'm = (x = 1 ^ m y = 1 ^ v = 0 ^ u = 0) and the sequence of distances m = 1=m(m + 1), for all m 1. The last sequence is strictly decreasing and converges to 0. But we have seen that this cannot be the case for a sequence ( m )m 1 obtained (as described above) from the reachable region of an additive-inductive hybrid automaton. Hence, the multiplicative-inductive hybrid automaton in Figure 2 is not additive-inductive. 2

Figure 2. Multiplicative-inductive hybrid automaton Proposition 3.5. The class of additive-inductive hybrid automata is strictly

Reachability veri cation can still be applied to multiplicative-inductive hybrid automata, provided the user guesses the reachable region. For instance, consider the hybrid automaton in Figure 2, whose initial region I is de ned by location s1 . We apply reachability veri cation: we guess the reachable region at location s3 to be formula (6) above (using the heuristic of observing the rst steps of reachability construction). This guess is furthermore directly inductive (cf. end of Section 2): to prove that the guess is correct, we show by induction that for all k 1, the region Postk (I ) at location s3 is described by the formula (x = 1 ^ k y = 1 ^ v = 0 ^ u = 0). However, unlike the case of additiveinductive hybrid automata, this proof can only be partially automated. Indeed, the extension and projection operations (equations (1), (2) of Section 2) can be computed automatically for predicates in (IR; IN; +; I I ; I I ): these operN N N R ations require eliminating the existential quanti ers on the real variables, which can be done using a generalization of the Fourier-Motzkin algorithm BR97]. But after the quanti er elimination, we are left to decide a rst-order formula of the (undecidable) theory (IN; +; ; ). This last formula has to be dealt with by theorem proving. So, the veri cation process is more involved than in the case of additive-inductive hybrid automata.

x = 1; y = 0

x := 3x ? 4y y := 4x + 3y

Figure 3. Hybrid automaton with exponential/trigonometric reachable region

While the theory of natural numbers with addition, multiplication and order is extremely expressive for encoding purposes, there exist linear hybrid automata whose reachable regions are most naturally expressed in terms of other operations, like exponentials and trigonometric functions. Consider the hybrid automaton in Figure 3. The transition sets the variables to new values4 that we denote x0 ; y0 . Let 2 IR be such that 5 cos = 3. Then, we have x0 = 5(x cos ? y sin ); y0 = 5(x sin + y cos ). Interpreted as a vector operation, the previous relations just say that vector x0 ; y0] has a length 5 times greater than vector x; y], and that x0 ; y0 ] is rotated by angle from x; y]. Thus, the reachable region is de ned by formula 9n 2 IN:9 2 IR:(x = 5n cos n ^ y = 5n sin n ^ 5 cos = 3). This would suggest that reachable regions need quite expressive theories in order to be expressed nitely. However, it is easy to show that the previous region can be encoded in the rst-order theory of integers with multiplication: let code(x; y) be an encoding function of pairs of integers as natural numbers, and consider the natural numbers of the form (7): 2code(x1;y1 ) 3code(x2;y2 ) : : : pcode(xn;yn) . Here, n pn is the n-th prime number, and xn , yn are the terms of the sequence de ned by x1 = 1; y1 = 0, and the transition relation of the automaton. Clearly, the fact that (xn ; yn ) is in the reachable region is encoded by the existence of natural numbers of the form (7), which can be described in the theory (IN; +; ; ).

4 The linear assignments can be simulated by appropriate slopes, tests, and resets.

Finally, we mention a restricted subclass of linear hybrid automata for which the reachable region can be computed algorithmically, even though reachability construction does not necessarily terminate. Some well-known examples of hybrid automata (like the ones we discuss in Section 4) are in this class. We say a hybrid automaton is time-predictable if for each location l0 and each pair of transitions (l; l0) and (l; l00 ) with destination (resp. with origin) l, there exists an interval of IR+ such that transition (s0 ; s00 ) can be red at any moment within the given interval, after the ring of transition (s; s0 ). We say a hybrid automaton is without nested cycles if its graph is equivalent to a regular expression (on the transition names) without nested operations. We have proved5 that time-predictable hybrid automata without nested cycles are additive-inductive but not polyhedral (cf. De nitions 3.1, 3.2), and that their reachable region can be computed algorithmically, by a procedure di erent from reachability construction. This shows that there exist hybrid automata for which the reachability problem is decidable, even though reachability construction does not terminate.

4 Hybrid Automata in PVS

Pvs ORR+ 96]. First we specify a theory polyhedra n] of n-dimensional polyhedra (parametric in the dimension n 2 IN ). It contains essentially the de niWe outline the modeling of hybrid automata and reachability veri cation in tions of extension, projection (formulas (1), (2) of Section 2), and intersection operations on polyhedra. Writing such rst-order predicates in the higher-order Pvs speci cation language is straightforward. Then, we write another theory that is speci c to the particular hybrid automaton to be analyzed (containing the de nition of the automaton features: states, transitions, activities, invariants, guards, and resets). This second theory uses (imports) the theory polyhedra n], instantiating n with the number of variables of the hybrid automaton. Finally, in a third theory called symbolic-analysis we specify the types and operations of reachability analysis (independent of any particular hybrid automaton): the region type (record of state and polyhedron), the continuous and discrete successors of a region, and a post predicate on regions, according to the de nition of the Post operation (cf. Section 2):

region : TYPE = # thestate: state, thepoly: poly #]

continuous(r1:region) : region = (# thestate:= thestate(r1), thepoly:= intersection(extend(thepoly(r1), slope(thestate(r1))),invar(thestate(r1))) #)

5 The proof is not presented here due to lack of space.

discrete (r1:region, t:trans) : region = (# thestate := dest(t), thepoly:= intersection(project(reset(t), intersection(thepoly(r1),guard(t))), invar(dest(t))) #) post(R1,R2:setof region]) : bool = FORALL (r2:region): member (r2,R2) IMPLIES EXISTS(r1:region,t:trans): member(r1,R1) AND orig(t)=thestate(r1) AND r2 = continuous(discrete(r1,t))

To prove statements about the reachable region Post (I ), we use induction and the predicate post. We now describe the application of reachability veri cation to examples of hybrid systems modeled by additive-inductive hybrid automata.

The leaking gas burner. The hybrid automaton in Figure 4 models a leaking

gas burner CHR91]: location s1 (resp. s2 ) stands for the leaking (resp. the nonleaking) state of the system; variable x is used to control the time spent in each state, variable y is a global clock, and variable z measures the total time spent by the gas burner in the leaking state. A design requirement for the leaking

x; y; z

1 := 0 __ = 1 =1 _=1

x x y z

s

1

x x x x

1 := 0 30 := 0

s

2

x y z

__ = 1 =1 _=0

true

Figure 4. Leaking gas burner automaton

gas burner is that in any interval of time of at least 60 seconds, the leaking time does not exceed 5% of the total time. This can be expressed by the fact that linear predicate y 60 ) 20z y is an invariant of the system (i.e., true in all reachable states). The speci cation in Pvs of this example includes the theories polyhedra n] with n instantiated by 3 (the number of variables of the automaton), and symbolic-analysis for the reachability analysis of the system. The system itself (hybrid automaton in Figure 4) is speci ed in a theory leaking-gas-burner, that contains the description of the automaton: locations with invariants and di erential laws, and transitions called s1_to_s2 and s2_to_s1, with their guards and variables to reset. The reachability construction does not terminate6 but by studying the rst few iterations, one can guess

6 Although backwards reachability construction terminates in this case.

that the reachable region is described by the following set of linear regions (from which it can be seen that the hybrid automaton is additive-inductive): fhs1 ; 0 x 1^x = y = z _9i 2 IN:(i 1^0 x 1^0 z ?x i^30i+z y)i, hs2 ; 0 z 1^y = x+z ^x 0_9i 2 IN:(i 1^0 x^0 z i+1^30i+x+z y)ig However, this guess is not directly inductive (cf. end of Section 2) because the natural-number variable i does not represent the number of iterations. It is possible to make the guess directly inductive, by introducing a new naturalnumber variable j and two new constraints j = 2i, j = 2i + 1. More precisely, we de ne the sets of regions R(j ) such that for all j 2, R(j ) is equal to: fhs1 ; 9i 2 IN:(i 1 ^ j = 2i ^ 0 x 1 ^ 0 z ? x i ^ 30i + z y)i, hs2 ; 9i 2 IN:(i 1 ^ j = 2i + 1 ^ 0 x ^ 0 z i + 1 ^ 30i + x + z y)ig Furthermore, R(0) equals fhs1 ; 0 x 1 ^ x = y = z i; hs2 ; falseig and R(1) equals fhs1 ; falsei; hs2; 0 z 1 ^ y = x + z ^ x 0ig. Now, the new \guess" 9j 2 IN:R(j ) is directly inductive (with j representing the number of iterations). We prove by induction on j that Postj (I ) = R(j ), for all j 2 IN . This means that Post (I ) = 9j 2 IN:R(j ); i.e., the guess of the reachable region is correct. Finally, to prove the design requirement of the gas burner y 60 ) 20z y, we prove that it is implied by Post (I ). Except for some details (like the expansions of the de nitions for continuous, discrete, post etc), Pvs can do all the proofs automatically, using its built-in decision procedures.

The reactor temperature controller. This example is taken from JLHM91].

It is a variant of the nuclear reactor temperature control problem, in which non-linear evolutions are approximated by piecewise-linear functions HHWT98]. The reactor automaton (cf. Figure 5) has three locations: in the no rod location,

x x y

510 _ 2 ?5 ?1] _1 = _2 = 1

; y

rod

1

x y

x y

= 510 1 := 0 = 550 1 20

no rod x

x y

550 _ 2 1 5] _1 = _2 = 1

; y

x y y

x

= 510 2 := 0 = 550 2 20

x x y

510 _ 2 ?9 ?5] _1 = _2 = 1

; y

rod

2

Figure 5. Reactor temperature control automaton

the temperature x increases according to the law x 2 1; 5], and control can stay _ in location no rod as long as the temperature does not exceed 550. When the temperature reaches 550, the reactor uses one of two cooling rods, and the control goes to a location where temperature decreases, according to law x 2 ?5; ?1] or _ x 2 ?9; ?5], depending on the cooling rod that is used. When the temperature _ falls to 510, the rod is removed and the reactor goes back to the no rod location. After a rod has been used, it cannot be used again before 20 time units. This is speci ed using two clocks y1 and y2 : when the control leaves the location rodi (that is, rod i is removed from the reactor) the clock variable yi is reset, and the next entry to location rodi is guarded by the condition yi 20. A design

requirement for the temperature control system is that the temperature never reaches the upper limit (x = 550) in the no rod location of the automaton with both rods unavailable (y1 < 20 and y2 < 20). The reachability construction from the initial region (location no rod, variables x = 510, y1 = y2 = 20) does not terminate. However, the reachable region behaves in a regular manner; by studying the output of the model checker HyTech, it can be guessed that the reachable region for location no rod (the location that interests us) has the form: (x 550) ^ (y1 = y2 ^ x y1 + 490 ^ x 5y1 + 410) _ 9i 2 IN:(x y1 +510 ^ x 5y1 +510 ^ y2 y1 +36+28i ^ y2 y1 +100+80i) _ 9i 2 IN:(x y1 +510 ^ x 5y1 +510 ^ y2 y1 +16+28i ^ y2 y1 +80(1+ i)) _ 9i 2 IN:(x y2 +510^x 5y2 +510^9y1 9y2 +112+220i^y1 y2 +48(i+2))_ 9i 2 IN:(x y2 +510 ^ x 5y2 +510 ^ 9y1 9y2 +292+220i ^ y1 y2 +68+48i)]. We prove in Pvs that the above predicate is an invariant at location no rod of the automaton. For this, we show that our guess R satis es I R and Post (R) R. This is enough for proving the design requirement: indeed, the above predicate implies the negation of the `dangerous' region x = 550 ^ y1 < 20 ^ y2 < 20, so the design requirement is met. Except for details like de nition expansion, these proofs are completely automatic in Pvs.

5 Conclusion

We have presented a new approach to the reachability problem of hybrid automata. The idea is to guess the form of the reachable region and to use theorem proving for verifying that the guess is correct. We have classi ed hybrid automata according to the theory in which their reachable region can be written nitely. In this classi cation, we have identi ed the additive-inductive and multiplicative-inductive hybrid automata, for which the guess can be done using a simple heuristic and the veri cation by induction. We have presented some applications using the prover Pvs. In the future, we plan to automate the method as much as possible (including automated guess heuristics and adapted strategies for the Pvs proofs) for being able to cope with larger examples. Related work. BW94] exploit the regularity of cycles on a discrete model (automata with counters). Their approach is fully automatic but it is limited to linear operations on the variables that are idempotent. BBR97] present a similar approach for a restricted class of hybrid automata (there is a xed interval of time between transitions), but their method is fully automatic. Abstract interpretation of hybrid automata HPR94] would automatically recognize the regularities of polyhedra and detect an invariant which, in general, is only an over-approximation of the actually reachable states. Finally, VH96] describe an approach based on stepwise re nement for the veri cation of hybrid systems, where Pvs is used to prove the correctness of each re nement step. Acknowledgments. Thanks to Natarajan Shankar, Luca de Alfaro, Peter Habermehl, and the anonymous reviewers of the Hybrid Systems workshop for useful comments and suggestions.

ACH+95. R. Alur, C. Courcoubetis, N. Halbwachs, T.A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138:3{34, 1995. AD94. R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 126:183{235, 1994. AHH96. R. Alur, T.A. Henzinger, and P.-H. Ho. Automatic symbolic veri cation of embedded systems. IEEE Transactions on Software Engineering, 22(3):181{201, 1996. BBR97. B. Boigelot, L. Bronne, and S. Rassart. An improved reachability analysis method for strongly linear hybrid systems. In Proc. of the 9th Conference on Computer-Aided Veri cation, CAV'97, LNCS 1254, pages 167{178. Springer-Verlag, 1997. BR97. A. Burgue~o and V. Rusu. Task-system analysis using slope-parametric n hybrid automata. In Proc. of the 3rd Conference on Parallel Processing, Euro-Par'97, LNCS 1300, pages 1262{1273. Springer-Verlag, 1997. BW94. B. Boigelot and P. Wolper. Symbolic veri cation with periodic sets. In Proc. of the 6th Conference on Computer-Aided Veri cation, CAV'94, LNCS 818, pages 55{67. Springer-Verlag, 1994. CHR91. Z. Chaochen, C.A.R. Hoare, and A.P. Ravn. A calculus of durations. Information Processing Letters, 40:269{276, 1991. HHWT98. T.A. Henzinger, P.-H. Ho, and H. Wong-Toi. Algorithmic analysis of nonlinear hybrid systems. IEEE Transactions on Automatic Control, 1998. To appear. HKPV95. T.A. Henzinger, P.W. Kopke, A. Puri, and P. Varaiya. What's decidable about hybrid automata? In Proc. of the 27th Annual ACM Symposium on Theory of Computing, STOC'95, pages 373{382, 1995. HPR94. N. Halbwachs, Y.-E. Proy, and P. Raymond. Veri cation of linear hybrid systems by means of convex approximations. In Proc. of the 1st Static Analysis Symposium, SAS'94, LNCS 864, pages 223{237. Springer-Verlag, 1994. JLHM91. M. Ja e, N. Levenson, M. Heimdahl, and B. Melhart. Software requirements analysis for real-time process-control systems. IEEE Transactions on Software Engineering, 17(3):241{258, 1991. KPSY93. Y. Kesten, A. Pnueli, J. Sifakis, and S. Yovine. Integration graphs: a class of decidable hybrid systems. In Proc. of the 1st Workshop on Theory of Hybrid Systems, LNCS 736, pages 179{208. Springer-Verlag, 1993. ORR+96. S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M.K. Srivas. Pvs: Combining speci cation, proof checking, and model checking. In Proc. of the 8th Conference on Computer-Aided Veri cation, CAV '96, LNCS 1102, pages 411{414. Springer-Verlag, 1996. RR96. O. Roux and V. Rusu. Uniformity for the decidability of hybrid automata. In Proc. of the 3rd Static Analysis Symposium, SAS'96, LNCS 1145, pages 301{316. Springer-Verlag, 1996. VH96. Jan Vitt and Josef Hooman. Assertional speci cation and veri cation using Pvs of the steam boiler control system. In Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control, LNCS 1165, pages 453{472. Springer-Verlag, 1996. Zie95. G. M. Ziegler. Lectures on Polytopes, volume 152 of Graduate Texts in Mathematics. Springer-Verlag, 1995.

References

赞助商链接

- Pushdown Timed Automata a Binary Reachability Characterization and Safety Verification
- Hybrid Automata an algorithmic approach to the specification and verification of hybrid sys
- State Equivalences for Rectangular Hybrid Automata
- Uniformity for the decidability of hybrid automata
- Computing Approximating Automata for a Class of Linear Hybrid Systems
- Pushdown time automata a binary reachability characterization and safety verification
- A CSP Model for Hybrid Automata
- Improving Reachability Analysis of Hybrid Automata for Engine Control
- Hybrid Automata an algorithmic approach to the specification and verification of hybrid sys
- Reachability for Linear Hybrid Automata Using Iterative Relaxation Abstraction
- Constraints for continuous reachability in the verification of hybrid systems
- Hybrid cc, hybrid automata and program verification
- automata, a hybrid system for computational automata theory
- Numerical Simulation guided Lazy Abstraction Refinement for Nonlinear Hybrid Automata
- Symbolic reachability analysis of lazy linear hybrid automata

更多相关文章：
更多相关标签：