×

Symbolic verification of hybrid systems: an algebraic approach. (English) Zbl 1293.93420

Summary: In this paper we present a new symbolic, computer algebra based approach to hybrid systems. Hybrid systems are systems containing both, continuous and discrete changing quantities. As is commonly done, we model hybrid systems using hybrid automata. Hybrid automata extend the classical notion of finite state machines by combining differential equations to model the dynamic behavior of systems with a finite control. In contrast to other approaches we consider hybrid automata as a generalization of differential equations and develop the notion of an “explicit symbolic solution” of a hybrid automaton. An explicit symbolic solution is an expression which gives the value of the quantities in question, the state variables, as a function of the design parameters and time. These solutions allow us to perform the verification of design properties. We present an algorithm leading to an implementation which computes these explicit symbolic solutions. We were able to detect design constraints on control systems that other methods fail to detect. This paper gives the basic definitions, algorithms, and three examples to demonstrate the advantage of the proposed approach.

MSC:

93C30 Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems)
68W30 Symbolic computation and algebraic computation

Software:

STeP
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Alur, R.; Coucoubetis, C.; Halbwachs, N.; Henzinger, T. A.; Ho, P. H.; Nicolin, X.; Olivero, A.; Sifakis, J.; Yovine, S., The Algorithmic Analysis of Hybrid Systems, Theor Comput Sci, 138, 3-34 (1995)
[2] Alur, R.; Henzinger, T. A.; Ho, P. H., Automatic symbolic verification of embedded systems, (Proceedings of the 14th Annual IEEE real-time systems symposium (RTSS) (1993)), 2-11
[3] Bronstein, M., The transcendental risch differential equation, J Symbol Computation, 9, 49-60 (1990) · Zbl 0707.12003
[4] Henzinger TA. The theory of hybrid automata. In: 11th Annual IEEE symposium on logic in computer science (LICS) 96, 278-292; Henzinger TA. The theory of hybrid automata. In: 11th Annual IEEE symposium on logic in computer science (LICS) 96, 278-292
[5] Filipoph P. Differential equations with discontinuous right-hand side. Mathematics and its Applications. Kluwer, ISBN 90-277-2699-X; Filipoph P. Differential equations with discontinuous right-hand side. Mathematics and its Applications. Kluwer, ISBN 90-277-2699-X
[6] Branicky, M. S., A unified framework for hybrid control: model and optimal control theory, IEEE Trans Auto Control, 43, 1 (1998) · Zbl 0951.93002
[7] Nicollin, X.; Olivero, A.; Sifakis, J.; Yovine, S., An approach to the description and analysis of hybrid systems, Lecture Notes in Computer Science, 736, 149-178 (1993)
[8] Mohrenschildt, Mv., A normal form for rings of piecewise functions, J Symbolic Computation, 26, 607-619 (1998) · Zbl 0920.68063
[9] Mohrenschildt, Mv., Using piecewise to solve classes of control theory problems, MapleTech, 4, 3, 33-37 (1997)
[10] Mohrenschildt Mv. Solving discontinuous differential equations. In: (Eds.),. The Combinatory Program, Engeler E, Birkhauser, pp 98-116; Mohrenschildt Mv. Solving discontinuous differential equations. In: (Eds.),. The Combinatory Program, Engeler E, Birkhauser, pp 98-116
[11] Mohrenschildt Mv. Solving discontinuous ordinary differential equations with a computer algebra system, submitted to J Symbolic Computation; Mohrenschildt Mv. Solving discontinuous ordinary differential equations with a computer algebra system, submitted to J Symbolic Computation
[12] Hybrid Systems, Lecture Notes in Computer Science (736); Hybrid Systems, Lecture Notes in Computer Science (736)
[13] Clarke FH. et al. Non-smooth analysis and control theory. Springer, ISBN 0-387-98336-8; Clarke FH. et al. Non-smooth analysis and control theory. Springer, ISBN 0-387-98336-8
[14] Kesten, Y.; Pnueli, A.; Sifakis, J.; Yovine, S., Decidable integration graphs: a class of decidable hybrid systems, Information and Computation, 150, 209-243 (1999) · Zbl 1045.68566
[15] Kurki-Suonio, R., Hybrid models with fairness and distributed clocks, Lecture Notes in Computer Science, 736, 103-120 (1993)
[16] Nicollin, X.; Sifakis, J.; Yovine, S., Compiling real-time specifications into extended automata, IEEE TSE Real- Time Systems, 18, 9, 794-804 (1992)
[17] Singer, M. F., Formal solutions of differential equations, J Symbolic Computation, 10, 59-94 (1990) · Zbl 0727.12011
[18] Kapur, D.; Shyamasundar, R. K., Synthesizing controllers for hybrid systems. Hybrid and Real Time Systems, HART’97, Lecture Notes in Computer Science 1201, 361-375 (1997), Springer-Verlag
[19] Pappas, G.; Lafferriere, G.; Yovine, S., A new class of decidable hybrid systems Hybrid Systems: Computation and Control, Lecture Notes in Computer Science 1569, HS’99, 137-152 (March 1999), Nijmegen, The Netherlands
[20] Manna, Z.; Sipma, H., Deductive verification of hybrid systems using STeP, HSCC 98, Lecture Notes in Computer Science 1386, 305-318 (1998)
[21] Alur, R.; Henzinger, A.; Lafferriere, G.; Pappas, G. J., Discrete Abstraction of Hybrid Systems, Proceedings of the IEEE, 88, 2, 971-984 (2000)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.