Symbolic Verification of Hybrid Systems: An Algebraic Approach

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.