Skip to main contentSkip to search
Episciences
Open Access Journals
Sign in(new window)
Discrete Mathematics & Theoretical Computer Science logo
Discrete Mathematics & Theoretical Computer Science
Discrete Mathematics & Theoretical Computer Science logo
Discrete Mathematics & Theoretical Computer Science
Sign in(new window)
Articles & Issues
All articlesAll accepted articlesAll volumesLast volumeSectionsSpecial issuesAuthors
About
The journalIndexing
Boards
Publish
For authorsEthical charter
Submit
Discrete Mathematics & Theoretical Computer Science logo
Contact
|
Credits
eISSN 1365-8050
|
RSS
|
Atom
Episciences
Documentation
|
Acknowledgements
|
Publishing policy
Accessibility: non-compliant
|
Legal mentions
|
Privacy statement
|
Terms of use
  1. Home > Articles & Issues >
  2. Articles >
  3. Karp-Miller Trees fo ...
Article

Karp-Miller Trees for a Branching Extension of VASS

Kumar Neeraj Verma (1), Jean Goubault-Larrecq ORCID (2) (3)
(1) Institut für Informatik
(2) Laboratoire Spécification et Vérification [Cachan]
(3) Security of information systems
Download article
Open on HAL
Imported on
March 26, 2015
Published on
January 1, 2005
Last modified on
March 31, 2025
Volume 7
vol. 7
DOI
10.46298/dmtcs.350
License
https://about.hal.science/hal-authorisation-v1
Indicators
1091
Views
1142
Downloads

Karp-Miller Trees for a Branching Extension of VASS

Kumar Neeraj Verma (1), Jean Goubault-Larrecq ORCID (2) (3)
(1) Institut für Informatik
(2) Laboratoire Spécification et Vérification [Cachan]
(3) Security of information systems
Abstract
We study BVASS (Branching VASS) which extend VASS (Vector Addition Systems with States) by allowing addition transitions that merge two configurations. Runs in BVASS are tree-like structures instead of linear ones as for VASS. We show that the construction of Karp-Miller trees for VASS can be extended to BVASS. This entails that the coverability set for BVASS is computable. This allows us to obtain decidability results for certain classes of equational tree automata with an associative-commutative symbol. Recent independent work by de Groote et al. implies that decidability of reachability in BVASS is equivalent to decidability of provability in MELL (multiplicative exponential linear logic), which is still an open problem. Hence our results are also a step towards answering this question in the affirmative.
Keywords
  • [INFO.INFO-DM]Computer Science [cs]/Discrete Mathematics [cs.DM]
  • branching vector addition systems
  • Karp-Miller trees
  • coverability
  • multiplicative exponential linear logic
  • equational tree automata
Cited by

Source: OpenCitations

  • The covering and boundedness problems for branching vector addition systems

    Journal of Computer and System Sciences

    Authors : Stéphane Demri ORCID, Marcin Jurdziński ORCID, Oded Lachish ORCID, Ranko Lazić ORCID

    Journal reference : Volume 79, 2012, pp. 23-38

    DOI : 10.1016/j.jcss.2012.04.002

  • On the complexity of resource-bounded logics

    Theoretical Computer Science

    Authors : N. Alechina ORCID, N. Bulling, S. Demri ORCID, B. Logan ORCID

    Journal reference : Volume 750, 2018, pp. 69-100

    DOI : 10.1016/j.tcs.2018.01.019

  • Binary Reachability of Timed-register Pushdown Automata and Branching Vector Addition Systems

    ACM Transactions on Computational Logic

    Authors : Lorenzo Clemente ORCID, Sławomir Lasota ORCID, Ranko Lazić ORCID, Filip Mazowiecki ORCID

    Journal reference : Volume 20, 2019, pp. 1-31

    DOI : 10.1145/3326161

  • Forward analysis for WSTS, part I: completions

    arXiv (Cornell University)

    Authors : Alain Finkel ORCID, Jean Goubault-Larrecq ORCID

    Journal reference : Volume 30, 2020, pp. 752-832

    DOI : 10.1017/s0960129520000195

  • A Survey of Elevator Group Control Systems for Vertical Transportation: A Look at Recent Literature

    IEEE Control Systems

    Authors : Joaquin R. Fernandez ORCID, Pablo Cortes ORCID

    Journal reference : Volume 35, 2015, pp. 38-55

    DOI : 10.1109/mcs.2015.2427045

  • Alternation in Equational Tree Automata Modulo XOR

    Lecture notes in computer science

    Authors : Kumar Neeraj Verma

    Journal reference : Volume , 2004, pp. 518-530

    DOI : 10.1007/978-3-540-30538-5_43

  • Analysis of Recursively Parallel Programs

    ACM Transactions on Programming Languages and Systems

    Authors : Ahmed Bouajjani ORCID, Michael Emmi ORCID

    Journal reference : Volume 35, 2013, pp. 1-49

    DOI : 10.1145/2518188

  • On the Reachability Problem for Two-Dimensional Branching VASS

    DROPS (Schloss Dagstuhl – Leibniz Center for Informatics)

    Authors : Bizière, Hilaire, Leroux, Sutre

    Journal reference : Volume , 2025, pp.

    DOI : 10.4230/lipics.mfcs.2025.22

  • On the Complexity of Equational Horn Clauses

    Lecture notes in computer science

    Authors : Kumar Neeraj Verma, Helmut Seidl ORCID, Thomas Schwentick ORCID

    Journal reference : Volume , 2005, pp. 337-352

    DOI : 10.1007/11532231_25

  • IMPLICATIONAL RELEVANCE LOGIC IS 2-EXPTIME-COMPLETE

    Journal of Symbolic Logic

    Authors : SYLVAIN SCHMITZ ORCID

    Journal reference : Volume 81, 2016, pp. 641-661

    DOI : 10.1017/jsl.2015.7

  • Strategic reasoning with a bounded number of resources: The quest for tractability

    Authors : Francesco Belardinelli ORCID, Stéphane Demri ORCID

    Journal reference : Volume 300, 2021, pp. 103557

    DOI : 10.1016/j.artint.2021.103557

  • On the Complexity of Resource-Bounded Logics

    Authors : Natasha Alechina ORCID, Nils Bulling, Stephane Demri ORCID, Brian Logan ORCID

    Journal reference : Volume , 2016, pp. 36-50

    DOI : 10.1007/978-3-319-45994-3_3
Preview
Loading PDF preview...