Nowa wersja platformy jest już dostępna.
Przejdź na https://bibliotekanauki.pl

PL EN


Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników
2016 | Vol. 143, nr 3/4 | 317--338
Tytuł artykułu

Relating Reachability Problems in Timed and Counter Automata

Warianty tytułu
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.
Wydawca

Rocznik
Strony
317--338
Opis fizyczny
Bibliogr. 26 poz., rys.
Twórcy
autor
  • 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 , haase@lsv.ens-cachan.fr
autor
autor
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.
Typ dokumentu
Bibliografia
Identyfikatory
Identyfikator YADDA
bwmeta1.element.baztech-d5ddb938-d9a1-48a7-a723-e65a0f850756
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.