2 A Model for Hybrid Systems

The Algorithmic Analysis of Hybrid Systems

^

R.Alur y

C.Courcoub etis z

N. Halbwachs x

T.A.Henzinger {

P.-H.Ho x

X. Nicollin z

A. Olivero z

J. Sifakis z

S.Yovine z

Abstract

We present a general framework for the formal specication and algorithmic analysis of hybrid systems. A hybrid system consists of a discrete program with an analog environment. We model hybrid systems as nite automata equipped with variables that evolve continuously with time according to dynamical laws. For verication purposes, we restrict ourselves to linear hybrid systems, where all variables follow piecewise-linear trajectories. We provide decidability and undecidability results for classes of linear hybrid systems, and we show that standard program- analysis techniques can be adapted to linear hybrid systems. In particular, we consider symbolic model-checking and minimization procedures that are based on the reachability analysis of an innite state space. The procedures iteratively compute state sets that are denable as unions of convex polyhedra in multidimensional real space. We also present approximation techniques for dealing with systems for which the iterative procedures do not converge.

A preliminary version of this paper appeared in theProceedings of the 11th International Conference on Analysis and Optimization of Discrete Event Systems, Lecture Notes in Control and Information Sciences 199, Springer-Verlag, 1994, pp. 331{351, and an extended version appeared in Theoretical Computer Science ¹³⁸, 1995, pp. 3{34.

yAT&T Bell Laboratories, Murray Hill, NJ, U.S.A.

zUniversity of Crete and ICS, FORTH, Heraklion, Greece. Partially supported by Esprit-BRA 6021 REACT-P.

xVERIMAG-SPECTRE, Grenoble, France. VERIMAG is a joint laboratory of CNRS, INPG, UJF, and VERILOG S.A., associated with the institute IMAG. SPECTRE is an INRIA project. Partially supported by Esprit-BRA 6021 REACT-P.

{Computer Science Department, Cornell University, Ithaca, NY, U.S.A. Supported in part by the National Science

1 Introduction

A hybrid system consists of a discrete program with an analog environment. We assume that a run of a hybrid system is a sequence of steps. Within each step the system state evolves continuously according to a dynamical law until a transition occurs. Transitions are instantaneous state changes that separate continuous state evolutions.

We model a hybrid system as a nite automaton that is equipped with a set of variables. The control locations of the automaton are labeled with evolution laws. At a location the values of the variables change continuously with time according to the associated law. The transitions of the automaton are labeled with guarded sets of assignments. A transition is enabled when the associated guard is true, and its execution modies the values of the variables according to the assignments. Each location is also labeled with an invariant condition that must hold when the control resides at the location. This model for hybrid systems is inspired by the phase transition systems of [MMP92, NSY93], and can be viewed as a generalization of timed safety automata[AD94, HNSY94].

The purpose of this paper is to demonstrate that standard program-analysis techniques can be adapted to hybrid systems. For verication purposes we restrict ourselves to linear hybrid systems. In a linear hybrid system, for each variable the rate of change is constant|though this constant may vary from location to location|and the terms involved in the invariants, guards, and assignments are required to be linear. An interesting special case of a linear hybrid system is a timed automaton [AD94]. In a timed automaton each continuously changing variable is an accurate clock whose rate of change with time is always 1. Furthermore, in a timed automaton all terms involved in assignments are constants, and all invariants and guards only involve comparisons of clock values with constants. Even though the reachability problem for linear hybrid systems is undecidable, it can be solved for timed automata. In this paper, we provide new decidability and undecidability results for classes of linear hybrid systems, and we show that some algorithms for the analysis of timed automata can be extended to linear hybrid systems to obtain semidecision procedures for various verication problems.

In particular, we consider the symbolic model-checking method for timed automata presented in [HNSY94], and the minimization procedure for timed automata presented in [ACD⁺92]. Both methods perform a reachability analysis over an innite state space. The procedures compute state sets by iterative approximation such that each intermediate result is denable by a linear formula;

that is, each computed state set is a nite union of convex polyhedra in multidimensional real space. The termination of the procedures, however, is not guaranteed for linear hybrid systems.

To cope with this problem, approximate analysis techniques are used to enforce the convergence of iterations by computing upper approximations of state sets. Approximate techniques yield either necessary or sucient verication conditions.

The paper is essentially a synthesis of the results presented in [ACHH93, NOSY93, HPR94].

Section 2 presents a general model for hybrid systems. Section 3 denes linear hybrid systems, and presents decidability and undecidability results for the reachability problem of subclasses of linear hybrid systems. The verication methods are presented in Section 4. Some paradigmatic examples are specied and veried to illustrate the application of our results. These examples are analyzed using the ^Kronos tool [NSY92, NOSY93] (available from Grenoble) and the ^HyTech tool [AHH93, HH94] (available from Cornell), two symbolic model checkers for timed and hybrid systems.

2 A Model for Hybrid Systems

We specify hybrid systems by graphs whose edges represent discrete transitions and whose vertices represent continuous activities.

A hybrid system

H

= (Loc

;

Var

;

Lab

;

Edg

;Act;

Inv) consists of six components:

 A nite set Loc of vertices called locations.

 A nite set Var of real-valued variables. A valuation



for the variables is a function that assigns a real-value



(

x

)²R to each variable

x

²Var. We write

V

for the set of valuations.

A state is a pair (

`;

) consisting of a location

`

²Loc and a valuation



²

V

. We write  for the set of states.

 A nite set Lab of synchronization labels that contains the stutter label



²Lab.

 A nite set Edg of edges called transitions. Each transition

e

= (

`;a;;`

⁰) consists of a source location

`

²Loc, a target location

`

⁰²Loc, a synchronization label

a

²Lab, and a transition relation



^

V

². We require that for each location

`

² Loc, there is a set Con ^ Var of controlled variables and a stutter transition of the form (

`;;

Id^Con

;`

), where (

;

⁰)²Id^Con i for all variables

x

²Var, either

x

⁶²Con or



(

x

) =



⁰(

x

).

The transition

e

is enabled in a state (

`;

) if for some valuation



^{0 2}

V

, (

;

⁰) ²



. The state (

`

⁰

;

⁰), then, is a transition successor of the state (

`;

).

 A labeling function

Act

that assigns to each location

`

²Loca set of activities. Each activity is a function from the nonnegative reals R^0 to

V

. We require that the activities of each location are time-invariant: for all locations

`

²Loc, activities

f

²

Act

(

`

), and nonnegative reals

t

²R^0, also (

f

+

t

) ²

Act

(

`

), where (

f

+

t

)(

t

⁰) =

f

(

t

+

t

⁰) for all

t

⁰²R^0.

For all locations

`

² Loc, activities

f

²

Act

(

`

), and variables

x

² Var, we write

f

^x the function from R^0 to R such that

f

^x(

t

) =

f

(

t

)(

x

).

 A labeling function Inv that assigns to each location

`

²Loc an invariant Inv(

`

)^

V

. The hybrid system

H

is time-deterministic if for every location

`

² Loc and every valuation



²

V

, there is at most one activity

f

²

Act

(

`

) with

f

(0) =



. The activity

f

, then, is denoted by

'

`[



].

The runs of a hybrid system

At any time instant, the state of a hybrid system is given by a control location and values for all variables. The state can change in two ways:

 By a discrete and instantaneous transition that changes both the control location and the values of the variables according to the transition relation;

 By a time delay that changes only the values of the variables according to the activities of the current location.

The system may stay at a location only if the location invariant is true; that is, some discrete transition must be taken before the invariant becomes false.

A run of the hybrid system

H

, then, is a nite or innite sequence



:



^{0 7!t}_f⁰0



^{1 7!t}_f¹1



^{2 7!t}_f²2

of states



i = (

`

i

;

i) ², nonnegative reals

