@inproceedings{DangEtAl:CAV:2000,
    Abstract = {We introduce discrete pushdown timed automata that are timed automata with integer-valued clocks augmented with a pushdown stack. A configuration of a discrete pushdown timed automaton includes a control state, finitely many clock values and a stack word. Using a pure automata-theoretic approach, we show that the binary reachability (i.e., the set of all pairs of configurations ($\alpha$,$\beta$), encoded as strings, such that $\alpha$ can reach $\beta$ through 0 or more transitions) can be accepted by a nondeterministic pushdown machine augmented with reversal-bounded counters (NPCM). Since discrete timed automata with integer-valued clocks can be treated as discrete pushdown timed automata without the pushdown stack, we can show that the binary reachability of a discrete timed automaton can be accepted by a nondeterministic reversal-bounded multicounter machine. Thus, the binary reachability is Presburger. By using the known fact that the emptiness problem is decidable for reversal-bounded NPCMs, the results can be used to verify a number of properties that can not be expressed by timed temporal logics for discrete timed automata and CTL* for pushdown systems.},
    Address = {Berlin, Heidelberg},
    Author = {Dang, Zhe and Ibarra, Oscar H. and Bultan, Tevfik and Kemmerer, Richard A. and Su, Jianwen},
    BookTitle = {Computer Aided Verification: 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000. Proceedings},
    Editor = {Emerson, E. Allen and Sistla, Aravinda Prasad},
    File = {cav00 (0) - a - a - s.pdf},
    ISBN = {978-3-540-45047-4},
    Pages = {69--84},
    Publisher = {Springer Berlin Heidelberg},
    Title = {Binary Reachability Analysis of Discrete Pushdown Timed Automata},
    URL = {https://doi.org/10.1007/10722167\_9},
    Year = {2000},
    bdsk-url-1 = {https://doi.org/10.1007/10722167\_9},
    date-added = {2017-12-06 18:04:52 +0000},
    date-modified = {2017-12-07 09:41:11 +0000},
    doi = {10.1007/10722167_9}
}

@inproceedings{DangEtAl:CAV:2000, Abstract = {We introduce discrete pushdown timed automata that are timed automata with integer-valued clocks augmented with a pushdown stack. A configuration of a discrete pushdown timed automaton includes a control state, finitely many clock values and a stack word. Using a pure automata-theoretic approach, we show that the binary reachability (i.e., the set of all pairs of configurations ($\alpha$,$\beta$), encoded as strings, such that $\alpha$ can reach $\beta$ through 0 or more transitions) can be accepted by a nondeterministic pushdown machine augmented with reversal-bounded counters (NPCM). Since discrete timed automata with integer-valued clocks can be treated as discrete pushdown timed automata without the pushdown stack, we can show that the binary reachability of a discrete timed automaton can be accepted by a nondeterministic reversal-bounded multicounter machine. Thus, the binary reachability is Presburger. By using the known fact that the emptiness problem is decidable for reversal-bounded NPCMs, the results can be used to verify a number of properties that can not be expressed by timed temporal logics for discrete timed automata and CTL* for pushdown systems.}, Address = {Berlin, Heidelberg}, Author = {Dang, Zhe and Ibarra, Oscar H. and Bultan, Tevfik and Kemmerer, Richard A. and Su, Jianwen}, BookTitle = {Computer Aided Verification: 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000. Proceedings}, Editor = {Emerson, E. Allen and Sistla, Aravinda Prasad}, File = {cav00 (0) - a - a - s.pdf}, ISBN = {978-3-540-45047-4}, Pages = {69--84}, Publisher = {Springer Berlin Heidelberg}, Title = {Binary Reachability Analysis of Discrete Pushdown Timed Automata}, URL = {https://doi.org/10.1007/10722167_9}, Year = {2000}, bdsk-url-1 = {https://doi.org/10.1007/10722167_9}, date-added = {2017-12-06 18:04:52 +0000}, date-modified = {2017-12-07 09:41:11 +0000}, doi = {10.1007/10722167_9} }