## Membership Problems for Timed and Hybrid Automata

*Rajeev Alur, Robert Kurshan, and
Mahesh Viswanathan*
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 event-sequence),
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
epsilon-transitions.

In particular, we give an efficient *O(n m^2)* 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 improve
its diagnostic feedback during timing verification.
Second, we show that for automata without epsilon-transitions,
the membership question is NP-complete for different types of automata
whether or not the timestamps are specified along with the trace.
Third, we show that for automata with epsilon-transitions, the membership
question is as hard as the reachability question even for timed traces:
it is PSPACE-complete
for timed automata, and undecidable for slight generalizations.

*Proceedings of the
19th IEEE Real-Time Systems Symposium*
(RTSS'98),
1998.