More Web Proxy on the site http://driver.im/

research-article

Hyper-Ackermannian bounds for pushdown vector addition systems

Authors:

Jérôme Leroux,

Grégoire SutreAuthors Info & Claims

CSL-LICS '14: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

Article No.: 63, Pages 1 - 10

https://doi.org/10.1145/2603088.2603146

Published: 14 July 2014 Publication History

Abstract

This paper studies the boundedness and termination problems for vector addition systems equipped with one stack. We introduce an algorithm, inspired by the Karp & Miller algorithm, that solves both problems for the larger class of well-structured pushdown systems. We show that the worst-case running time of this algorithm is hyper-Ackermannian for pushdown vector addition systems. For the upper bound, we introduce the notion of bad nested words over a well-quasi-ordered set, and we provide a general scheme of induction for bounding their lengths. We derive from this scheme a hyper-Ackermannian upper bound for the length of bad nested words over vectors of natural numbers. For the lower bound, we exhibit a family of pushdown vector addition systems with finite but large reachability sets (hyper-Ackermannian).

References

[1]

P. A. Abdulla, K. Čerāns, B. Jonsson, and Y.-K. Tsay. Algorithmic analysis of programs with well quasi-ordered domains. Inform. Comput., 160(1--2):109--127, 2000.

Digital Library

[2]

P. A. Abdulla, M. F. Atig, G. Delzanno, and A. Podelski. Push-down automata with gap-order constraints. In Selec. FSEN'13, volume 8161 of LNCS, pages 199--216. Springer, 2013.

[3]

R. Alur and P. Madhusudan. Adding nesting structure to words. J. ACM, 56(3):1--16, 2009.

Digital Library

[4]

M. F. Atig and P. Ganty. Approximating petri net reachability along context-free traces. In Proc. FSTTCS'11, volume 13 of LIPIcs, pages 152--163. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2011.

[5]

A. Bouajjani and M. Emmi. Analysis of recursively parallel programs. ACM Trans. Prog. Lang. Syst., 35(3):1--49, 2013.

Digital Library

[6]

X. Cai and M. Ogawa. Well-structured pushdown systems. In Proc. CONCUR'13, volume 8052 of LNCS, pages 121--136. Springer, 2013.

Digital Library

[7]

R. Chadha and M. Viswanathan. Decidability results for well-structured transition systems with auxiliary storage. In Proc. CONCUR'07, volume 4703 of LNCS, pages 136--150. Springer, 2007.

Digital Library

[8]

R. Chadha and M. Viswanathan. Deciding branching time properties for asynchronous programs. Theor. Comput. Sci., 410(42):4169--4179, 2009.

Digital Library

[9]

P. Chambart and Ph. Schnoebelen. The ordinal recursive complexity of lossy channel systems. In Proc. LICS'08, pages 205--216. IEEE, 2008.

Digital Library

[10]

S. Demri, M. Jurdziński, O. Lachish, and R. Lazić. The covering and boundedness problems for branching vector addition systems. J. Comput. Syst. Sci., 79(1):23--38, 2013.

Digital Library

[11]

N. Dershowitz and Z. Manna. Proving termination with multiset orderings. Commun. ACM, 22(8):465--476, 1979.

Digital Library

[12]

C. Dufourd, A. Finkel, and Ph. Schnoebelen. Reset nets between decidability and undecidability. In Proc. ICALP'98, volume 1443 of LNCS, pages 103--115. Springer, 1998.

Digital Library

[13]

D. Figueira, S. Figueira, S. Schmitz, and Ph. Schnoebelen. Ackermannian and primitive-recursive bounds with Dickson's lemma. In Proc. LICS'11, pages 269--278. IEEE, 2011.

Digital Library

[14]

A. Finkel. Reduction and covering of infinite reachability trees. Inform. Comput., 89(2):144--179, 1990.

Digital Library

[15]

A. Finkel and Ph. Schnoebelen. Well-structured transition systems everywhere! Theor. Comput. Sci., 256(1--2):63--92, 2001.

Digital Library

[16]

