Oscar H. Ibarra and Jianwen Su
Augmenting the Discrete Timed Automaton with Other Data
Structures
Theoretical Computer Science, Vol. 289, No. 1, Pages 191-204,
October 2002
We describe a general automata-theoretic approach for analyzing the
verification problems of discrete timed automata (i.e., timed automata
with integer-valued clocks) augmented with various data
structures. Formally, let 
be a class of
nondeterministic machines with reversal-bounded counters and possibly
other data structures (e.g., a pushdown stack, a queue, a read-write
worktape, etc.). Let A be a discrete timed automaton and
M be a machine in . Denote by
A
M the combined automaton, i.e., A augmented
with M (in some precise sense to be defined). We show that if
has a decidable emptiness problem, then the
(binary, forward, backward) reachability, safety, and invariance for
AM are solvable. We give examples of such 's and exhibit some new properties of discrete timed automata
that can be verified. We also briefly consider reachability in
discrete timed automata operating in parallel.