t

i ²R^0, and activities

f

i ²

Act

(

`

i), such that for all

i

^0,

1.

f

i(0) =



i,

2. for all 0^

t

^

t

i,

f

i(

t

)²Inv(

`

i),

3. the state



i⁺¹ is a transition successor of the state



⁰_i= (

`

i

;f

i(

t

i)).

The state



⁰_i is called a time successor of the state



i; the state



i⁺¹, a successor of



i. We write [

H

] for the set of runs of the hybrid system

H

.

Notice that if we require all activities to be smooth functions, then the run



can be described by a piecewise smooth function whose values at the points of higher-order discontinuity are sequences of discrete state changes. Also notice that for time-deterministic systems, we can omit the subscripts

f

i from the next relation ^7!.

The run



diverges if



is innite and the innite sum^P_i^0

t

i diverges. The hybrid system

H

is nonzeno if every nite run of

H

is a prex of some divergent run of

H

. Nonzeno systems can be executed [AH94].

Hybrid systems as transition systems

With the hybrid system

H

, we associate the labeled transition system ^TH = (

;

Lab^[R^0

;

^!), where the step relation ^! is the union of the transition-step relations ^!a, for

a

²Lab,

(

`;a;;`

⁰)²Edg (

;

⁰)²

 ;

⁰²Inv(

`

) (

`;

)^!a(

`

⁰

;

⁰)

and the time-step relations ^!t, for

t

²R^0,

f

²

Act

(

`

)

f

(0) =



⁸0^

t

^0

t: f

(

t

⁰)²Inv(

`

) (

`;

)^!t(

`;f

(

t

))

Notice that the stutter transitions ensure that the transition system ^TH is re exive.

There is a natural correspondence between the runs of the hybrid system

H

and the paths through the transition system^TH: for all states

;

⁰², where



= (

`;

), and for all

t

²R^0,

9

f

²

Act

(

`

)

;

^7!_tf



⁰ i ⁹



^{00 2}

;a

²Lab

: 

^!t



^00!a



⁰

:

It follows that for every hybrid system, the set of runs is closed under prexes, suxes, stuttering, and fusion [HNSY94].

For time-deterministic hybrid systems, the rule for the time-step relation can be simplied.

Time can progress by the amount

t

²R^0 from the state (

`;

) if this is permitted by the invariant of location

`

; that is,

tcp_`[



](

t

) i ⁸0^

t

^0

t: '

`[



](

t

⁰)²Inv(

`

)

:

Now we can rewrite the time-step rule for time-deterministic systems as

tcp_`[



](

t

) (

`;

)^!t(

`;'

`[



](

t

))

Example: thermostat

The temperature of a room is controlled through a thermostat, which continuously senses the temperature and turns a heater on and o. The temperature is governed by dierential equations.

When the heater is o, the temperature, denoted by the variable

x

, decreases according to the exponential function

x

(

t

) =

e

^;Kt, where

t

is the time,



is the initial temperature, and

K

is a constant determined by the room; when the heater is on, the temperature follows the function

x

(

t

) =

e

^;Kt+

h

(1^;

e

^;Kt), where

h

is a constant that depends on the power of the heater. We wish to keep the temperature between

m

and

M

degrees and turn the heater on and o accordingly.

The resulting time-deterministic hybrid system is shown in Figure 1. The system has two locations: in location

`

⁰, the heater is turned o; in location

`

¹, the heater is on. The transition relations are specied by guarded commands; the activities, by dierential equations; and the location invariants, by logical formulas.

x

_ =^;

Kx

x

=

m

x

=

M x

=

M

`

¹

`

⁰

x

_ =

K

(

h

^;

x

)

x

^

M x

^

m

Figure 1: Thermostat

The parallel composition of hybrid systems

Let

H

¹ = (Loc¹

;

Var

;

Lab¹

;

Edg¹

;Act

¹

;

Inv¹) and

H

² = (Loc²

;

Var

;

Lab²

;

Edg²

;Act

²

;

Inv²) be two hybrid systems over a common set Var of variables. The two hybrid systems synchronize on the common set Lab^{1 \}Lab² of synchronization labels; that is, whenever

H

¹ performs a discrete transition with the synchronization label

a

²Lab^1\Lab², then so does

H

².

The product

H

^1

H

² is the hybrid system (Loc^1Loc²

;

Var

;

Lab^1[Lab²

;

Edg

;Act;

Inv) such that

 ((

`

¹

;`

²)

;a;;

(

`

⁰¹

;`

⁰²))²Edg i

(1) (

`

¹

;a

¹

;

¹

;`

⁰¹)²Edg¹ and (

`

²

;a

²

;

²

;`

⁰²)²Edg²,

(2) either

a

¹ =

a

² =

a

, or

a

^{1 62}Lab² and

a

²=



, or

a

¹ =



and

a

^{2 62}Lab¹, (3)



=



^1\



²;



Act

(

`

¹

;`

²) =

Act

¹(

`

¹)^\

Act

²(

`

²);

 Inv(

`

¹

;`

²) = Inv¹(

`

¹)^\Inv²(

`

²).

It follows that all runs of the product system are runs of both component systems:

[

H

^1

H

²]^{Loc1 } [

H

¹] and [

H

^1

H

²]^{Loc2 } [

H

²] where [

H H

] is the projection of [

H H

] on Loci.

3 Linear Hybrid Systems

A linear term over the set Var of variables is a linear combination of the variables in Var with integer coecients. A linear formula over Var is a boolean combination of inequalities between linear terms over Var.

The time-deterministic hybrid system

H

= (Loc

;

Var

;

Lab

;

Edg

;Act;

Inv) is linear if its activ- ities, invariants, and transition relations can be dened by linear expressions over the set Var of variables:

1. For all locations

`

²Loc, the activities

Act

(

`

) are dened by a set of dierential equations of the form _

x

=

k

x, one for each variable

x

²Var, where

k

x ²Z is an integer constant: for all valuations



²

V

, variables

x

²Var, and nonnegative reals

t

²R^0,

'

_x`[



](

t

) =



(

x

) +

k

x

t:

We write

Act

(

`;x

) =

k

x to refer to the rate of the variable

x

at location

`

.

2. For all locations

`

²Loc, the invariant Inv(

`

) is dened by a linear formula over Var:



²Inv(

`

) i



( )

:

3. For all transitions

e

²Edg, the transition relation



is dened by a guarded set of nondeter- ministic assignments

) f

x

:= [



x

;

x]^j

x

²Var^g

;

where the guard is a linear formula and for each variable

x

²Var, both interval boundaries



x and



x are linear terms:

(

;

⁰)²



i



( ) ^{^ 8}

x

²Var

: 

(



x)^



⁰(

x

)^



(



x)

:

If



x =



x, we write



(

e;x

) =



x to refer to the updated value of the variable

x

after the transition

e

.

Notice that every run of a linear hybrid system can be described by a piecewise linear function whose values at the points of rst-order discontinuity are nite sequences of discrete state changes.

Special cases of linear hybrid systems

Various special cases of linear hybrid systems are of particular interest:

 If

Act

(

`;x

) = 0 for each location

`

² Loc, then

x

is a discrete variable. Thus, a discrete variable changes only when the control location changes. A discrete system is a linear hybrid system all of whose variables are discrete.

 A discrete variable

x

is a proposition if



(

e;x

) ^{2 f}0

;

1^g for each transition

e

² Edg. A nite-state system is a linear hybrid system all of whose variables are propositions.

 If

Act

(

`;x

) = 1 for each location

`

and



(

e;x

)^2f0

;x

^gfor each transition

e

, then

x

is a clock.

Thus, (1) the value of a clock increases uniformly with time, and (2) a discrete transition either resets a clock to 0, or leaves it unchanged. A timed automaton [AD94] is a linear hybrid system all of whose variables are propositions or clocks, and the linear expressions are boolean combinations of inequalities of the form

x

#

c

or

x

^;

y

#

c

where

c

is a nonnegative integer and #^2f

<;

^

;

=

;>;

^g.

 If there is a nonzero integer constant

k

²Z such that

Act

(

`;x

) =

k

for each location

`

and



(

e;x

)^2f0

;x

^gfor each transition

e

, then

x

is a skewed clock. Thus, a skewed clock is similar to a clock except that it changes with time at some xed rate dierent from 1. A multirate timed system is a linear hybrid system all of whose variables are propositions and skewed clocks. An n-rate timed system is a multirate timed system whose skewed clocks proceed at

n

dierent rates.

 If

Act

(

`;x

)^2f0

;

1^gfor each location

`

and



(

e;x

)^2f0

;x

^gfor each transition

e

, then

x

is an integrator. Thus, an integrator is a clock that can be stopped and restarted; it is typically used to measure accumulated durations. An integrator system is a linear hybrid system all of whose variables are propositions and integrators.

 A discrete variable

x

is a parameter if



(

e;x

) =

x

for each transition

e

² Edg. Thus, a parameter is a symbolic constant. For each of the subclasses of linear hybrid systems listed above, we obtain parameterized versions by admitting parameters.

Notice that linear hybrid systems, and all of the subclasses of linear hybrid systems listed above, are closed under parallel composition.

3.1 Examples of Linear Hybrid Systems A water-level monitor

The water level in a tank is controlled through a monitor, which continuously senses the water level and turns a pump on and o. The water level changes as a piecewise-linear function over time.

When the pump is o, the water level, denoted by the variable

y

, falls by 2 inches per second; when the pump is on, the water level rises by 1 inch per second. Suppose that initially the water level is 1 inch and the pump is turned on. We wish to keep the water level between 1 and 12 inches.

But from the time that the monitor signals to change the status of the pump to the time that the change becomes eective, there is a delay of 2 seconds. Thus the monitor must signal to turn the pump on before the water level falls to 1 inch, and it must signal to turn the pump o before the water level reaches 12 inches.

The linear hybrid system of Figure 2 describes a water-level monitor that signals whenever the water level passes 5 and 10 inches, respectively. The system has four locations: in locations 0 and 1, the pump is turned on; in locations 2 and 3, the pump is o. The clock

x

is used to specify the delays: whenever the control is in location 1 or 3, the signal to switch the pump o or on, respectively, was sent

x

seconds ago. In the next section, we will prove that the monitor indeed keeps the water level between 1 and 12 inches.

A mutual-exclusion protocol

This example describes a parameterized multirate timed system. We present a timing-based algo- rithm that implements mutual exclusion for a distributed system with skewed clocks. Consider an asynchronous shared-memory system that consists of two processes

P

¹ and

P

² with atomic read and write operations. Each process has a critical section and at each time instant, at most one of the two processes is allowed to be in its critical section. Mutual exclusion is ensured by a version of Fischer's protocol [Lam87], which we describe rst in pseudocode. For each process

P

i, where

i

= 1

;

2:

y

= 10

x

:= 0

y

= 1

x

= 2

x

= 2

y

= 5

x

:= 0

x

_= 1

0

3

2

x

_ = 1

x

_ = 1

y

_= 1

y

_= 1

y

^10

x

^2

x

_ = 1

y

_=^;2

x

^2

y

_=^;2

y

^5 Figure 2: Water-level monitor

repeat repeat

await k

= 0

k

:=

i delay b until k

=

i

Critical section

k

:= 0

forever

The two processes

P

¹ and

P

² share a variable

k

and process

P

i is allowed to be in its critical section i

k

=

i

. Each process has a private clock. The instruction

delay b

delays a process for at least

b

time units as measured by the process's local clock. Furthermore, each process takes at most

a

time units, as measured by the process's clock, for a single write access to the shared memory (i.e., for the assignment

k

:=

i

). The values of

a

and

b

are the only information we have about the timing behavior of instructions. Clearly, the protocol ensures mutual exclusion only for certain values of

a

and

b

. If both private processor clocks proceed at precisely the same rate, then mutual exclusion is guaranteed i

a < b

.

To make the example more interesting, we assume that the two private clocks of the processes

P

¹ and

P

² proceed at dierent rates, namely, the local clock of

P

² is 1

:

1 times faster than the clock of

P

¹. The resulting system can be modeled by the product of the two hybrid systems presented in Figure 3.

Each of the two graphs models one process, with the two critical sections being represented by the locations 4 and

D

. The private clocks of the processes

P

¹ and

P

² determine the rate of change of the two skewed-clock variables

x

and

y

, respectively.

A leaking gas burner

Now we consider an integrator system. In [CHR91], the duration calculus is used to prove that a gas burner does not leak excessively. It is assumed that (1) any leakage can be detected and

1

2

3

4

x

_ = 1

x

_ = 1

x

_= 1

k

= 0

x

:= 0

x < a x k

:= 1:= 0

x > b

^{^}

k

⁶= 1

k

= 0

A

B

C

D

y

:= 0

y > b

^{^}

k

⁶= 2

k

:= 2

y < a

k

:= 0

k

:= 0

k

= 1

k

= 2^{^}

x > b

^

y

_= 1

:

1

y

_= 1

:

1

x

_ = 1

y

_ = 1

:

1

y

_ = 1

:

1

y > b

y

:= 0

Figure 3: Mutual-exclusion protocol

stopped within 1 second and (2) the gas burner will not leak for 30 seconds after a leakage has been stopped. We wish to prove that the accumulated time of leakage is at most one twentieth of the time in any interval of at least 60 seconds. The system is modeled by the hybrid system of Figure 4. The system has two locations: in location 1, the gas burner leaks; location 2 is the nonleaking location. The integrator

z

records the cumulative leakage time; that is, the accumulated amount of time that the system has spent in location 1. The clock

x

records the time the system has spent in the current location; it is used to specify the properties (1) and (2). The clock

y

records the total elapsed time. In the next section, we will prove that

y

^ 60 ⁾ 20

z

^

y

is an invariant of the system.

1

x

:= 0 2

x

^30

x

:= 0

x

= 0

z

= 0

y

= 0

x

_ = 1

y

_= 1

z

_= 1

x

^1

x

_ = 1

y

_= 1

z

_= 0 Figure 4: Leaking gas burner

A temperature control system

This example appears in [JLHM91]. The system controls the coolant temperature in a reactor tank by moving two independent control rods. The goal is to maintain the coolant between the temperatures



m and



M. When the temperature reaches its maximum value



M, the tank must be refrigerated with one of the rods. The temperature rises at a rate

v

r and decreases at rates

v

¹ and

v

² depending on which rod is being used. A rod can be moved again only if

T

time units have elapsed since the end of its previous movement. If the temperature of the coolant cannot decrease because there is no available rod, a complete shutdown is required. Figure 5 shows the hybrid system of this example: variable



measures the temperature, and the values of clocks

x

¹ and

x

² represent the times elapsed since the last use of rod 1 and rod 2, respectively.



=



M ^{^}

x

^{1 }

T

x 

¹=:= 0



m

shutdown x

^{2 }

T

x

²:= 0



=



m



=



M^{^}



=



M ^{^}

x

¹

< T

^{^}

x

²

< T x

¹=

T

x

²=

T

1

x

_² = 1



^



m

0

2 3



_=^;

v

²

x

_¹= 1

x

_² = 1



^



m



_=

v

r

x

_¹ = 1

x

_² = 1



^



M



_=^;

v

¹

x

_¹ = 1

Figure 5: Temperature control system

A game of billiards

Consider a billiard table of dimensions

l

and

h

, with a grey ball and a white ball (Figure 6).

Initially, the balls are placed at positions

b

g = (

x

g

;y

g) and

b

w = (

x

w

;y

w). The grey ball is knocked and starts moving with constant velocity

v

. If the ball reaches a vertical side then it rebounds, i.e., the sign of the horizontal velocity component

v

x changes. The same occurs with the vertical velocity component

v

y when the ball reaches a horizontal side. The combination of signs of velocity components gives four dierent directions of movement.

The hybrid system shown in Figure 7 describes the movement of the grey ball for the bil- liards game. Each possible combination of directions is represented by a location. The rebounds correspond to the execution of transitions between locations.

v

y

v

v

x

x

g

x

w

l x

h y

w

y

g

y

Figure 6: Billiards game

x

=

l

_ 1

x

=

v

x

x

^

l

^{^}

y

^

h

_ 2

x

=^;

v

x

y

_=

v

y

x

^0 ^{^}

y

^

h y

_=

v

y

y

= 0

y

=

h y

=

h y

= 0

3

y

_

x

_==^;

v

x

v

y

4

x

_=^;

v

x

x

= 0

x

^

l

^{^}

y

^0

x

^

y

_0=^{^;}

y v

y^0

x

=

x

g

y

=

y

g

x

=

l x

= 0

Figure 7: Movement of the grey ball

3.2 The Reachability Problem for Linear Hybrid Systems

Let



and



⁰be two states of a hybrid system

H

. The state



⁰is reachable from the state



, written



^7!



⁰, if there is a run of

H

that starts in



and ends in



⁰. The reachability question asks, then, if



^7!



⁰for two given states



and



⁰of a hybrid system

H

.

The reachability problem is central to the verication of hybrid systems. In particular, the verication of invariance properties is equivalent to the reachability question: a set

R

^ of states is an invariant of the hybrid system

H

i no state in ^;

R

is reachable from an initial state of

H

.

A decidability result

A linear hybrid system is simple if all linear atoms in location invariants and transition guards are of the form

x

^

k

or

k

^

x

, for a variable

x

²Var and an integer constant

k

²Z. In particular, for multirate timed systems the simplicity condition prohibits the comparison of skewed clocks with dierent rates.

Theorem 3.1

The reachability problem is decidable for simple multirate timed systems.

Proof.

Let

H

be a simple multirate timed system. We translate

H

into a timed automa- ton sc(

H

): (1) adjust the rates of all skewed clocks to 1, and (2) replace all occurrences of each skewed clock

x

in location invariants and transition guards with

k

x

x

. Given a valuation



of

H

, let the valuation sc(



) be such that sc(



)(

x

) =

k

x



(

x

) for all skewed clocks

x

and sc(



)(

p

) =



(

p

) for all propositions

p

; moreover, sc(

`;

) = (

`;

sc(



)). It is not dicult to check that there is a run of

H

from



to



⁰ i there is a run of sc(

H

) from sc(



) to sc(



⁰). The reachability problem for timed automata is solved in [ACD93].

Two undecidability results

Theorem 3.2

The reachability problem is undecidable for 2-rate timed systems.

Proof.

The theorem follows from the undecidability of the halting problem for nondeterministic 2-counter machines. Given any two distinct clock rates, a 2-rate timed system can encode the computations of the given 2-counter machine

M

. For the 2-rate timed system

H

, we use \accurate"

clocks of rate 1 and skewed clocks of rate 2. We use an accurate clock

y

to mark intervals of length 1: the clock

y

is zero initially, and is reset whenever it reaches 1. The

i

-th conguration of the machine

M

is encoded by the state of

H

at time

i

. The location of

H

encodes the program counter of

M

, and the values of two accurate clocks

x

¹ and

x

² encode the counter values: the counter value

n

is encoded by the clock value 1

=

2ⁿ.

Encoding the program counter, setting up the initial conguration, and testing a counter for being 0, is straightforward. Hence it remains to be shown how to update the counter values.

Suppose at time

i

the value of an accurate clock

x

is 1

=

2ⁿ, that is, suppose that the clock

x

is reset to 0 at time

i

^;1

=

2ⁿ. Suppose the value of the counter encoded by

x

stays unchanged. Then simply reset

x

to 0 when its value reaches 1 (that is, at time (

i

+ 1^;1

=

2ⁿ)); the value of

x

at time

i

+ 1 will then be 1

=

2ⁿ. To increment the counter represented by

x

, reset an accurate clock

z

when the value of

x

reaches 1, then nondeterministically reset both

x

and a skewed clock

z

⁰in the interval (

i

+ 1^;1

=

2ⁿ

;i

+ 1) and test

z

=

z

⁰ at time

i

+ 1. The equality test ensures that the value of the skewed clock

z

⁰ is 1

=

2ⁿ at time

i

+ 1, and hence, the value of

x

is 1

=

2ⁿ⁺¹ at time

i

+ 1.

To decrement the counter represented by

x

, nondeterministically reset an accurate clock

z

in the interval (

i

^;1

;i

^;1

=

2ⁿ), reset a skewed clock

z

⁰ simultaneously with

x

at time

i

^;1

=

2ⁿ, and test

the condition

z

=

z

⁰at time

i

. This ensures that the value of

z

at time

i

is 1

=

2^n;1. Then resetting the clock

x

when the value of

z

reaches 1 ensures that the value of

x

is 1

=

2^n;1 at time

i

+ 1.

Thus, the runs of

H

encode the runs of

M

, and the halting problem for

M

is reduced to a reachability problem for

H

.

Theorem 3.3

The reachability problem is undecidable for simple integrator systems.

Proof.

This is proved in [Cer92].

4 The Verication of Linear Hybrid Systems

We present a methodology for analyzing linear hybrid systems that is based on predicate transform- ers for computing the step predecessors and the step successors of a given set of states. Throughout this section, let

H

= (Loc

;

Var

;

Lab

;

Edg

;Act;

Inv) be a linear hybrid system.

4.1 Forward Analysis

Given a location

`

²Loc and a set of valuations

P

^

V

, the forward time closure ^h

P

^i%_` of

P

at

`

is the set of valuations that are reachable from some valuation



²

P

by letting time progress:



^02h

P

^i%_` i ⁹



²

V;t

²R^0

: 

²

P

^{^} tcp_`[



](

t

) ^{^}



⁰=

'

`[



](

t

)

:

Thus, for all valuations



^{0 2h}

P

^i%_` , there exist a valuation



²

P

and a nonnegative real

t

²R^0 such that (

`;

)^!t(

`;

⁰).

Given a transition

e

= (

`;a;;`

⁰) and a set of valuations

P

^

V

, the postcondition post_e[

P

] of

P

with respect to

e

is the set of valuations that are reachable from some valuation



²

P

by executing the transition

e

:



⁰²post_e[

P

] i ⁹



²

V: 

²

P

^{^} (

;

⁰)²

:

Thus, for all valuations



⁰²post_e[

P

], there exists a valuation



²

P

such that (

`;

)^!a(

`

⁰

;

⁰).

A set of states is called a region. Given a set

P

^

V

of valuations, by (

`;P

) we denote the region

f(

`;

)^j



²

P

^g; we write (

`;

)²(

`;P

) i



²

P

. The forward time closure and the postcondition can be naturally extended to regions: for

R

=^S_`^2Loc(

`;R

`),

h

R

^i% = ^[

`^2Loc(

`;

^h

R

`<sup>i%</sup>` ) post[

R

] = ^[

e⁼⁽`;`^0)2Edg(

`

⁰

;

post_e[

R

`])

A symbolic run of the linear hybrid system

H

is a nite or innite sequence

%

: (

`

⁰

;P

⁰)(

`

¹

;P

¹)

:::

(

`

i

;P

i)

:::

of regions such that for all

i

^0, there exists a transition

e

i from

`

i to

`

i⁺¹ and

P

i⁺¹ = post_eⁱ[^h

P

i^i%`ⁱ];

that is, the region (

` ;P

) is the set of states that are reachable from a state (

` ;

) (

` ;P

)

the runs and the symbolic runs of the linear hybrid system

H

. The symbolic run

%

represents the set of all runs of the form

(

`

⁰

;

⁰)^7!t0 (

`

¹

;

¹)^7!t1

such that (

`

i

;

i) ²(

`

i

;P

i) for all

i

^0. Besides, every run of

H

is represented by some symbolic run of

H

.

Given a region

I

^ , the reachable region (

I

^7!) ^  of

I

is the set of all states that are reachable from states in

I

:



²(

I

^7!) i ⁹



⁰²

I: 

^07!

:

Notice that

I

^(

I

^7!).

The following proposition suggests a method for computing the reachable region (

I

^7!) of

I

.

Proposition 4.1

Let

I

= ^S_`^2Loc(

`;I

`) be a region of the linear hybrid system

H

. The reachable region (

I

^7!) =^S_`^2Loc(

`;R

`) is the least xpoint of the equation

X

= ^h

I

^[post[

X

]^i%

or, equivalently, for all locations

`

²Loc, the set

R

` of valuations is the least xpoint of the set of equations

X

` = ^h

I

`^{[ [}

e⁼⁽`<sup>0</sup>;`^)2Edgpost_e[

X

`<sup>0</sup>]<sup>i%</sup><sub>`</sub>

:

Let be a linear formula over Var. By [[ ]] we denote the set of valuations that satisfy . A set

P

^

V

of valuations is linear if

P

is denable by a linear formula; that is,

P

= [[ ]] for some linear formula . If Var contains

n

variables, then a linear set of valuations can be thought of as a union of polyhedra in

n

-dimensional space.

Lemma 4.1

For all linear hybrid systems

H

, if

P

^

V

is a linear set of valuations, then for all locations

`

²Loc and transitions

e

²Edg, both ^h

P

^i%_` and post_e[

P

] are linear sets of valuations.

Given a linear formula , we write ^{h i%}_{`</sub> and post<sub>e</sub>[ ] for the linear formulas that dene the sets of valuations <sup>h</sup>[[ ]]<sup>i%</sup><sub>`} and post_e[[[ ]]], respectively.

Let pc ⁶² Var be a control variable that ranges over the set Loc of locations and let

R

=

S`^2Loc(

`;R

`) be a region. The region

R

is linear if for every location

`

² Loc, the set

R

` of valuations is linear. If the sets

R

` are dened by the linear formulas `, then the region

R

is dened by the linear formula

= ^_

`^2Loc(pc =

`

^{^} `);

that is, [[ ]] =

R

. Hence, by Lemma 4.1, for all linear hybrid systems, if

R

is a linear region, then so are both^h

R

^i% and post[

R

].

Using Proposition 4.1, we compute the reachable region (

I

^7!) of a region

I

by successive approximation. Lemma 4.1 ensures that all regions computed in the process are linear. Since the reachability problem for linear hybrid systems is undecidable, the successive-approximation procedure does not terminate in general. The procedure does terminate for simple multirate timed systems (Theorem 3.1) and for the following example.

Example: the leaking gas burner

Let

I

be the set of initial states dened by the linear formula

I = (pc = 1 ^{^}

x

=

y

=

z

= 0)

:

The set (

I

^7!) of reachable states is characterized by the least xpoint of the two equations

1 = ^h

x

=

y

=

z

= 0^_ post⁽²_;¹⁾[ ²]^i%1

2 = ^hfalse^_ post⁽¹_;²⁾[ ¹]^i%2 which can be iteratively computed as

1;i = ¹;i^{;1_ h}post⁽²_;¹⁾[ ²;i^;1]^i%1

2;i = ²;i^{;1_ h}post⁽¹_;²⁾[ ¹;i^;1]^i%2

where ¹;⁰ =^h

x

=

y

=

z

= 0^i%1 = (

x

^1 ^{^}

y

=

x

=

z

) and ²;⁰ = false. For

i

= 1, we have

1;¹ = ¹;^{0_ h}post⁽²_;¹⁾[ ²;⁰]^i%1

= ¹;⁰

2;¹ = ²;^{0_ h}post⁽¹_;²⁾[ ¹;¹]^i%2

= ^hpost⁽¹_;²⁾[

x

^1 ^{^}

y

=

x

=

z

= 0]^i%2

= ^h(

x

= 0 ^{^}

y

^1 ^{^}

z

=

y

)^i%2

= (

z

^1 ^{^}

y

=

z

+

x

) Now, it is easy to show by induction that for all

i

^2,

1;i= ¹;i^;1_

x

^1 ^{^} 0^

z

^;

x

^

i

^{^} 30

i

+

z

^

y

and

2;i= ²;i^;1_

y

^

i

+ 1 ^{^} 30

i

+

x

+

z

^

y

Hence, the least solution of the equations above is the linear formula

R = (pc = 1 ^{^ 1})^_ (pc = 2 ^{^ 2}) where

1 =

x

^1 ^{^}

x

=

y

=

z

^{_ 9}

i

^1

:

(

x

^1 ^{^} 0^

z

^;

x

^

i

^{^} 30

i

+

z

^

y

)

= (

x

^1 ^{^}

x

=

y

=

z

)^_ (

x

^1 ^{^}

x

^

z

^{^}

y

+ 30

x

^31

z

)

2 =

z

^1 ^{^}

y

=

x

+

z

^{^}

x

^0^{_ 9}

i

^1

:

(

z

^

i

+ 1 ^{^} 30

i

+

x

+

z

^

y

)

= (

z

^1 ^{^}

y

=

x

+

z

^{^}

x

^0)^_

y

^

x

+ 31

z

^;30

This characterization of the reachable states can be used to verify invariance properties of the gas burner system ( Ris the strongest invariant of the system). For instance, the formula R implies the design requirement

y

^60 ⁾ 20

z

^

y

.

4.2 Backward Analysis

The forward time closure and the postcondition dene the successor of a region

R

. Dually, we can compute the predecessor of

R

.

Given a location

`

² Loc and a set of valuations

P

^

V

, the backward time closure of

P

at

`

is the set of valuations from which it is possible to reach some valuation



²

P

by letting time progress:



^02h

P

^i._` i ⁹



²

V;t

²R^0

: 

=

'

`[



⁰](

t

) ^{^}



²

P

^{^} tcp_`[



⁰](

t

)

:

Thus, for all valuations



^{0 2h}

P

^i._` , there exist a valuation



²

P

and a nonnegative real

t

²R^0 such that (

`;

⁰)^!t(

`;

).

Given a transition

e

= (

`;a;;`

⁰) and a set of valuations

P

^

V

, the precondition pre_e[

P

] of

P

with respect to

e

is the set of valuations from which it is possible to reach a valuation



²

P

by executing the transition

e

:



⁰²pre_e[

P

] i ⁹



²

V: 

²

P

^{^} (



⁰

;

)²

:

Thus, for all valuations



⁰²pre_e[

P

], there exists a valuation



²

P

such that (

`;

⁰)^!a(

`

⁰

;

).

The backward time closure and the precondition can be naturally extended to regions: for

R

=

S`^2Loc(

`;R

`),

h

R

^i. = ^[

`^2Loc(

`;

^h

R

`<sup>i.</sup>` ) pre[

R

] = ^[

e⁼⁽`<sup>0</sup>;`^)2Edg(

`

⁰

;

pre_e[

R

`])

Given a region

R

^, the initial region (^7!

R

)^ of

R

is the set of all states from which a state in

R

is reachable:



²(^7!

R

) i ⁹



⁰²

R: 

^7!



⁰

:

Notice that

R

^(^7!

R

).

The following proposition suggests a method for computing the initial region (^7!

R

) of

R

.

Proposition 4.2

Let

R

= ^S_`^2Loc(

`;R

`) be a region of the linear hybrid system

H

. The initial region

I

=^S_`^2Loc(

`;I

`) is the least xpoint of the equation

X

= ^h

R

^[pre[

X

]^i.

or, equivalently, for all locations

`

²Loc, the set

I

` of valuations is the least xpoint of the set

X

` = ^h

R

`^{[ [}

e⁼⁽`;`^0)2Edgpre_e[

X

`<sup>0</sup>]<sup>i.</sup><sub>`</sub> of equations.

Lemma 4.2

For all linear hybrid systems

H

, if

P

^

V

is a linear set of valuations, then for all locations

`

²Loc and transitions

e

²Edg, both ^h

P

^i._` and pre_e[

P

] are linear sets of valuations.

It follows that for all linear hybrid systems, if

R

is a linear region, then so are both ^h

R

^i. and pre[

R

]. Given a linear formula , we write ^{h i.}_{`</sub> and pre<sub>e</sub>[ ] for the linear formulas that dene the sets of valuations <sup>h</sup>[[ ]]<sup>i.</sup><sub>`} and pre_e[[[ ]]], respectively.