The Reachability Problem for Two-Dimensional Vector Addition Systems with States

被引：4

作者：

Blondin, Michael ^{[1
]}

Englert, Matthias ^{[2
]}

Finkel, Alain ^{[3
]}

Goeller, Stefan ^{[4
]}

Haase, Christoph ^{[5
]}

Lazic, Ranko ^{[2
]}

Mckenzie, Pierre ^{[6
]}

Totzke, Patrick ^{[7
]}

机构：

[1] Univ Sherbrooke, 2500 Blvd Univ, Sherbrooke, PQ J1K 2R1, Canada

[2] Univ Warwick, Coventry CV4 7AL, W Midlands, England

[3] Univ Paris Saclay, Lab LMF, IUF, CNRS,ENS Paris Saclay, 4 Ave Sci,CS 30008, F-91192 Gif Sur Yvette, France

[4] Univ Kassel, Wilhelmshoher Allee 73, D-34121 Kassel, Germany

[5] Univ Oxford, Parks Rd, Oxford OX1 3QD, England

[6] Univ Montreal, CP 6128 Succ Ctr Vile, Montreal, PQ H3C 3J7, Canada

[7] Univ Liverpool, Dept Comp Sci, Ashton Bldg,Ashton St, Liverpool L69 3BX, Merseyside, England

来源：

JOURNAL OF THE ACM | 2021年 / 68卷 / 05期

基金：

英国工程与自然科学研究理事会; 加拿大自然科学与工程研究理事会;

关键词：

Vector addition systems with states; Petri nets; semi-linear sets; linear path schemes; reachability; BOUNDS;

D O I：

10.1145/3464794

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

We prove that the reachability problem for two-dimensional vector addition systems with states is NL-complete or PSPACE-complete, depending on whether the numbers in the input are encoded in unary or binary. As a key underlying technical result, we show that, if a configuration is reachable, then there exists a witnessing path whose sequence of transitions is contained in a bounded language defined by a regular expression of pseudo-polynomially bounded length. This, in turn, enables us to prove that the lengths of minimal reachability witnesses are pseudo-polynomially bounded.

引用

页数：41

共 42 条

[1] PERSISTENCE RESULTS FOR CHEMICAL REACTION NETWORKS WITH TIME-DEPENDENT KINETICS AND NO GLOBAL CONSERVATION LAWS
Angeli, David
De Leenheer, Patrick
Sontag, Eduardo D.
[J]. SIAM JOURNAL ON APPLIED MATHEMATICS, 2011, 71 (01) : 128 - 146
[2] Petri nets for modelling metabolic pathways: a survey
Baldan, Paolo
Cocco, Nicoletta
Marin, Andrea
Simeoni, Marta
[J]. NATURAL COMPUTING, 2010, 9 (04) : 955 - 989
[3] Reachability in Two-Dimensional Vector Addition Systems with States is PSPACE-complete
Blondin, Michael
Finkel, Alain
Goeller, Stefan
Haase, Christoph
McKenzie, Pierre
[J]. 2015 30TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2015, : 32 - 43
[4] Böhm S, 2013, STOC'13: PROCEEDINGS OF THE 2013 ACM SYMPOSIUM ON THEORY OF COMPUTING, P131
[5] Long-Run Average Behaviour of Probabilistic Vector Addition Systems
Brazdil, Tomas
Kiefer, Stefan
Kucera, Antonin
Novotny, Petr
[J]. 2015 30TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2015, : 44 - 55
[6] Cardoza E., 1976, STOC 1976: Proceedings of the 8th annual ACM Symposium on Theory of Computing, P50, DOI DOI 10.1145/800113.803630
[7] SHORTEST PATHS IN ONE-COUNTER SYSTEMS
Chistikov, Dmitry
Czerwinski, Wojciech
Hofman, Piotr
Pilipczuk, Michal
Wehar, Michael
[J]. LOGICAL METHODS IN COMPUTER SCIENCE, 2019, 15 (01) : 19:1 - 19:28
[8] The Reachability Problem for Petri Nets Is Not Elementary
Czerwinski, Wojciech
Lasota, Slawomir
Lazic, Ranko
Leroux, Jerome
Mazowiecki, Filip
[J]. PROCEEDINGS OF THE 51ST ANNUAL ACM SIGACT SYMPOSIUM ON THEORY OF COMPUTING (STOC '19), 2019, : 24 - 33
[9] Czerwinski W, 2017, IEEE S LOG
[10] Czerwinski Wojciech, 2019, SCHLOSS DAGSTUHL LEI, V138, DOI [10. 4230/LIPIcs.MFCS.2019.62, DOI 10.4230/LIPICS.MFCS.2019.62]

← 1 2 3 4 5 →