article

Pushdown timed automata: a binary reachability characterization and safety verification

Author:

Zhe DangAuthors Info & Claims

Theoretical Computer Science, Volume 302, Issue 1-3

Pages 93 - 121

https://doi.org/10.1016/S0304-3975(02)00743-0

Published: 13 June 2003 Publication History

Abstract

We consider pushdown timed automata (PTAs) that are timed automata (with dense clocks) augmented with a pushdown stack. A configuration of a PTA includes a state, dense clock values and a stack word. By using the pattern technique, we give a decidable characterization of the binary reachability (i.e., the set of all pairs of configurations such that one can reach the other) of a PTA. Since a timed automaton can be treated as a PTA without the pushdown stack, we can show that the binary reachability of a timed automaton is definable in the additive theory of reals and integers. The results can be used to verify a class of properties containing linear relations over both dense variables and unbounded discrete variables. The properties previously could not be verified using the classic region technique nor expressed by timed temporal logics for timed automata and CTL* for pushdown systems. The results are also extended to other generalizations of timed automata.

References

[1]

{1} R. Alur, Timed automata, CAV'99, Lecture Notes in Computer Science, Vol. 1633, Springer, Berlin, 1999, pp. 8-22.]]

Digital Library

[2]

{2} R. Alur, C. Courcoibetis, D. Dill, Model-checking in dense real time, Inform. Comput. 104 (1993) 2-34.]]

Digital Library

[3]

{3} R. Alur, D. Dill, A theory of timed automata, Theoret. Comput. Sci. 126 (1994) 183-236.]]

Digital Library

[4]

{4} R. Alur, T. Feder, T.A. Henzinger, The benefits of relaxing punctuality, J. ACM 43 (1996) 116-146.]]

Digital Library

[5]

{5} R. Alur, T.A. Henzinger, Real-time logics: complexity and expressiveness, Inform. Comput. 104 (1993) 35-77.]]

Digital Library

[6]

{6} R. Alur, T.A. Henzinger, A really temporal logic, J. ACM 41 (1994) 181-204.]]

Digital Library

[7]

{7} T. Ball, S.K. Rajamani, Bebop: a symbolic model-checker for Boolean programs, Spin Workshop'00, Lecture Notes in Computer Science, Vol. 1885, Springer, Berlin, 2000, pp. 113-130.]]

Digital Library

[8]

{8} J.R. Buchi, On a decision method in restricted second order arithmetic, Proc. Internat. Congress on Logic, Method, and Philosophy of Sciences. Stanford University Press, Stanford, CA, 1962, pp. 1-12.]]

[9]

{9} B. Boigelot, S. Rassart, P. Wolper, On the expressiveness of real and integer arithmetic automata, ICALP'98, Lecture Notes in Computer Science, Vol. 1443, Springer, Berlin, 1998, pp. 152-163.]]

Digital Library

[10]

{10} A. Bouajjani, R. Echahed, R. Robbana, On the automatic verification of systems with continuous variables and unbounded discrete data structures, in: P.J. Antsaklis, W. Kohn, A. Nerode, S. Sastry (Eds.), Hybrid System II, Lecture Notes in Computer Science, Vol. 999, Springer, Berlin, 1995, pp. 64-85.]]

Digital Library

[11]

{11} A. Bouajjani, J. Esparza, O. Maler, Reachability Analysis of Pushdown Automata: Application to Model-Checking, CONCUR'97, Lecture Notes in Computer Science, Vol. 1243, Springer, Berlin. 1997, pp. 135-150.]]

Digital Library

[12]

{12} M. Bozga, C. Daws, O. Maler, A. Olivero S. Tripakis, S. Yovine, Kronos: A model-checking tool for real-time systems, CAV'98, Lecture Notes in Computer Science, Vol. 1427, Springer, Berlin, 1998, pp. 546-550.]]

Digital Library

[13]

{13} A. Cherubini, L. Breveglieri, C. Citrini, S. Crespi Reghizzi, Multi-push-down languages and grammars, Internat. J. Foundations Comput. Sci. 7 (3) (1996) 253-291.]]

[14]

{14} A. Coen-Porisini, C. Ghezzi, R. Kemmerer, Specification of real-time systems using ASTRAL, IEEE Trans. Software Eng. 23 (1997) 572-598.]]

Digital Library

[15]

{15} H. Comon, V. Cortier, Flatness is not a weakness, CSL'00, Lecture Notes in Computer Science, Vol. 1862, Springer, Berlin, 2000, pp. 262-276.]]

Digital Library

[16]

{16} H. Comon, Y. Jurski, Multiple counters automata, safety analysis and Presburger arithmetic, CAV'98, Lecture Notes in Computer Science, Vol. 1427, Springer, Berlin, 1998, pp. 268-279.]]

Digital Library

[17]

