ON A CLASS OF TIMER HYBRID SYSTEMS REDUCIBLE TO FINITE-STATE AUTOMATA

A hybrid timer system with different timer rates and idling timer feat ure operating in dense time is modeled as an event-driven nondetermini stic automaton and it is shown that the system is weak bisimulation eq uivalent to a finite state nondeterministic automaton. Our original mo del is an event driven infinite state automaton as in Dill (1989) and an explicit representation for the bisimulation equivalent finite stat e automaton whose state set consists of an index set of active timers and n pairs of bounded nonnegative integers or the symbol +infinity is derived where n is the number of clocks. The reduced model is simpler than Dill's difference bound matrix model-and similar to the model us ed in Alur et al. (1990)-for the finite system automaton since all dif ference inequalities are represented by a single order vector of integ ers.