Verifying average dwell time of hybrid systems

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Verifying average dwell time of hybrid systems

Full text

Pdf (824 KB)

Source

ACM Transactions on Embedded Computing Systems (TECS) archive
Volume 8 , Issue 1 (December 2008) table of contents

Article No. 3

Year of Publication: 2008

ISSN:1539-9087

Authors

Sayan Mitra	University of Illinois at Urbana-Champaign, Urbana, IL
Daniel Liberzon	University of Illinois at Urbana-Champaign, Urbana, IL
Nancy Lynch	Massachusetts Institute of Technology, Cambridge, MA

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 8, Downloads (12 Months): 135, Citation Count: 0

Additional Information:

abstract references index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1457246.1457249 What is a DOI?

ABSTRACT

Average dwell time (ADT) properties characterize the rate at which a hybrid system performs mode switches. In this article, we present a set of techniques for verifying ADT properties. The stability of a hybrid system A can be verified by combining these techniques with standard methods for checking stability of the individual modes of A.

We introduce a new type of simulation relation for hybrid automata—switching simulation—for establishing that a given automaton A switches more rapidly than another automaton B. We show that the question of whether a given hybrid automaton has ADT τ_a can be answered either by checking an invariant or by solving an optimization problem. For classes of hybrid automata for which invariants can be checked automatically, the invariant-based method yields an automatic method for verifying ADT; for automata that are outside this class, the invariant has to be checked using inductive techniques. The optimization-based method is automatic and is applicable to a restricted class of initialized hybrid automata. A solution of the optimization problem either gives a counterexample execution that violates the ADT property, or it confirms that the automaton indeed satisfies the property. The optimization and the invariant-based methods can be used in combination to find the unknown ADT of a given hybrid automaton.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	R. Alur , C. Courcoubetis , N. Halbwachs , T. A. Henzinger , P.-H. Ho , X. Nicollin , A. Olivero , J. Sifakis , S. Yovine, The algorithmic analysis of hybrid systems, Theoretical Computer Science, v.138 n.1, p.3-34, Feb. 6, 1995 [doi>10.1016/0304-3975(94)00202-T]
	2	Johan Bengtsson , W. O. David Griffioen , Kåre J. Kristoffersen , Kim Guldstrand Larsen , Fredrik Larsson , Paul Pettersson , Wang Yi, Verification of an Audio Protocol with Bus Collision Using UPPAAL, Proceedings of the 8th International Conference on Computer Aided Verification, p.244-256, August 03, 1996
	3	Rajeev Alur , Costas Courcoubetis , Thomas A. Henzinger , Pei-Hsin Ho, Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems, Hybrid Systems, p.209-229, January 1993
	4	Alur, R. and Pappas, G. J., Eds. 2004. Hybrid systems: computation and control. In Proceedings of the 7th International Workshop (HSCC'04). Springer, Berlin.
	5	Myla Archer, TAME: Using PVS strategies for special-purpose theorem proving, Annals of Mathematics and Artificial Intelligence, v.29 n.1-4, p.139-181, 2000 [doi>10.1023/A:1018913028597]
	6	Alexandre M. Bayen , Eva Crück , Claire Tomlin, Guaranteed Overapproximations of Unsafe Sets for Continuous and Hybrid Systems: Solving the Hamilton-Jacobi Equation Using Viability Techniques, Proceedings of the 5th International Workshop on Hybrid Systems: Computation and Control, p.90-104, March 25-27, 2002
	7	Bemporad, A., Bicchi, A., and Buttazzo, G. C., Eds. 2007. Proceedings of the 10th International Workshop, (HSCC'07). Springer, Berlin.
	8	Alberto Bemporad , Manfred Morari, Verification of Hybrid Systems via Mathematical Programming, Proceedings of the Second International Workshop on Hybrid Systems: Computation and Control, p.31-45, March 29-31, 1999
	9	Michael Stephen Branicky, Studies in hybrid systems: modeling, analysis, and control, Massachusetts Institute of Technology, Cambridge, MA, 1996
	10	Branicky, M. 1998. Multiple Lyapunov functions and other analysis tools for switched and hybrid systems. IEEE Trans. Auto. Control 43, 475--482.
	11	Branicky, M., Borkar, V., and Mitter, S. 1998. A unified framework for hybrid control: Model and optimal control theory. IEEE Trans. Auto. Control 43, 1, 31--45.
	12	Debasish Chatterjee , Daniel Liberzon, Stability analysis of deterministic and stochastic switched systems via a comparison principle and multiple Lyapunov functions, SIAM Journal on Control and Optimization, v.45 n.1, p.174-206, 2006 [doi>10.1137/040619429]
	13	Thomas T. Cormen , Charles E. Leiserson , Ronald L. Rivest, Introduction to algorithms, MIT Press, Cambridge, MA, 1990
	14	Cruz, R. L. 1991. A calculus for network delay, part i: Network elements in isolation. IEEE Trans. Inform. Theory 37, 1, 114--131.
	15	Floyd, R. 1967. Assigning meanings to programs. In Proceedings of the Symposium on Applied Mathematics. Mathematical Aspects of Computer Science. American Mathematical Society, 19--32.
	16	Frehse, G. 2005. Phaver: algorithmic verification of hybrid systems past hytech. In Proceedings of the 8th International Workshop on Hybrid Systems: Computation and Control (HSCC'05). Springer, Berlin.
	17	GNU. GLPK—GNU linear programming kit. http://www.gnu.org/directory/libs/glpk.html.
	18	Heitmeyer, C. and Lynch, N. 1994. The generalized railroad crossing: A case study in formal verification of real-time system. In Proceedings of the 15th IEEE Real-Time Systems Symposium, (San Juan, Puerto Rico). IEEE, Los Alamitos, CA.
	19	Thomas A. Henzinger , Pei-Hsin Ho , Howard Wong-Toi, HYTECH: A Model Checker for Hybrid Systems, Proceedings of the 9th International Conference on Computer Aided Verification, p.460-463, June 22-25, 1997
	20	Thomas A. Henzinger , Peter W. Kopke, State Equivalences for Rectangular Hybrid Automata, Proceedings of the 7th International Conference on Concurrency Theory, p.530-545, August 26-29, 1996
	21	Thomas A. Henzinger , Peter W. Kopke , Anuj Puri , Pravin Varaiya, What's decidable about hybrid automata?, Proceedings of the twenty-seventh annual ACM symposium on Theory of computing, p.373-382, May 29-June 01, 1995, Las Vegas, Nevada, United States [doi>10.1145/225058.225162]
	22	Thomas A. Henzinger , Rupak Majumdar, Symbolic Model Checking for Rectangular Hybrid Systems, Proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems: Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, p.142-156, March 25-April 02, 2000
	23	Hespanha, J., Liberzon, D., and Morse, A. 2003. Hysteresis-based switching algorithms for supervisory control of uncertain systems. Automatica 39, 263--272.
	24	Hespanha, J. and Morse, A. 1999. Stability of switched systems with average dwell-time. In Proceedings of 38th IEEE Conference on Decision and Control. IEEE, Los Alamitos, CA, 2655--2660.
	25	Hespanha, J. P. and Tiwari, A., Eds. 2006. Proceedings of the 9th International Workshop on Hybrid Systems: Computation and Control (HSCC'06). Springer, Berlin.
	26	Khalil, H. K. 2002. Nonlinear Systems 3rd Ed. Prentice Hall, Upper Saddle River, NJ.
	27	Alexander B. Kurzhanski , Pravin Varaiya, Ellipsoidal Techniques for Reachability Analysis, Proceedings of the Third International Workshop on Hybrid Systems: Computation and Control, p.202-214, March 23-25, 2000
	28	Gerardo Lafferriere , George J. Pappas , Sergio Yovine, A New Class of Decidable Hybrid Systems, Proceedings of the Second International Workshop on Hybrid Systems: Computation and Control, p.137-151, March 29-31, 1999
	29	Liberzon, D. 2003. Switching in Systems and Control. Systems and Control: Foundations and Applications. Birkhauser, Boston, MA.
	30	Carolos Livadas , John Lygeros , Nancy A. Lynch, High-Level Modeling and Analysis of TCAS, Proceedings of the 20th IEEE Real-Time Systems Symposium, p.115, December 01-03, 1999
	31	Lynch, N. 1996. A three-level analysis of a simple acceleration maneuver, with uncertainties. In Proceedings of the 3rd AMAST Workshop on Real-Time Systems. World Scientific Publishing Company, Mountain View, CA, 1--22.
	32	Nancy Lynch , Roberto Segala , Frits Vaandrager, Hybrid I/O automata, Information and Computation, v.185 n.1, p.105-157, August 25, 2003 [doi>10.1016/S0890-5401(03)00067-1]
	33	Nancy Lynch , Frits Vaandrager, Forward and backward simulations II.: timing-based systems, Information and Computation, v.128 n.1, p.1-25, July 10, 1996 [doi>10.1006/inco.1996.0060]
	34	Maler, O. and Pnueli, A., Eds. 2003. Proceedings of the 6th International Workshop on Hybrid Systems: Computation and Control (HSCC'03). Springer, Berlin.
	35	Ian Mitchell , Claire Tomlin, Level Set Methods for Computation in Hybrid Systems, Proceedings of the Third International Workshop on Hybrid Systems: Computation and Control, p.310-323, March 23-25, 2000
	36	Sayan Mitra , Nancy A. Lynch, A verification framework for hybrid systems, Massachusetts Institute of Technology, Cambridge, MA, 2007
	37	Mitra, S. and Archer, M. 2005. PVS strategies for proving abstraction properties of automata. Electronic Notes Theore. Comput. Sci. 125, 2, 45--65.
	38	Mitra, S. and Lynch, N. A. 2007. Trace-based semantics for probabilistic timed i/o automata. In Proceedings of the 10th International Workshop (HSCC'07), (Pisa, Italy), April 3--5. Springer, Berlin, 718--722.
	39	Mitra, S., Wang, Y., Lynch, N., and Feron, E. 2003. Safety verification of model helicopter controller using hybrid Input/Output automata. In Proceedings of the 6th International Workshop on Hybrid Systems: Computation and Control (HSCC'03). Springer, Berlin, 343--358.
	40	Morari, M. and Thiele, L., Eds. 2005. Proceedings of the 8th International Workshop on Hybrid Systems: Computation and Control (HSCC'05). Springer, Berlin.
	41	Morse, A. S. 1996. Supervisory control of families of linear set-point controllers, part 1: Exact matching. IEEE Trans. Auto. Control 41, 1413--1431.
	42	Sam Owre , S. Rajan , John M. Rushby , Natarajan Shankar , Mandayam K. Srivas, PVS: Combining Specification, Proof Checking, and Model Checking, Proceedings of the 8th International Conference on Computer Aided Verification, p.411-414, August 03, 1996
	43	Prajna, S. and Jadbabaie, A. 2004. Safety verification of hybrid systems using barrier certificates. In Proceedings of the 7th International Workshop on Hybrid Systems: Computation and Control (HSCC'04). Springer, Berlin.
	44	Proceedings of the 5th International Workshop on Hybrid Systems: Computation and Control, March 2002
	45	Umeno, S. and Lynch, N. A. 2007. Safety verification of an aircraft landing protocol: A refinement approach. In Proceedings of the 10th International Workshop, (HSCC'07). Springer, Berlin, 557--572.
	46	van der Schaft, A. and Schumacher, H. 2000. An Introduction to Hybrid Dynamical Systems. Springer, Berlin.
	47	L. Vu , D. Chatterjee , D. Liberzon, Brief paper: Input-to-state stability of switched systems and switching adaptive control, Automatica (Journal of IFAC), v.43 n.4, p.639-646, April, 2007 [doi>10.1016/j.automatica.2006.10.007]
	48	H. B. Weinberg , N. Lynch, Correctness of vehicle control systems-a case study, Proceedings of the 17th IEEE Real-Time Systems Symposium (RTSS '96), p.62, December 04-06, 1996
	49	H. B. Weinberg , Nancy Lynch , Norman Delisle, Verification of automated vehicle protection systems (extended abstract), Proceedings of the DIMACS/SYCON workshop on Hybrid systems III : verification and control: verification and control, p.101-113, July 1996, New Brunswick, NeW Jersey, United States
	50	Williams, H. 1990. Model Building in Mathematical Programming 3rd Ed. John Wiley, New York.
	51	Zhai, G., Hu, B., Yasuda, K., and Michel, A. 2000. Stability analysis of switched systems with stable and unstable subsystems: An average dwell time approach. In Proceedings of the American Control Conference (AACC).