{17} H. Comon, Y. Jurski, Timed automata and the theory of real numbers, CONCUR'99, Lecture Notes in Computer Science, Vol. 1664, Springer, Berlin, 1999, pp. 242-257.]]

Digital Library

[18]

{18} Z. Dang, Debugging and verification of infinite state real-time systems, Ph.D. Dissertation, University of California, Santa Barbara, August 2000.]]

Digital Library

[19]

{19} Z. Dang, Binary reachability analysis of pushdown timed automata with dense clocks, CAV'01, Lecture Notes in Computer Science, Vol. 2102, Springer, Berlin, 2001, pp. 506-517.]]

Digital Library

[20]

{20} Z. Dang, O.H. Ibarra, T. Bultan, R.A. Kemmerer, J. Su, Binary reachability analysis of discrete pushdown timed automata, CAV'00, Lecture Notes in Computer Science, Vol 1855, Springer, Berlin, 2000, pp. 69-84.]]

Digital Library

[21]

{21} Z. Dang, O.H. Ibarra, R.A. Kemmerer, Decidable approximations on generalized and parameterized discrete timed automata, COCOON'01, Lecture Notes in Computer Science, Vol. 2108, Springer, Berlin, 2001, pp. 529-539.]]

Digital Library

[22]

{22} Z. Dang, P. San Pietro, R.A. Kemmerer, On Presburger liveness of discrete timed automata, STACS'01, Lecture Notes in Computer Science, Vol. 2010, Springer, Berlin, 2001, pp. 132-143.]]

Digital Library

[23]

{23} J. Esparza, S. Schwoon, A BDD-based model-checker for recursive programs, CAV'01, Lecture Notes in Computer Science, Vol. 2102, Springer, Berlin, 2001, pp. 324-336.]]

Digital Library

[24]

{24} A. Finkel, B. Willems, P. Wolper, A direct symbolic approach to model checking pushdown systems, Electronic Notes in Theoretical Computer Science, Vol. 9, Elsevier, Amsterdam, 2000.]]

[25]

{25} E. Gurari, O. Ibarra, The complexity of decision problems for finite-turn multicounter machines, J. Comput. System Sci. 22 (1981) 220-229.]]

[26]

{26} T.A. Henzinger, X. Nicollin, J. Sifakis, S. Yovine, Symbolic model checking for real-time systems, Inform. Comput. 111 (1994) 193-244.]]

Digital Library

[27]

{27} T.A. Henzinger, Pei-Hsin Ho, HyTech: the Cornell hybrid technology tool, in: P.J. Antsaklis, W. Kohn, A. Nerode, S. Sastry (Eds.), Hybrid Systems II, Lecture Notes in Computer Science, Vol. 999, Springer, Berlin, 1995, pp. 265-294.]]

Digital Library

[28]

{28} O.H. Ibarra, Reversal-bounded multicounter machines and their decision problems, J. ACM 25 (1978) 116-133.]]

Digital Library

[29]

{29} O.H. Ibarra, T. Jiang, N. Tran, H. Wang, New decidability results concerning two-way counter machines, SIAM J. Comput. 24 (1995) 123-137.]]

Digital Library

[30]

{30} F. Laroussinie, K.G. Larsen, C. Weise, From timed automata to logic--and back, MFCS'95, Lecture Notes in Computer Science, Vol. 969, Springer, Berlin, 1995, pp. 529-539.]]

Digital Library

[31]

{31} K.G. Larsen, G. Behrmann, Ed Brinksma, A. Fehnker, T. Hune, P. Pettersson, J. Romijn, As cheap as possible: efficient cost-optimal reachability for priced timed automata, CAV'01, Lecture Notes in Computer Science, Vol. 2102, Springer, Berlin, 2001, pp. 493-505.]]

Digital Library

[32]

{32} K.G. Larsen, P. Pattersson, W. Yi, UPPAAL in a nutshell, Internat. J. Software Tools Technol. Transfer 1 (1997) 134-152.]]

Digital Library

[33]

{33} M.L. Minsky, Computation: Finite and Infinite Machines, Prentice-Hall, Englewood Cliffs, NJ, 1967.]]

Digital Library

[34]

{34} J. Raskin, P. Schobben, State clock logic: a decidable real-time logic, HART'97, Lecture Notes in Computer Science, Vol. 1201, Springer, Berlin, 1997, pp. 33-47.]]

Digital Library

[35]

{35} T. Wilke, Specifying timed state sequences in powerful decidable logics and timed automata, Lecture Notes in Computer Science, Vol. 863, Springer, Berlin, 1994, pp. 694-715.]]

Digital Library

[36]

{36} S. Yovine, Model checking timed automata, in: G. Rozenberg, F.W. Vaandrager (Eds.), Embedded Systems'98, Lecture Notes in Computer Science, Vol. 1494, Springer, Berlin, 1998, pp. 114-152.]]

