Membership Questions for Timed and Hybrid Automata

Timed and hybrid automata are extensions of finite-state machines for formal modeling of embedded systems with both discrete and continuous components. Reachability problems for these automata are well studied and have been implemented in verification tools. In this paper, for the purpose of effective error reporting and testing, we consider the membership problems for such automata. We consider different types of membership problems depending on whether the path (i.e. edge-sequence), or the trace (i.e. event-sequence), or the timed trace (i.e. timestamped eventsequence), is specified. We give comprehensive results regarding the complexity of these membership questions for different types of automata, such as timed automata and linear hybrid automata, with and without -transitions. In particular, we give an efficient O(n m2) algorithm for generating timestamps corresponding a path of length n in a timed automaton with m clocks. This algorithm is implemented in the verifier COSPAN to i...

• Type: Conference
• Year: 1998
• Where: RTSS
• Authors: Rajeev Alur, Robert P. Kurshan, Mahesh Viswanathan
• Keywords: Control Systems, Linear Hybrid Automata, Membership Question, RTSS 1998, Timed Traces