Sciweavers

Share
RTSS
1998
IEEE

Membership Questions for Timed and Hybrid Automata

11 years 9 months ago
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...
Rajeev Alur, Robert P. Kurshan, Mahesh Viswanathan
Added 05 Aug 2010
Updated 05 Aug 2010
Type Conference
Year 1998
Where RTSS
Authors Rajeev Alur, Robert P. Kurshan, Mahesh Viswanathan
Comments (0)
books