Introduction

Systems with both discrete and continuous dynamics are called hybrid systems. The Hybrid Input/Output Automaton (HIOA) [2] is a framework for compositional specification and analysis of hybrid systems. Most of our prior work with HIOA focused on verifying safety of hybrid systems [5]. Our current work [3,4] shows that HIOA is a suitable framework for applying both control theory and computer science techniques for analyzing hybrid systems. In particular, we bring together well known results from control theory, tools from formal verification and optimization to propose two methods for stability analysis of hybrid systems under slow switchings.

Approach

To prove stability of a hybrid system under slow switchings we use the average dwell time theorem of Hespanha and Morse [1]. Roughly, this theorem states that a hybrid system is uniformly stable if (a) the discrete switches are between modes that are individually stable, and (b) that the switches do not occur "too frequently" on the average. The latter requirement is termed as the average dwell time property; average dwell time (ADT) being the average duration of time the system stays in each mode. We propose two different approaches for verifying ADT properties of HIOA. This property effectively decouples the problem of finding the Lyapunov functions (which we assume are known, from existing control theory methods), from the problem of checking that all the executions of the HIOA satisfy certain properties. In general, properties of the executions of an automaton, are harder to verify than invariant properties which are properties of the state.

Our first approach for checking the ADT property relies on the availability of powerful formal verification techniques, like model checking and mechanical theorem proving, for checking invariants of hybrid automata. We transform the given automaton A to a new automaton A' and find a condition I(T) on the states of A', such that A has ADT T if and only if I(T) is an invariant of A'. This enables us to prove the ADT property by checking I(T) with a suitable formal verification technique. Our second approach is applicable to an important class of linear HIOA for which existence of a cyclic execution fragment with fast mode switches is necessary and sufficient for violating the ADT property. For this class of HIOA, we show that it is possible to automatically check the ADT property by solving a mixed integer linear program (MILP).

Progress

As indicated above, we have indeed found a general transformation which converts a given HIOA to a new one, such that the former has ADT T if and only if the latter has a certain invariant property I(T). We have illustrated this approach by analyzing the stability of a scale independent hysteresis switching system. As for the second approach, we have introduced the notion of an ADT preserving abstraction that eliminates certain "unimportant" variables from the set of variables of the given HIOA to give us a corresponding abstract region automaton. The abstract region automaton and the original HIOA have the same ADT and therefore, we can search for cyclic execution fragments with fast mode switches in the set of executions of the abstract automaton. We have proposed a methodology for constructing a MILP from a given linear HIOA A and T >= 0, such that the optimal value is positive if and only if the average dwell time of A is less than T. If the optimal value is positive, we get a witness execution fragment, namely the optimal solution, which violates the ADT property. This method of abstraction, and the formulation and solution of the MILP for verifying ADT has been demonstrated in detail with the gas-burner hybrid system example.

Future

We want to explore other interesting properties of HIOA which can be formulated and solved as search problems over the set of executions. We believe that finding the appropriate abstractions would play a key role in formulating different verification problems as mathematical programs. In this work we examined internal stability only; however, using the explicit external variables of the HIOA framework we would like to study input-output properties of hybrid systems as well. Another direction of future research is to extend these techniques to stochastic hybrid systems, by combining the probabilistic I/O automaton model with stability results for stochastic switched systems.

Research Support

This project is supported by DARPA Air Force contract number FA9550-04-C-0084, DARPA Award number F33615-01-C-1896, NSF Award numbers CCR-0326277 and CCR-0121277, NSF-Texas Engineering Experiment Station grant 64961-CS, DARPA/AFOSR MURI Award F49620-02-1-0325 and MURI AFOSR Award Number SA2796PO 1-0000243658.

References

[1] J. Hespanha and A. Morse. Stability of switched systems with average dwell-time. In Proceedings of 38th IEEE Conference on Decision and Control, pages 2655-2660, 1999.

[2] Nancy Lynch, Roberto Segala, and Frits Vaandrager. Hybrid I/O automata. Information and Computation,185(1):105-157, August 2003.

[3] Sayan Mitra, Daniel Liberzon. Stability of hybrid automata with average dwell time: An invariant approach. Submitted to IEEE Conference on Decision and Control, 2004.

[4] Sayan Mitra, Daniel Liberzon, and Nancy Lynch. Verifying average dwell time. Submitted for journal review.

[5] Sayan Mitra, Yong Wang, Nancy Lynch, and Eric Feron. Safety verification of model helicopter controller using hybrid Input/Output automata. In HSCC'03, Hybrid System: Computation Control, Prague, the Czech Republic, April 3-5 2003.