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 ...

• Type: Conference
• Year: 2001
• Where: WIA
• Authors: Zhe Dang, Tevfik Bultan, Oscar H. Ibarra, Richard A. Kemmerer
• Keywords: Artificial Intelligence, Past Pushdown, Pushdown Timed Automata, Pushdown Timed Automaton, WIA 2001