Reachability in Vector Addition Systems is Primitive-Recursive in Fixed Dimension
| Autor: | Sylvain Schmitz, Jérôme Leroux |
|---|---|
| Přispěvatelé: | Laboratoire Bordelais de Recherche en Informatique (LaBRI), Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Institut Universitaire de France (IUF), Ministère de l'Education nationale, de l’Enseignement supérieur et de la Recherche (M.E.N.E.S.R.), ANR-14-CE28-0005,PRODAQ,Systèmes de preuves pour requêtes avec données(2014), ANR-17-CE40-0028,BRAVAS,IDEAL-BASED ALGORITHMS FOR VASSES AND WELL-STRUCTURED SYSTEMS(2017) |
| Jazyk: | angličtina |
| Rok vydání: | 2019 |
| Předmět: |
Discrete mathematics
Computer Science - Logic in Computer Science Reachability problem [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] 0102 computer and information sciences 02 engineering and technology Petri net Decision problem fast-growing complexity 01 natural sciences Ackermann function Upper and lower bounds Dimension (vector space) 010201 computation theory & mathematics Reachability 0202 electrical engineering electronic engineering information engineering Primitive recursive function 020201 artificial intelligence & image processing vector addition system Mathematics reachability |
| Zdroj: | LICS 2019, 34th Annual ACM/IEEE Symposium on Logic in Computer Science LICS 2019, 34th Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2019, Vancouver, Canada. pp.1--13, ⟨10.1109/LICS.2019.8785796⟩ LICS |
| DOI: | 10.1109/LICS.2019.8785796⟩ |
| Popis: | International audience; The reachability problem in vector addition systems is a central question, not only for the static verification of these systems, but also for many inter-reducible decision problems occurring in various fields. The currently best known upper bound on this problem is not primitive-recursive, even when considering systems of fixed dimension. We provide significant refinements to the classical decomposition algorithm of Mayr, Kosaraju, and Lambert and to its termination proof, which yield an ACKERMANN upper bound in the general case, and primitive-recursive upper bounds in fixed dimension. While this does not match the currently best known TOWER lower bound for reachability, it is optimal for related problems. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|