PL EN


Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników
Tytuł artykułu

Co-Finiteness and Co-Emptiness of Reachability Sets in Vector Addition Systems with States

Wybrane pełne teksty z tego czasopisma
Identyfikatory
Warianty tytułu
Języki publikacji
EN
Abstrakty
EN
The boundedness problem is a well-known exponential-space complete problem for vector addition systems with states (or Petri nets); it asks if the reachability set (for a given initial configuration) is finite. Here we consider a dual problem, the co-finiteness problem that asks if the complement of the reachability set is finite; by restricting the question we get the co-emptiness (or universality) problem that asks if all configurations are reachable. We show that both the co-finiteness problem and the co-emptiness problem are exponential-space complete. While the lower bounds are obtained by a straightforward reduction from coverability, getting the upper bounds is more involved; in particular we use the bounds derived for reversible reachability by Leroux (2013). The studied problems were motivated by a result for structural liveness of Petri nets; this problem was shown decidable by Jančar (2017), without clarifying its complexity. The structural liveness problem is tightly related to a generalization of the co-emptiness problem, where the sets of initial configurations are (possibly infinite) downward closed sets instead of just singletons. We formulate the problems even more generally, for semilinear sets of initial configurations; in this case we show that the co-emptiness problem is decidable (without giving an upper complexity bound), and we formulate a conjecture under which the co-finiteness problem is also decidable.
Wydawca
Rocznik
Strony
123--150
Opis fizyczny
Bibliogr. 20 poz., rys., tab.
Twórcy
autor
  • Department of Computer Science, Faculty of Science, Palacký University, Olomouc, Czechia
  • Univ. Bordeaux, CNRS, Bordeaux INP, LaBRI, UMR 5800, F-33400, Talence, France
  • Univ. Bordeaux, CNRS, Bordeaux INP, LaBRI, UMR 5800, F-33400, Talence, France
Bibliografia
  • [1] Jančar P. Deciding Structural Liveness of Petri Nets. In: SOFSEM 2017, volume 10139 of LNCS. Springer, 2017 pp. 91-102. doi:10.1007/978-3-319-51963-0_8.
  • [2] Best E, Esparza J. Existence of home states in Petri nets is decidable. Inf. Process. Lett., 2016. 116(6):423-427. URL https://doi.org/10.1016/j.ipl.2016.01.011.
  • [3] Leroux J. Presburger Vector Addition Systems. In: LICS 2013. IEEE Computer Society, 2013 pp. 23-32. doi:10.1109/LICS.2013.7.
  • [4] Leroux J, Schmitz S. Reachability in Vector Addition Systems is Primitive-Recursive in Fixed Dimension. In: LICS 2019. IEEE Computer Society, 2019. URL http://arxiv.org/abs/1903.08575.
  • [5] Czerwinski W, Lasota S, Lazic R, Leroux J, Mazowiecki F. The Reachability Problem for Petri Nets is Not Elementary (Extended Abstract). In: STOC 2019. ACM, 2019 pp. 24-33. doi:10.1145/3313276.3316369.
  • [6] Rackoff C. The Covering and Boundedness Problems for Vector Addition Systems. Theor. Comput. Sci., 1978. 6:223-231. URL https://doi.org/10.1016/0304-3975(78)90036-1.
  • [7] Leroux J. Vector Addition System Reversible Reachability Problem. Logic. Meth. in Comput. Sci., 2013. 9(1). doi:10.2168/LMCS-9(1:5)2013.
  • [8] Ginsburg S, Spanier EH. Semigroups, Presburger formulas, and languages. Pacific J. Math., 1966. 16(2):285-296. URL https://projecteuclid.org/euclid.pjm/1102994974.
  • [9] Hopcroft JE, Pansiot J. On the Reachability Problem for 5-Dimensional Vector Addition Systems. Theor. Comput. Sci., 1979. 8:135-159. URL https://doi.org/10.1016/0304-3975(79)90041-0.
  • [10] Mayr EW. An Algorithm for the General Petri Net Reachability Problem. SIAM J. Comput., 1984. 13(3):441-460. URL https://doi.org/10.1137/0213029.
  • [11] Lipton RJ. The Reachability Problem Requires Exponential Space. Technical Report 63, Department of Computer Science, Yale University, 1976.
  • [12] Presburger M. Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. Comptes Rendus du premier congrès de mathématiciens des Pays Slaves, Warszawa, 1929. pp. 92-101.
  • [13] Finkel A, Leroux J. How to Compose Presburger-Accelerations: Applications to Broadcast Protocols. In: FST TCS 2002, volume 2556 of LNCS. Springer, 2002 pp. 145-156. doi:10.1007/3-540-36206-1_14.
  • [14] Kleine Büning H, Lettmann T, Mayr EW. Projections of Vector Addition System Reachability Sets are Semilinear. Theor. Comput. Sci., 1989. 64(3):343-350. URL https://doi.org/10.1016/0304-3975(89)90055-8.
  • [15] Abdulla PA, Cerans K, Jonsson B, Tsay Y. Algorithmic Analysis of Programs with Well Quasi-ordered Domains. Inf. Comput., 2000. 160(1-2):109-127. URL https://doi.org/10.1006/inco.1999.2843.
  • [16] Finkel A, Schnoebelen P. Well-structured transition systems everywhere! Theor. Comput. Sci., 2001. 256(1-2):63-92. URL https://doi.org/10.1016/S0304-3975(00)00102-X.
  • [17] Esparza J. Decidability and Complexity of Petri Net Problems—An Introduction, volume 1491 of LNCS, pp. 374-428. Springer, 1998. doi:10.1007/3-540-65306-6_20.
  • [18] Yen H. A Unified Approach for Deciding the Existence of Certain Petri Net Paths. Inf. Comput., 1992. 96(1):119-137. URL https://doi.org/10.1016/0890-5401(92)90059-0.
  • [19] Atig MF, Habermehl P. On Yen’s Path Logic for Petri Nets. Int. J. Found. Comput. Sci., 2011. 22(4):783-799. URL https://doi.org/10.1142/S0129054111008428.
  • [20] Hack M. The Recursive Equivalence of the Reachability Problem and the Liveness Problem for Petri Nets and Vector Addition Systems. In: SWAT 1974. IEEE Computer Society, 1974 pp. 156-164. doi:10.1109/SWAT.1974.28.
Uwagi
Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2019).
Typ dokumentu
Bibliografia
Identyfikator YADDA
bwmeta1.element.baztech-1e54e943-6b21-4f52-9751-b4700f0e6409
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ć.