Modeling and verification of hybrid systems with clocked and unclocked events

Abstract

We define sampled-data hybrid automata (SDHA), to model systems with clocked and unclocked events. Although clocked events can be modeled in standard hybrid automata by introducing additional continuous state variables, we show in this paper how the SDHA formalism provides a basis for more efficient computational methods for verification. Towards this end, we define a transition system semantics for the SDHA and present a method for computing approximate quotient transition systems using a modification of existing tools for computing reachable sets for hybrid systems. The definitions and the elements of a model checking procedure for SDHA are illustrated with an example.