Abstract
A discrete pushdown timed automaton is a pushdown machine with integer-valued clocks. It has been shown recently that the binary reachability of a discrete pushdown timed automaton can be accepted by a 2-tape pushdown acceptor with reversal-bounded counters. We improve this result by showing that the stack can be removed from the acceptor, i.e., the binary reachability can be accepted by a 2-tape finite-state acceptor with reversal-bounded counters.We also obtain similar results for more general machine models. Our characterizations can be used to verify certain properties concerning these machines that were not verifiable before using previous techniques. We are also able to formulate a subset of Presburger LTL that is decidable for satisfiability-checking with respect to these machines.
Supported in part by NSF grant IRI-9700370
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
R. Alur and D. Dill. “The theory of timed automata,” TCS, 126(2):183–236, 1994
P. Abdulla and B. Jonsson. “Verifying programs with unreliable channels,” Information and Computation, 127(2): 91–101, 1996
A. Bouajjani, J. Esparza, and O. Maler. “Reachability analysis of pushdown automata: application to model-Checking,” CONCUR’97, LNCS 1243, pp. 135–150
G. Cece and A. Finkel. “Programs with Quasi-Stable Channels are Effectively Recognizable,” CAV’97, LNCS 1254, pp. 304–315 244
H. Comon and V. Cortier. “Flatness is not a weakness,” Proc. Computer Science Logic, 2000
H. Comon and Y. Jurski. “Multiple counters automata, safety analysis and Presburger arithmetic,” CAV’98, LNCS 1427, pp. 268–279
H. Comon and Y. Jurski. “Timed automata and the theory of real numbers,” CONCUR’99, LNCS 1664, pp. 242–257
Z. Dang. “Binary reachability analysis of timed pushdown automata with dense clocks,” CAV’01, LNCS 2102, pp. 506–517
Z. Dang and O. H. Ibarra. “Liveness verification of reversal-bounded counter machines with a free counter,” submitted, 2001
Z. Dang, O. H. Ibarra, T. Bultan, R. A. Kemmerer and J. Su. “Binary Reachability Analysis of Discrete Pushdown Timed Automata,” CAV’00, LNCS 1855, pp. 69–84
Z. Dang, P. San Pietro, and R. A. Kemmerer. “On Presburger Liveness of Discrete Timed Automata,” STACS’01, LNCS 2010, pp. 132–143
J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon. “Effcient Algorithms for Model Checking Pushdown Systems,” CAV’00, LNCS 1855, pp. 232–247
A. Finkel and G. Sutre. “Decidability of Reachability Problems for Classes of Two Counter Automata,” STACS’00, LNCS 1770, pp. 346–357 244
A. Finkel, B. Willems, and P. Wolper. “A direct symbolic approach to model checking pushdown systems,” INFINITY’97
S. Ginsburg and E. Spanier. “Bounded Algol-like languages,” Transactions of American Mathematical Society, 113, pp. 333–368, 1964.
O. H. Ibarra. “Reversal-bounded multicounter machines and their decision problems,” J. ACM, 25 (1978) 116–133
O. H. Ibarra. “Reachability and safety in queue systems with counters and pushdown stack,” Proceedings of the International Conference on Implementation and Application of Automata, pp. 120–129, 2000.
O. H. Ibarra, T. Bultan, and J. Su. “Reachability analysis for some models of infinite-state transition systems,” CONCUR’00, pp. 183–198, 2000.
O. H. Ibarra. “Reachability and safety in queue systems with counters and pushdown stack,” Proceedings of the International Conference on Implementation and Application of Automata, pp. 120–129, 2000
O. H. Ibarra, Z. Dang, and P. San Pietro, “Verification in Loosely Synchronous Queue-Connected Discrete Timed Automata,” submitted. 2001
O. H. Ibarra and J. Su. “Generalizing the discrete timed automaton,” Proceedings of the International Conference on Implementation and Application of Automata, 206–215, 2000.
O. H. Ibarra, J. Su, T. Bultan, Z. Dang, and R. A. Kemmerer. “Counter Machines: Decidable Properties and Applications to Verification Problems,”, MFCS’00, LNCS 1893, pp. 426–435
K. L. McMillan. “Symbolic model-checking — an approach to the state explosion problem,” PhD thesis, Department of Computer Science, Carnegie Mellon University, 1992
W. Peng and S. Purushothaman. “Analysis of a Class of Communicating Finite State Machines,” Acta Informatica, 29(6/7): 499–522, 1992
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ibarra, O.H., Dang, Z. (2001). On Removing the Pushdown Stack in Reachability Constructions. In: Eades, P., Takaoka, T. (eds) Algorithms and Computation. ISAAC 2001. Lecture Notes in Computer Science, vol 2223. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45678-3_22
Download citation
DOI: https://doi.org/10.1007/3-540-45678-3_22
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42985-2
Online ISBN: 978-3-540-45678-0
eBook Packages: Springer Book Archive