Digital Library

Cited By

Bergsträßer PGanardi MLin AZetzsche G(2024)Ramsey Quantifiers in Linear ArithmeticsProceedings of the ACM on Programming Languages10.1145/36328438:POPL(1-32)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632843
Akshay SGastin PPrakash K(2021)Fast Zone-Based Algorithms for Reachability in Pushdown Timed AutomataComputer Aided Verification10.1007/978-3-030-81685-8_30(619-642)Online publication date: 20-Jul-2021
https://dl.acm.org/doi/10.1007/978-3-030-81685-8_30
Menghi CBersani MRossi MPietro P(2020)Model Checking MITL Formulae on Timed AutomataACM Transactions on Computational Logic10.1145/338368721:3(1-44)Online publication date: 17-Apr-2020
https://dl.acm.org/doi/10.1145/3383687
Show More Cited By

Index Terms

Pushdown timed automata: a binary reachability characterization and safety verification

Recommendations

Interrupt Timed Automata: verification and expressiveness

We introduce the class of Interrupt Timed Automata (ITA), a subclass of hybrid automata well suited to the description of timed multi-task systems with interruptions in a single processor environment.

While the reachability problem is undecidable for ...
Past pushdown timed automata and safety verification
Implementation and application automata

We consider past pushdown timed automata that are discrete pushdown timed automata 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 ...
Presburger liveness verification of discrete timed automata

Using an automata-theoretic approach, we investigate the decidability of liveness properties (called Presburger liveness properties) for timed automata when Presburger formulas on configurations are allowed. While the general problem of checking a ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Theoretical Computer Science

Theoretical Computer Science Volume 302, Issue 1-3

13 June 2003

489 pages

ISSN:0304-3975

Issue’s Table of Contents

Publisher

Elsevier Science Publishers Ltd.

United Kingdom

Publication History

Published: 13 June 2003

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

21
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 16 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Bergsträßer PGanardi MLin AZetzsche G(2024)Ramsey Quantifiers in Linear ArithmeticsProceedings of the ACM on Programming Languages10.1145/36328438:POPL(1-32)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632843
Akshay SGastin PPrakash K(2021)Fast Zone-Based Algorithms for Reachability in Pushdown Timed AutomataComputer Aided Verification10.1007/978-3-030-81685-8_30(619-642)Online publication date: 20-Jul-2021
https://dl.acm.org/doi/10.1007/978-3-030-81685-8_30
Menghi CBersani MRossi MPietro P(2020)Model Checking MITL Formulae on Timed AutomataACM Transactions on Computational Logic10.1145/338368721:3(1-44)Online publication date: 17-Apr-2020
https://dl.acm.org/doi/10.1145/3383687
Li XChen TWu ZXia M(2020)Computing Linear Arithmetic Representation of Reachability Relation of One-Counter AutomataDependable Software Engineering. Theories, Tools, and Applications10.1007/978-3-030-62822-2_6(89-107)Online publication date: 24-Nov-2020
https://dl.acm.org/doi/10.1007/978-3-030-62822-2_6
Quaas KShirmohammadi MWorrell JAceto LIngólfsdóttir A(2017)Revisiting reachability in timed automataProceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3329995.3330033(1-12)Online publication date: 20-Jun-2017
https://dl.acm.org/doi/10.5555/3329995.3330033
Cui CDang ZFischer TIbarra O(2017)Information rate of some classes of non-regular languagesInformation and Computation10.1016/j.ic.2017.04.008256:C(45-61)Online publication date: 1-Oct-2017
https://dl.acm.org/doi/10.1016/j.ic.2017.04.008
Benerecetti MPeron A(2016)Timed recursive state machinesTheoretical Computer Science10.1016/j.tcs.2016.02.021625:C(85-124)Online publication date: 25-Apr-2016
https://dl.acm.org/doi/10.1016/j.tcs.2016.02.021
Dang ZFischer THutton WIbarra OLi Q(2016)Quantifying communication in synchronized languagesTheoretical Computer Science10.1016/j.tcs.2016.01.042654:C(33-44)Online publication date: 22-Nov-2016
https://dl.acm.org/doi/10.1016/j.tcs.2016.01.042
Cui CDang ZFischer TIbarra O(2016)Execution information rate for some classes of automataInformation and Computation10.1016/j.ic.2015.11.006246:C(20-29)Online publication date: 1-Feb-2016
https://dl.acm.org/doi/10.1016/j.ic.2015.11.006
Li QDang Z(2015)Sampling automata and programsTheoretical Computer Science10.1016/j.tcs.2015.03.012577:C(125-140)Online publication date: 27-Apr-2015
https://dl.acm.org/doi/10.1016/j.tcs.2015.03.012
Show More Cited By

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents