Relating Reachability Problems in Timed and Counter Automata

• Autorzy: Haase C. , Ouaknine J. , Worrell J.

Identyfikatory

DOI

10.3233/FI-2016-1316

• Języki publikacji: EN

Abstrakty

EN

We establish a relationship between reachability problems in timed automata and spacebounded counter automata. We show that reachability in timed automata with three or more clocks is logarithmic-space inter-reducible with reachability in space-bounded counter automata with two counters. We moreover show the logarithmic-space equivalence of reachability in two-clock timed automata and space-bounded one-counter automata. This last reduction has recently been employed by Fearnley and Jurdziński to settle the computational complexity of reachability in two-clock timed automata.

Słowa kluczowe

EN

timed automata; counter automata; reachability; infinite-state systems

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2016
• Tom: Vol. 143, nr 3/4
• Strony: 317--338
• Opis fizyczny: Bibliogr. 26 poz., rys.

Twórcy

autor

Haase C.

• Laboratoire Spécification et Vérification (LSV), CNRS École Normale Supérieure (ENS) de Cachan 61, avenue du Président Wilson, 94235 Cachan Cedex, France

autor

Ouaknine J.

• Department of Computer Science, University of Oxford, Parks Rd, OX1 3QD, Oxford, United Kingdom

autor

Worrell J.

• Department of Computer Science, University of Oxford, Parks Rd, OX1 3QD, Oxford, United Kingdom

Bibliografia

• [1] Haase C. On the Complexity of Model Checking Counter Automata. University of Oxford, UK; 2012.
• [2] Alur R, Dill DL. A theory of timed automata. Theoretical computer science. 1994;126(2):183–235. doi:10.1016/0304-3975(94)90010-8.
• [3] Minsky ML. Computation: Finite and Infinite Machines. Prentice-Hall; 1967. ISBN:0-13-165563-9.
• [4] Haase C, Ouaknine J, Worrell J. On the Relationship between Reachability Problems in Timed and Counter Automata. In: Finkel A, Leroux J, Potapov I, editors. Reachability Problems. vol. 7550 of Lecture Notes in Computer Science. Springer Berlin Heidelberg; 2012. p. 54–65. doi:10.1007/978-3-642-33512-9-6.
• [5] Fearnley J, Jurdziński M. Reachability in Two-Clock Timed Automata Is PSPACE-Complete. In: Fomin FV, Freivalds R, Kwiatkowska M, Peleg D, editors. Automata, Languages, and Programming. vol. 7966 of Lecture Notes in Computer Science. Springer Berlin Heidelberg; 2013. p. 212–223. doi:10.1007/978-3-642-39212-2 21.
• [6] Abdulla PA, Deneux J, Ouaknine J, Worrell J. Decidability and Complexity Results for Timed Automata via Channel Machines. In: Caires L, Italiano GF, Monteiro L, Palamidessi C, Yung M, editors. Automata, Languages and Programming. vol. 3580 of Lecture Notes in Computer Science. Springer Berlin Heidelberg; 2005. p. 1089–1101. doi:10.1007/11523468 88.
• [7] Bouyer P, Markey N, Reynier PA. Robust Analysis of Timed Automata Via Channel Machines. In: Amadio R, editor. Foundations of Software Science and Computational Structures. vol. 4962 of Lecture Notes in Computer Science. Springer Berlin Heidelberg; 2008. p. 157–171. doi:10.1007/978-3-540-78499-9 12.
• [8] Demri S, Gascon R. The Effects of Bounding Syntactic Resources on Presburger LTL. Journal of Logic and Computation. 2009;19(6):1541–1575. doi:10.1093/logcom/exp037.
• [9] Courcoubetis C, Yannakakis M. Minimum and maximum delay problems in real-time systems. Formal Methods in System Design. 1992;1(4):385–415. doi:10.1007/BF00709157.
• [10] Laroussinie F, Markey N, Schnoebelen Ph. Model Checking Timed Automata with One or Two Clocks. In: Gardner P, Yoshida N, editors. CONCUR 2004 - Concurrency Theory. vol. 3170 of Lecture Notes in Computer Science. Springer Berlin Heidelberg; 2004. p. 387–401. doi:10.1007/978-3-540-28644-8 25.
• [11] Naves G. Accessibilité dans les automates temporisés à deux horloges [Rapport de Master]. MPRI, Paris, France; 2006.
• [12] Göller S, Lohrey M. Branching-Time Model Checking of One-Counter Processes and Timed Automata. SIAM Journal on Computing. 2013;42(3):884–923. doi:10.1137/120876435.
• [13] Rosier LE, Yen HC. A multiparameter analysis of the boundedness problem for vector addition systems. Journal of Computer and System Sciences. 1986;32(1):105–135. doi:10.1016/0022-0000(86)90006-1.
• [14] Haase C, Kreutzer S, Ouaknine J,Worrell J. Reachability in Succinct and Parametric One-Counter Automata. In: Bravetti M, Zavattaro G, editors. CONCUR 2009 - Concurrency Theory. vol. 5710 of Lecture Notes in Computer Science. Springer Berlin Heidelberg; 2009. p. 369–383. doi:10.1007/978-3-642-04081-8 25.
• [15] Mayr EW. An algorithm for the general Petri net reachability problem. In: ACM Symposium on Theory of Computing. New York, NY, USA: ACM; 1981. p. 238–246. doi:10.1145/800076.802477.
• [16] Lambert JL. A structure to decide reachability in Petri nets. Theoretical Computer Science. 1992;99(1):79–104. doi:10.1016/0304-3975(92)90173-D.
• [17] Reinhardt K. Reachability in Petri Nets with Inhibitor Arcs. Electronic Notes in Theoretical Computer Science. 2008;223(0):239–264. doi:10.1016/j.entcs.2008.12.042.
• [18] Leroux J. Vector Addition Systems Reachability Problem (A Simpler Solution). In: Voronkov A, editor. Turing-100. The Alan Turing Centenary. vol. 10 of EPiC Series in Computer Science. EasyChair; 2012. p. 214–228. ISSN:2040-557X. Available from: EasyChair,http://www.easychair.org.
• [19] Bonnet R. The Reachability Problem for Vector Addition System with One Zero-Test. In: Murlak F, Sankowski P, editors. Mathematical Foundations of Computer Science 2011. vol. 6907 of Lecture Notes in Computer Science. Springer Berlin Heidelberg; 2011. p. 145–157. doi:10.1007/978-3-642-22993-0 16.
• [20] Ibarra OH. Reversal-Bounded Multicounter Machines and Their Decision Problems. Journal of the ACM. 1978;25(1):116–133. doi:10.1145/322047.322058.
• [21] Finkel A, Sangnier A. Reversal-Bounded Counter Machines Revisited. In: Ochmański E, Tyszkiewicz J, editors. Mathematical Foundations of Computer Science 2008. vol. 5162 of Lecture Notes in Computer Science. Springer Berlin Heidelberg; 2008. p. 323–334. doi:10.1007/978-3-540-85238-4 26.
• [22] Leroux J, Sutre G. Flat Counter Automata Almost Everywhere! In: Peled DA, Tsay YK, editors. Automated Technology for Verification and Analysis. vol. 3707 of Lecture Notes in Computer Science. Springer Berlin Heidelberg; 2005. p. 489–503. doi:10.1007/11562948 36.
• [23] Bouyer P, Fahrenberg U, Larsen K, Markey N, Srba J. Infinite Runs in Weighted Timed Automata with Energy Constraints. In: Cassez F, Jard C, editors. Formal Modeling and Analysis of Timed Systems. vol. 5215 of Lecture Notes in Computer Science. Springer Berlin Heidelberg; 2008. p. 33–47. doi:10.1007/978-3-540-85778-5 4.
• [24] Memmi G, Roucairol G. Linear algebra in net theory. In: Brauer W, editor. Net Theory and Applications. vol. 84 of Lecture Notes in Computer Science. Springer Berlin Heidelberg; 1980. p. 213–223. ISBN:3-540-10001-6.
• [25] Alur R, Henzinger TA, Vardi MY. Parametric real-time reasoning. In: ACM Symposium on Theory of Computing. New York, NY, USA: ACM; 1993. p. 592–601. ISBN:0-89791-591-7.
• [26] Hopcroft J, Pansiot JJ. On the reachability problem for 5-dimensional vector addition systems. Theoretical Computer Science. 1979;8(2):135–159. doi:10.1016/0304-3975(79)90041-0.