A. Finkel, P. McKenzie, and C. Picaronny. A well-structured framework for analysing Petri net extensions. Inform. Comput., 195(1--2):1--29, 2004.

Digital Library

[17]

P. Ganty and R. Majumdar. Algorithmic verification of asynchronous programs. ACM Trans. Prog. Lang. Syst., 34(1):6:1--6:48, 2012.

Digital Library

[18]

C. Haase, S. Schmitz, and Ph. Schnoebelen. The power of priority channel systems. In Proc. CONCUR'13, volume 8052 of LNCS, pages 319--333. Springer, 2013.

Digital Library

[19]

R. Lazic. The reachability problem for vector addition systems with a stack is not elementary. CoRR, abs/1310.1767, 2013. Presented at RP'12.

[20]

M. Löb and S. Wainer. Hierarchies of number-theoretic functions. I. Archiv für mathematische Logik und Grundlagenforschung, 13(1--2):39--51, 1970. http://dx.doi.org/10.1007/BF01967649.

[21]

E. Mayr and A. Meyer. The complexity of the finite containment problem for petri nets. J. ACM, 28(3):561--576, 1981.

Digital Library

[22]

K. McAloon. Petri nets and large finite sets. Theor. Comput. Sci., 32(1--2):173--183, 1984.

[23]

C. Rackoff. The covering and boundedness problems for vector addition systems. Theor. Comput. Sci., 6(2):223--231, 1978.

[24]

K. Reinhardt. Reachability in petri nets with inhibitor arcs. Electr. Notes Theor. Comput. Sci., 223:239--264, 2008.

Digital Library

[25]

S. Schmitz and Ph. Schnoebelen. Multiply-recursive upper bounds with Higman's lemma. In Proc. ICALP'11, volume 6756 of LNCS, pages 441--452. Springer, 2011.

Digital Library

[26]

K. Sen and M. Viswanathan. Model checking multithreaded programs with asynchronous atomic methods. In Proc. CAV'06, volume 4144 of LNCS, pages 300--314. Springer, 2006.

Digital Library

Cited By

Leroux J(2022)The Reachability Problem for Petri Nets is Not Primitive Recursive2021 IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS)10.1109/FOCS52979.2021.00121(1241-1252)Online publication date: Feb-2022
https://doi.org/10.1109/FOCS52979.2021.00121
Athaiya SKomondoor RKumar K(2021)Data Flow Analysis of Asynchronous Systems using Infinite Abstract DomainsProgramming Languages and Systems10.1007/978-3-030-72019-3_2(30-58)Online publication date: 23-Mar-2021
https://doi.org/10.1007/978-3-030-72019-3_2
Englert MHofman PLasota SLazić RLeroux JStraszyński J(2020)A lower bound for the coverability problem in acyclic pushdown VASInformation Processing Letters10.1016/j.ipl.2020.106079(106079)Online publication date: Dec-2020
https://doi.org/10.1016/j.ipl.2020.106079
Show More Cited By

Index Terms

Hyper-Ackermannian bounds for pushdown vector addition systems
1. Theory of computation
  1. Computational complexity and cryptography
    1. Complexity classes
  2. Formal languages and automata theory

Recommendations

An Approach to Regular Separability in Vector Addition Systems
LICS '20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science

We study the problem of regular separability of languages of vector addition systems with states (VASS). It asks whether for two given VASS languages K and L, there exists a regular language R that includes K and is disjoint from L. While decidability ...
Ramsey-Based Inclusion Checking for Visibly Pushdown Automata

Checking whether one formal language is included in another is important in many verification tasks. In this article, we provide solutions for checking the inclusion of languages given by visibly pushdown automata over both finite and infinite words. ...
Timed pushdown automata and branching vector addition systems
LICS '17: Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science

We prove that non-emptiness of timed register pushdown automata is decidable in doubly exponential time. This is a very expressive class of automata, whose transitions may involve state and top-of-stack clocks with unbounded differences. It strictly ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CSL-LICS '14: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

July 2014

764 pages

ISBN:9781450328869

DOI:10.1145/2603088

