×

zbMATH — the first resource for mathematics

Reachability relations of timed pushdown automata. (English) Zbl 07304648
Summary: Timed pushdown automata (TPDA) are an expressive formalism combining recursion with a rich logic of timing constraints. We prove that reachability relations of TPDA are expressible in linear arithmetic, a rich logic generalising Presburger arithmetic and rational arithmetic. The main technical ingredients are a novel quantifier elimination result for clock constraints (used to simplify the syntax of TPDA transitions), the use of clock difference relations to express reachability relations of the fractional clock values, and an application of Parikh’s theorem to reconstruct the integral clock values.
MSC:
68 Computer science
Software:
Kronos; Uppaal
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] (2016)
[2] Abdulla, P. A.; Atig, M. F.; Stenman, J., Dense-timed pushdown automata, (Proc. LICS’12 (2012), IEEE), 35-44 · Zbl 1360.68535
[3] Akshay, S.; Gastin, P.; Jugé, V.; Krishna, S. N., Timed systems through the lens of logic, (Proc. of LICS’19 (2019)), 1-13
[4] Akshay, S.; Gastin, P.; Krishna, S. N., Analyzing timed systems using tree automata, Log. Methods Comput. Sci., 14, 2 (2018) · Zbl 1398.68290
[5] Alur, R.; Dill, D. L., A theory of timed automata, Theor. Comput. Sci., 126, 183-235 (1994) · Zbl 0803.68071
[6] Alur, R.; Fix, L.; Henzinger, T. A., Event-clock automata: a determinizable class of timed automata, Theor. Comput. Sci., 211, 253-273 (1999) · Zbl 0912.68132
[7] Alur, R.; Madhusudan, P., Visibly pushdown languages, (STOC’04. STOC’04, STOC ’04 (2004), ACM: ACM New York, NY, USA), 202-211 · Zbl 1192.68396
[8] Behrmann, G.; David, A.; Larsen, K. G.; Hakansson, J.; Petterson, P.; Yi, W.; Hendriks, M., Uppaal 4.0, (Proceedings of the 3rd International Conference on the Quantitative Evaluation of Systems. Proceedings of the 3rd International Conference on the Quantitative Evaluation of Systems, QEST ’06 (2006), IEEE Computer Society: IEEE Computer Society Washington, DC, USA), 125-126
[9] Benerecetti, M.; Minopoli, S.; Peron, A., Analysis of timed recursive state machines, (Proc. TIME’10 (2010), IEEE), 61-68
[10] Bengtsson, J.; Jonsson, B.; Lilius, J.; Yi, W., Partial order reductions for timed systems, (Proc. of CONCUR’98. Proc. of CONCUR’98, CONCUR ’98 (1998), Springer-Verlag: Springer-Verlag London, UK), 485-500
[11] Bérard, B.; Petit, A.; Diekert, V.; Gastin, P., Characterization of the expressive power of silent transitions in timed automata, Fundam. Inform., 36, 2-3, 145-182 (1998) · Zbl 0930.68077
[12] Bhave, D.; Dave, V.; Krishna, S. N.; Phawade, R.; Trivedi, A., A logical characterization for dense-time visibly pushdown automata, (Dediu, A.-H.; Janoušek, J.; Martín-Vide, C.; Truthe, B., Proc. of LATA’16 (2016), Springer), 89-101 · Zbl 1435.68144
[13] Bhave, D.; Dave, V.; Krishna, S. N.; Phawade, R.; Trivedi, A., A perfect class of context-sensitive timed languages, (Brlek, S.; Reutenauer, C., Proc. of DLT’16 (2016), Springer: Springer Berlin, Heidelberg), 38-50 · Zbl 1436.68161
[14] Bhave, D.; Krishna, S. N.; Phawade, R.; Trivedi, A., On timed scope-bounded context-sensitive languages, (Hofman, P.; Skrzypczak, M., Proc. of DLT’19 (2019), Springer International Publishing: Springer International Publishing Cham), 168-181 · Zbl 07117544
[15] Boigelot, B.; Jodogne, S.; Wolper, P., An effective decision procedure for linear arithmetic over the integers and reals, ACM Trans. Comput. Log., 6, 3, 614-633 (2005) · Zbl 1407.03052
[16] Bojańczyk, M.; Lasota, S., A machine-independent characterization of timed languages, (Proc. of ICALP’12. Proc. of ICALP’12, ICALP’12 (2012), Springer-Verlag: Springer-Verlag Berlin, Heidelberg), 92-103 · Zbl 1367.68159
[17] Bouajjani, A.; Echahed, R.; Robbana, R., On the automatic verification of systems with continuous variables and unbounded discrete data structures, (Proc. Hybrid Systems ’94. Proc. Hybrid Systems ’94, LNCS, vol. 999 (1995), Springer), 64-85
[18] Cai, X.; Ogawa, M., Well-structured pushdown system: case of dense timed pushdown automata, (Proc. of FLOPS’14 (2014)) · Zbl 1417.68080
[19] Chandra, A. K.; Kozen, D. C.; Stockmeyer, L. J., Alternation J. ACM, 28, 1, 114-133 (1981) · Zbl 0473.68043
[20] Choffrut, C.; Goldwurm, M., Timed automata with periodic clock constraints, J. Autom. Lang. Comb., 5, 4, 371-403 (2000) · Zbl 0964.68076
[21] Clemente, L.; Hofman, P.; Totzke, P., Timed basic parallel processes, (Fokkink, W.; van Glabbeek, R., Proc. of CONCUR’19. Proc. of CONCUR’19, LIPIcs, vol. 140 (2019), Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik: Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik Dagstuhl, Germany), 15:1-15:16
[22] Clemente, L.; Lasota, S., Reachability analysis of first-order definable pushdown systems, (Proc. of CSL’15. Proc. of CSL’15, Dagstuhl. Proc. of CSL’15. Proc. of CSL’15, Dagstuhl, LIPIcs, vol. 41 (2015)), 244-259 · Zbl 1373.68280
[23] Clemente, L.; Lasota, S., Timed pushdown automata revisited, (Proc. LICS’15 (2015), IEEE), 738-749 · Zbl 1401.68157
[24] Clemente, L.; Lasota, S., Binary reachability of timed pushdown automata via quantifier elimination, (Chatzigiannakis, I.; Kaklamanis, C.; Marx, D.; Sannella, D., Proc. of ICALP’18. Proc. of ICALP’18, Dagstuhl, Germany, vol. 107 (2018), Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik), 118:1-118:14
[25] Clemente, L.; Lasota, S.; Lazić, R.; Mazowiecki, F., Timed pushdown automata and branching vector addition systems, (Proc. of LICS’17 (2017))
[26] Clemente, L.; Lasota, S.; Lazić, R.; Mazowiecki, F., Binary reachability of timed-register pushdown automata and branching vector addition systems, ACM Trans. Comput. Log., 20, 3, 14:1-14:31 (2019) · Zbl 1433.68194
[27] Comon, H.; Jurski, Y., Timed automata and the theory of real numbers, (Proc. of CONCUR’99. Proc. of CONCUR’99, CONCUR ’99 (1999), Springer-Verlag: Springer-Verlag London, UK), 242-257 · Zbl 0940.68092
[28] Dang, Z., Binary reachability analysis of pushdown timed automata with dense clocks, (Proc. of CAV’01. Proc. of CAV’01, CAV ’01 (2001), Springer-Verlag: Springer-Verlag London, UK), 506-518 · Zbl 0991.68035
[29] Dang, Z., Pushdown timed automata: a binary reachability characterization and safety verification, Theor. Comput. Sci., 302, 1-3, 93-121 (2003) · Zbl 1044.68085
[30] Dang, Z.; Ibarra, O. H.; Bultan, T.; Kemmerer, R. A.; Su, J., Binary reachability analysis of discrete pushdown timed automata, (Emerson, E. A.; Sistla, A. P., Proc. of CAV 2000. Proc. of CAV 2000, Berlin, Heidelberg (2000)), 69-84 · Zbl 0974.68085
[31] Dima, C., Computing reachability relations in timed automata, (Proc. of LICS’02 (2002)), 177-186
[32] Droste, M.; Perevoshchikov, V., A logical characterization of timed pushdown languages, (Beklemishev, L. D.; Musatov, D. V., Proc. of CSR’15. Proc. of CSR’15, LNCS, vol. 9139 (2015), Springer), 189-203 · Zbl 06496822
[33] Emmi, M.; Majumdar, R., Decision problems for the verification of real-time software, (Hespanha, J.; Tiwari, A., Proc. of HSCC’06. Proc. of HSCC’06, LNCS, vol. 3927 (2006), Springer), 200-211 · Zbl 1178.68340
[34] Esparza, J.; Kucera, A.; Schwoon, S., Model checking ltl with regular valuations for pushdown systems, Inf. Comput., 186, 2, 355-376 (2003) · Zbl 1078.68081
[35] Fearnley, J.; Jurdzinski, M., Reachability in two-clock timed automata is PSPACE-complete, Inf. Comput., 243, 26-36 (2015) · Zbl 1345.68155
[36] Ferrante, J.; Rackoff, C., A decision procedure for the first order theory of real addition with order, SIAM J. Comput., 4, 1, 69-76 (1975) · Zbl 0294.02022
[37] Fränzle, M.; Quaas, K.; Shirmohammadi, M.; Worrell, J., Effective definability of the reachability relation in timed automata, Inf. Process. Lett., 153 (2020) · Zbl 07134468
[38] Fribourg, L., A closed-form evaluation for extended timed automata (1998), CNRS & Ecole Normale Superieure de Cachan, Technical report
[39] Fribourg, L., Constraint logic programming applied to model checking, (Bossi, A., Logic-Based Program Synthesis and Transformation (2000), Springer Berlin Heidelberg: Springer Berlin Heidelberg Berlin, Heidelberg), 30-41 · Zbl 0964.68555
[40] Garey, M.; Johnson, D., Computers and Intractability (1979), W. H. Freeman & Co.: W. H. Freeman & Co. New York
[41] Gastin, P.; Mukherjee, S.; Srivathsan, B., Reachability in timed automata with diagonal constraints, (Schewe, S.; Zhang, L., Proc. of CONCUR’18. Proc. of CONCUR’18, Dagstuhl, Germany. Proc. of CONCUR’18. Proc. of CONCUR’18, Dagstuhl, Germany, Leibniz International Proceedings in Informatics (LIPIcs), vol. 118 (2018), Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik), 28:1-28:17
[42] Gastin, P.; Mukherjee, S.; Srivathsan, B., Fast algorithms for handling diagonal constraints in timed automata, (Dillig, I.; Tasiran, S., Computer Aided Verification (2019), Springer International Publishing: Springer International Publishing Cham), 41-59
[43] Ginsburg, S.; Spanier, E. H., Semigroups, presburger formulas, and languages, Pac. J. Math., 16, 2, 285-296 (1966) · Zbl 0143.01602
[44] Govind, R.; Herbreteau, F.; Srivathsan, B.; Walukiewicz, I., Revisiting local time semantics for networks of timed automata (2019), arXiv e-prints
[45] Herbreteau, F.; Srivathsan, B.; Walukiewicz, I., Better abstractions for timed automata, Inf. Comput., 251, 67-90 (2016) · Zbl 1353.68166
[46] Heußner, A.; Leroux, J.; Muscholl, A.; Sutre, G., Reachability analysis of communicating pushdown systems, Log. Methods Comput. Sci., 8, 3, 1-20 (2012) · Zbl 1248.68330
[47] Koubarakis, M., Complexity results for first-order theories of temporal constraints, (Doyle, J.; Sandewall, E.; Torasso, P., Principles of Knowledge Representation and Reasoning. Principles of Knowledge Representation and Reasoning, The Morgan Kaufmann Series in Representation and Reasoning (1994), Morgan Kaufmann), 379-390
[48] Kozen, D., Lower bounds for natural proof systems, (Proc. of FOCS’77. Proc. of FOCS’77, SFCS ’77 (1977), IEEE Computer Society: IEEE Computer Society Washington, DC, USA), 254-266
[49] Krčál, P.; Pelánek, R., On sampled semantics of timed systems, (Sarukkai, S.; Sen, S., Proc. of FSTTCS’05. Proc. of FSTTCS’05, LNCS, vol. 3821 (2005), Springer), 310-321 · Zbl 1172.68537
[50] Krcal, P.; Yi, W., Communicating timed automata: the more synchronous, the more difficult to verify, (Proc. of CAV’06. Proc. of CAV’06, LNCS (2006), Springer-Verlag: Springer-Verlag Berlin, Heidelberg), 249-262 · Zbl 1188.68192
[51] Krishna, S. N.; Manasa, L.; Trivedi, A., Time-bounded reachability problem for recursive timed automata is undecidable, (Dediu, A.-H.; Formenti, E.; Martín-Vide, C.; Truthe, B., Proc. of LATA’15 (2015), Springer: Springer Cham), 237-248 · Zbl 1451.68151
[52] Krishna, S. N.; Manasa, L.; Trivedi, A., What’s decidable about recursive hybrid automata?, (Proc. of HSCC’15. Proc. of HSCC’15, HSCC ’15 (2015), ACM: ACM New York, NY, USA), 31-40 · Zbl 1364.68254
[53] Laroussinie, F.; Markey, N.; Schnoebelen, P., Model checking timed automata with one or two clocks, (Proc. of CONCUR’04. Proc. of CONCUR’04, LNCS, vol. 3170 (2004)), 387-401 · Zbl 1099.68057
[54] Li, G.; Cai, X.; Ogawa, M.; Yuen, S., Nested timed automata, (Proc. of FORMATS’13. Proc. of FORMATS’13, LNCS (2013), Springer), 168-182 · Zbl 1390.68407
[55] M’Hemdi, H.; Julliand, J.; Masson, P. A.; Robbana, R., Test generation from timed pushdown automata with inputs and outputs, (ICSTW’15 (2015)), 1-10
[56] M’Hemdi, H.; Julliand, J.; Masson, P.-A.; Robbana, R., Conformance testing for timed recursive programs, (Lee, R., Computer and Information Science 2015 (2016), Springer International Publishing: Springer International Publishing Cham), 203-219
[57] Minsky, M. L., Recursive unsolvability of post’s problem of “tag” and other topics in theory of turing machines, Ann. Math., 74, 3, 437-455 (1961) · Zbl 0105.00802
[58] Murawski, A.; Ramsay, S.; Tzevelekos, N., Reachability in pushdown register automata, J. Comput. Syst. Sci., 87, 58-83 (2017) · Zbl 1370.68185
[59] Parikh, R. J., On context-free languages, J. ACM, 13, 4, 570-581 (1966) · Zbl 0154.25801
[60] Pratt, V. R., Two easy theories whose combination is hard (1977), MIT, Technical report
[61] Presburger, M., Über der vollständigkeit eines gewissen systems der arithmetik ganzer zahlen, in welchen die addition als einzige operation hervortritt, Comptes Rendus Premier Congrès des Mathématicienes des Pays Slaves, 395, 92-101 (1930) · JFM 56.0825.04
[62] Quaas, K., Verification for timed automata extended with unbounded discrete data structures, Log. Methods Comput. Sci., 11, 3 (2015) · Zbl 1448.68314
[63] Quaas, K.; Shirmohammadi, M.; Worrell, J., Revisiting reachability in timed automata, (Proc. of LICS’17 (2017)), 1-12
[64] Sontag, E. D., Real addition and the polynomial hierarchy, Inf. Process. Lett., 20, 3, 115-120 (1985) · Zbl 0575.03030
[65] Tang, N.; Ogawa, M., Event-clock visibly pushdown automata, (Proc. of SOFSEM ’09. Proc. of SOFSEM ’09, SOFSEM ’09 (2009), Springer-Verlag: Springer-Verlag Berlin, Heidelberg), 558-569 · Zbl 1206.68183
[66] Trivedi, A.; Wojtczak, D., Recursive timed automata, (Proc. ATVA’10. Proc. ATVA’10, LNCS, vol. 6252 (2010), Springer), 306-324 · Zbl 1305.68115
[67] Uezato, Y.; Minamide, Y., Pushdown systems with stack manipulation, (Van Hung, D.; Ogawa, M., Proc. of ATVA’13 (2013), Springer), 412-426 · Zbl 1374.68302
[68] Uezato, Y.; Minamide, Y., Synchronized recursive timed automata, (Proc. of LPAR’15 (2015)) · Zbl 06528786
[69] Verma, K. N.; Seidl, H.; Schwentick, T., On the complexity of equational Horn clauses, (Proc. CADE-20, 2005 (2005)), 337-352 · Zbl 1135.94331
[70] Weispfenning, V., The complexity of linear problems in fields, J. Symb. Comput., 5, 1, 3-27 (1988) · Zbl 0646.03005
[71] Weispfenning, V., Mixed real-integer linear quantifier elimination, (Proc. of ISSAC’99 (1999), ACM: ACM New York, NY, USA), 129-136
[72] Yovine, S., Kronos: a verification tool for real-time systems, Int. J. Softw. Tools Technol. Transf., 1, 1, 123-133 (1997) · Zbl 1060.68606
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.