Hybrid Control Verification Methodologies and Tools

In theory, the approaches to hybrid controller design discussed above guarantee that the requirements specification is satisfied by design. In practice, system complexity often limits the applicability of automatic controller synthesis methods, and currently, a common approach to the design of hybrid controllers involves independently coming up with a reasonable design for both the discrete and continuous parts. The combined hybrid controller is then put together by means of interfaces, and verification is carried out to ensure that it satisfies certain properties. Typically, some design errors are found, and the verification attempt supplies the design engineer with diagnostic information that is helpful for reformulating the design. The process of simulation, verification attempts, and redesign is iterated until a successful design is obtained.

The Algorithmic Approach: HyTech
This approach has been motivated by the success of verification techniques for finite-state systems. Verification tools for finite state machines have been in use for years (SPIN [12] , SMV [13], COSPAN [14], HSIS [15], etc.) and proven successful for the automatic analysis of discrete problems such as communication protocols [16] and digital circuits. The push towards stronger verification techniques has been in the direction of extending the standard finite state machine results to incorporate progressively more complicated continuous dynamics. The first extension has been for systems with clocks [17] [18] . Verification tools for finite state machines with clocks have been implemented (KRONOS [19] , UPPAAL [20], and Timed COSPAN [21]) and used successfully for the automatic analysis of real-time hardware [22] and software [23].

The possible values of clocks range over the real numbers. Hence the state space of real-time systems is infinite and automatic verification must proceed symbolically, by representing sets of states using symbolic constraints (instead of state enumeration). Symbolic state space analysis techniques have been extended from real-valued clock variables to all real-valued variables whose trajectories can be characterized using piecewise-linear envelopes [24]. If the guarded assignments and invariants of hybrid automata are linear constraints on continuous states, and the differential equations are replaced by linear constraints on first derivatives, then we obtain the class of linear hybrid automata, which can be analyzed fully automatically. A typical linear constraint on first derivatives is a rectangular differential inclusion x' in [l,u], which can be used to model, for example, time measured by clocks with bounded drift, or distance covered by vehicles with bounded speed. The only computer package capable of dealing with the full class of linear hybrid automata, HyTech, is under development by one of our team members [25]. To support the automatic verification of layered hybrid multi-agent systems, we propose to extend HyTech in three directions.

From hybrid automata to hybrid modules. HyTech currently operates on the input of a given hybrid automaton. ``Flat'' hybrid automata support neither modular nor hierarchical decomposition, and thus are not suited for the specification or design of layered multi-agent systems. Above we outlined an extension of hybrid automata to hybrid modules, which distinguish between inputs and outputs, and can be composed and refined. We plan to generalize the verification theory for hybrid automata to hybrid modules, and to extend HyTech for verifying hybrid modules. This includes, in particular, the development of an assume-guarantee principle for hybrid modules. An assume-guarantee principle asserts that if, under given environment assumptions, every subsystem is guaranteed to perform correctly, then the compound system performs correctly. Assume-guarantee principles have played an important role in the verification of discrete systems, where they depend on the existence of winning strategies in discrete games between the system and the environment[26]. Hybrid analogues, which likely involve the study of continuous games, have not yet been formulated.

Conservative approximation of nonlinear hybrid automata. Most control applications cannot be modeled directly as linear hybrid modules. In [27] it has been suggested to approximate arbitrary trajectories by piecewise-linear envelopes, and so obtain conservative approximations of hybrid systems that can be analyzed automatically: if the approximating system satisfies a safety property, then so does the approximated system (which has fewer trajectories); otherwise, the approximation must be refined. This approximation technique has been improved in [28], where it is shown that, for a given cost, phase-domain approximation allows more accurate predictions than time-domain approximation. While in the time domain, differential equations are approximated by pairwise independent rectangular differential inclusions, in the phase domain, additional flow constraints, such as x'< y', are taken into account. We plan to extend HyTech to (semi)automatically construct and analyze linear phase-domain approximations. The extension will be guided by examples from the AHS and Air Traffic Management studies.

From reachability analysis to control. To check if a hybrid system has a trajectory that leads to an error state, HyTech searches backward from the error states to find all states that may lead to an error state. If, instead, one searches backward from a set of target states to find all states that must lead to a target state, one can design a controller that forces a system into a set of target states. This control technique has been suggested for timed systems in[29] . We plan to extend the technique to hybrid modules, implement it in HyTech, and study its relation to classical control. The Deductive Approach: STeP The Stanford Temporal Prover, STeP [30] , supports the computer-aided formal verification of reactive (and, in particular concurrent) and real-time systems based on temporal specifications. The deductive methods of STeP verify temporal properties of systems by means of verification rules and verification diagrams. Verification rules are used to reduce temporal properties of systems to first-order verification conditions [31]. Verification diagrams[32] provide a visual language for guiding, organizing, and displaying proofs. Verification diagrams allow the user to construct proofs hierarchically, starting from a high-level, intuitive proof sketch and proceeding incrementally, as necessary, through layers of greater detail.

The system implements powerful techniques for automatic invariant generation[33] . Deductive verification almost always relies on finding, for a given program and specification, suitably strong (inductive) invariants and intermediate assertions. The user can typically provide an intuitive, high-level invariant, from which the system derives stronger, more detailed, top-down invariants. Simultaneously, bottom-up invariants are generated automatically by analyzing the program text. By combining these two methods, the system can often deduce sufficiently detailed invariants to carry through the entire verification process. The system also provides an integrated suite of simplification and decision procedures for automatically checking the validity of a large class of first-order and temporal formulas. This degree of automated deduction is sufficient to handle most of the verification conditions that arise in deductive verification. Recently, STeP was extended to support verification of safety properties of real-time systems, based on the computational model of clocked transition systems as presented in[34] . Systems described by timed transition systems or timed automata can be readily translated into this formalism. The specification language of linear time temporal logic was extended with clocks measuring progress of time.

STeP has been applied in the analysis of many reactive systems. Real-time systems that were analyzed include Fisher's mutual-exclusion protocol and an (N-process) railroad gate controller [35].

To support the deductive verification of hybrid dynamical systems, and in particular control systems, we propose to extend STeP in the following directions:

1. Hybrid STeP. Except for clocks, the current version of STeP does not support continuously varying variables. STeP will be extended to support hybrid systems based on the computational model of phase transition systems as presented in [34] . This paper shows that an important class of hybrid systems can be reduced to an induced fair transition system, while preserving runs. Thus, the existing tools and methods for the discrete reactive systems already implemented in STeP can be reused in the verification of safety properties of hybrid systems. A phase transition system extends a fair transition system with a set of activities, each represented by an activity relation that describes the conditional evolution of the continuous variables of the system over time, and a time progress condition, an assertion that specifies a global restriction on the progress of time. In the induced transition system, the set of discrete transitions is extended with a transition associated with each activity. In addition to the new computational model we will devise a hybrid system description language that allows the textual description of system with both continuously-varying variables and discrete transitions. To handle systems that cannot be described by guarded first-order differential equations, we are planning to use linear approximation methods.
   
   
2. Modularity and Compositionality. The verification of multi-layered distributed control systems requires the ability to perform modular and compositional reasoning. Currently STeP has limited support for modular and compositional verification. In [36] we present the formalism of modular verification diagrams, which allow a modular representation of proofs that reactive systems satisfy a specification expressible by an existentially quantified temporal-logic formula. This formalism will be extended to real-time and hybrid systems, and will include methods to infer properties of a system from the properties of its subsystems.
   
   
3. Analysis. Design and verification of distributed control systems requires, in addition to verification tools, complementary tools to analyze the system in various ways. Simulation facilities for fair transition systems are being added to STeP now, and these will be extended into simulation and behavior visualization tools for hybrid systems too.

Game-Theoretic Approach to Hybrid Control Verification
Optimal control and gaming ideas may prove useful not only in hybrid control design but also in hybrid control verification. Standard algorithmic verification techniques often require some form of exhaustive search, to verify that all possible trajectories of a system satisfy a certain property. As discussed above, this leads to undecidability and complexity problems. An optimal-control approach to verification could be to obtain the worst possible trajectory by solving an optimal-control problem, and verifying that if the property holds for this trajectory, then it will also hold for all other trajectories. Optimal-control ideas can also be used to generate abstractions of continuous system behavior in terms of discrete languages. For example, optimal control can be used to obtain the minimum and maximum times that a hybrid system spends in each discrete state. These bounds can then be used for abstracting the hybrid system, and verification can then be performed more easily on the abstracted system.

Verification of closed-loop hybrid systems is better suited for optimal control, rather than game theory, as one of the two players (the controller) has its strategy fixed a-priori. Therefore only the disturbances, trying to do their worst to upset the design, enter the picture. [37] discusses the application of these ideas to the automated highway example. An interesting class of disturbances that need to be considered in this context is class 4: commands from the discrete controller. From the point of view of the continuous system (where the optimal control problem is to be solved) these commands can be viewed as signals that make the continuous system switch between control laws, fixed points, etc. Optimal control can be used to determine the discrete command sequences that force the continuous system to violate the performance specifications. If the discrete design is such that these command sequences are excluded, then the hybrid design is verified.

Our research on the application of gaming and optimal-control ideas to hybrid design and verification will focus on efficient numerical algorithms. In addition, extensive designer input is needed during the controller design, verification, or abstraction process. We will work on techniques for partially automating the process. Our approach is best suited to address questions of ``reachability'' (safety). Reachability problems can usually be cast as pursuit evasion problems in the gaming framework. Extensions to other important questions such as liveness and performance will also be addressed on this grant.

Top