Program Chairs:
Thomas Henzinger
Institute of Science and Technology (IST), Austria
,
Dale Miller
INRIA and LIX/Ecole Polytechnique, Palaiseau

Copyright © 2014 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGLOG: ACM Special Interest Group on Logic and Computation
EACSL: European Association for Computer Science Logic
IEEE-CS\DATC: IEEE Computer Society

In-Cooperation

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 July 2014

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

CSL-LICS '14

Sponsor:

SIGLOG
EACSL
IEEE-CS\DATC

CSL-LICS '14: JOINT MEETING OF the Twenty-Third EACSL Annual Conference on COMPUTER SCIENCE LOGIC

July 14 - 18, 2014

Vienna, Austria

Acceptance Rates

CSL-LICS '14 Paper Acceptance Rate 74 of 212 submissions, 35%;

Overall Acceptance Rate 215 of 622 submissions, 35%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
111
Total Downloads

Downloads (Last 12 months)9
Downloads (Last 6 weeks)1

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Leroux J(2022)The Reachability Problem for Petri Nets is Not Primitive Recursive2021 IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS)10.1109/FOCS52979.2021.00121(1241-1252)Online publication date: Feb-2022
https://doi.org/10.1109/FOCS52979.2021.00121
Athaiya SKomondoor RKumar K(2021)Data Flow Analysis of Asynchronous Systems using Infinite Abstract DomainsProgramming Languages and Systems10.1007/978-3-030-72019-3_2(30-58)Online publication date: 23-Mar-2021
https://doi.org/10.1007/978-3-030-72019-3_2
Englert MHofman PLasota SLazić RLeroux JStraszyński J(2020)A lower bound for the coverability problem in acyclic pushdown VASInformation Processing Letters10.1016/j.ipl.2020.106079(106079)Online publication date: Dec-2020
https://doi.org/10.1016/j.ipl.2020.106079
Schmitz SZetzsche G(2019)Coverability Is Undecidable in One-Dimensional Pushdown Vector Addition Systems with ResetsReachability Problems10.1007/978-3-030-30806-3_15(193-201)Online publication date: 6-Sep-2019
https://doi.org/10.1007/978-3-030-30806-3_15
Li CCai X(2017)Hardness Results for Coverability Problem of Well-Structured Pushdown SystemsLanguage and Automata Theory and Applications10.1007/978-3-319-53733-7_32(435-446)Online publication date: 16-Feb-2017
https://doi.org/10.1007/978-3-319-53733-7_32
Wang YTao XLi G(2016)On Termination and Boundedness of Nested Updatable Timed Automata6th International Workshop on Structured Object-Oriented Formal Language and Method - Volume 1018910.1007/978-3-319-57708-1_2(15-31)Online publication date: 15-Nov-2016
https://dl.acm.org/doi/10.1007/978-3-319-57708-1_2
Lazić RTotzke P(2016)What Makes Petri Nets Harder to Verify: Stack or Data?Concurrency, Security, and Puzzles10.1007/978-3-319-51046-0_8(144-161)Online publication date: 18-Dec-2016
https://doi.org/10.1007/978-3-319-51046-0_8
Hague MLin A(2016)Decidable Models of Integer-Manipulating Programs with Recursive ParallelismReachability Problems10.1007/978-3-319-45994-3_11(148-162)Online publication date: 13-Sep-2016
https://doi.org/10.1007/978-3-319-45994-3_11
Leroux JSutre GTotzke P(2015)On the Coverability Problem for Pushdown Vector Addition Systems in One DimensionProceedings, Part II, of the 42nd International Colloquium on Automata, Languages, and Programming - Volume 913510.1007/978-3-662-47666-6_26(324-336)Online publication date: 6-Jul-2015
https://dl.acm.org/doi/10.1007/978-3-662-47666-6_26
Leroux JSutre GTotzke P(2015)On Boundedness Problems for Pushdown Vector Addition SystemsReachability Problems10.1007/978-3-319-24537-9_10(101-113)Online publication date: 1-Oct-2015
https://doi.org/10.1007/978-3-319-24537-9_10
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents