Past Pushdown Timed Automata

13 years 7 months ago
Past Pushdown Timed Automata
d Abstract) Zhe Dang   , Tevfik Bultan ¡ , Oscar H. Ibarra ¡ , and Richard A. Kemmerer ¡ ¢ School of Electrical Engineering and Computer Science Washington State University Pullman, WA 99164£ Department of Computer Science University of California Santa Barbara, CA 93106 Abstract. We consider past pushdown timed automata that are discrete pushdown timed automata [20] with past-formulas as enabling conditions. Using past formulas allows a past pushdown timed automaton to access the past values of the finite state variables in the automaton. We prove that the reachability (i.e., the set of reachable configurations from an initial configuration) of a past pushdown timed automaton can be accepted by a nondeterministic reversal-bounded counter machine augmented with a pushdown stack (i.e., a reversal-bounded NPCM). By using the known fact that the emptiness problem for reversal-bounded NPCMs is decidable, we show that model-checking past pushdown timed automata against Presburger ...
Zhe Dang, Tevfik Bultan, Oscar H. Ibarra, Richard
Added 30 Jul 2010
Updated 30 Jul 2010
Type Conference
Year 2001
Where WIA
Authors Zhe Dang, Tevfik Bultan, Oscar H. Ibarra, Richard A. Kemmerer
Comments (0)