A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One

Stefan Goller; Christoph  Haase; Ranko  Lazic; Patrick Totzke

doi:10.4230/LIPIcs.ICALP.2016.105

A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One

Stefan Goller, Christoph Haase, Ranko Lazic, Patrick Totzke

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

Branching VASS (BVASS) generalise vector addition systems with states by allowing for special branching transitions that can non-deterministically distribute a counter value between two control states. A run of a BVASS consequently becomes a tree, and reachability is to decide whether a given configuration is the root of a reachability tree. This paper shows P-completeness of reachability in BVASS in dimension one, the first decidability result for reachability in a subclass of BVASS known so far. Moreover, we show that coverability and boundedness in BVASS in dimension one are P-complete as well.

Original language	English
Title of host publication	The 43rd International Colloquium on Automata, Languages and Programming (ICALP 2016), the main European conference in Theoretical Computer Science and annual meeting of the European Association for Theoretical Computer Science (EATCS)
Place of Publication	Rome, Italy
Publisher	Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany
Pages	105:1-105:13
Number of pages	13
ISBN (Electronic)	978-3-95977-013-2
DOIs	https://doi.org/10.4230/LIPIcs.ICALP.2016.105
Publication status	Published - 15 Jul 2016
Event	43rd International Colloquium on Automata, Languages and Programming (ICALP 2016), the main European conference in Theoretical Computer Science and annual meeting of the European Association for Theoretical Computer Science - Sapienza University of Rome, Rome, Italy Duration: 12 Jul 2016 → 15 Jul 2016 http://www.easyconferences.eu/icalp2016/ http://www.easyconferences.eu/icalp2016/index.html

Publication series

Name	Leibniz International Proceedings in Informatics (LIPIcs)
Publisher	Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
Volume	55
ISSN (Electronic)	1868-8969

Conference

Conference	43rd International Colloquium on Automata, Languages and Programming (ICALP 2016), the main European conference in Theoretical Computer Science and annual meeting of the European Association for Theoretical Computer Science
Abbreviated title	ICALP 2016
Country/Territory	Italy
City	Rome
Period	12/07/16 → 15/07/16
Internet address	http://www.easyconferences.eu/icalp2016/ http://www.easyconferences.eu/icalp2016/index.html

Access to Document

10.4230/LIPIcs.ICALP.2016.105

GHLT2016Accepted author manuscript, 666 KBLicence: Creative Commons: Attribution (CC-BY)

http://drops.dagstuhl.de/opus/volltexte/2016/6240/

Energy Efficient Control
Mayr, R. (Principal Investigator)
EPSRC
1/09/15 → 31/08/19
Project: Research

Cite this

Goller, S., Haase, C., Lazic, R., & Totzke, P. (2016). A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One. In The 43rd International Colloquium on Automata, Languages and Programming (ICALP 2016), the main European conference in Theoretical Computer Science and annual meeting of the European Association for Theoretical Computer Science (EATCS) (pp. 105:1-105:13). Article 105 (Leibniz International Proceedings in Informatics (LIPIcs); Vol. 55). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany. https://doi.org/10.4230/LIPIcs.ICALP.2016.105

Goller, Stefan ; Haase, Christoph ; Lazic, Ranko et al. / A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One. The 43rd International Colloquium on Automata, Languages and Programming (ICALP 2016), the main European conference in Theoretical Computer Science and annual meeting of the European Association for Theoretical Computer Science (EATCS). Rome, Italy : Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, 2016. pp. 105:1-105:13 (Leibniz International Proceedings in Informatics (LIPIcs)).

@inproceedings{900c996a9a0e4d1f9c0ba953ca564a9c,

title = "A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One",

abstract = "Branching VASS (BVASS) generalise vector addition systems with states by allowing for special branching transitions that can non-deterministically distribute a counter value between two control states. A run of a BVASS consequently becomes a tree, and reachability is to decide whether a given configuration is the root of a reachability tree. This paper shows P-completeness of reachability in BVASS in dimension one, the first decidability result for reachability in a subclass of BVASS known so far. Moreover, we show that coverability and boundedness in BVASS in dimension one are P-complete as well.",

author = "Stefan Goller and Christoph Haase and Ranko Lazic and Patrick Totzke",

year = "2016",

month = jul,

day = "15",

doi = "10.4230/LIPIcs.ICALP.2016.105",

language = "English",

series = "Leibniz International Proceedings in Informatics (LIPIcs)",

publisher = "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany",

pages = "105:1--105:13",

booktitle = "The 43rd International Colloquium on Automata, Languages and Programming (ICALP 2016), the main European conference in Theoretical Computer Science and annual meeting of the European Association for Theoretical Computer Science (EATCS)",

note = "43rd International Colloquium on Automata, Languages and Programming (ICALP 2016), the main European conference in Theoretical Computer Science and annual meeting of the European Association for Theoretical Computer Science, ICALP 2016 ; Conference date: 12-07-2016 Through 15-07-2016",

url = "http://www.easyconferences.eu/icalp2016/, http://www.easyconferences.eu/icalp2016/index.html",

}

Goller, S, Haase, C, Lazic, R & Totzke, P 2016, A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One. in The 43rd International Colloquium on Automata, Languages and Programming (ICALP 2016), the main European conference in Theoretical Computer Science and annual meeting of the European Association for Theoretical Computer Science (EATCS)., 105, Leibniz International Proceedings in Informatics (LIPIcs), vol. 55, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, Rome, Italy, pp. 105:1-105:13, 43rd International Colloquium on Automata, Languages and Programming (ICALP 2016), the main European conference in Theoretical Computer Science and annual meeting of the European Association for Theoretical Computer Science, Rome, Italy, 12/07/16. https://doi.org/10.4230/LIPIcs.ICALP.2016.105

A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One. / Goller, Stefan; Haase, Christoph ; Lazic, Ranko et al.
The 43rd International Colloquium on Automata, Languages and Programming (ICALP 2016), the main European conference in Theoretical Computer Science and annual meeting of the European Association for Theoretical Computer Science (EATCS). Rome, Italy: Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, 2016. p. 105:1-105:13 105 (Leibniz International Proceedings in Informatics (LIPIcs); Vol. 55).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One

AU - Goller, Stefan

AU - Haase, Christoph

AU - Lazic, Ranko

AU - Totzke, Patrick

PY - 2016/7/15

Y1 - 2016/7/15

N2 - Branching VASS (BVASS) generalise vector addition systems with states by allowing for special branching transitions that can non-deterministically distribute a counter value between two control states. A run of a BVASS consequently becomes a tree, and reachability is to decide whether a given configuration is the root of a reachability tree. This paper shows P-completeness of reachability in BVASS in dimension one, the first decidability result for reachability in a subclass of BVASS known so far. Moreover, we show that coverability and boundedness in BVASS in dimension one are P-complete as well.

AB - Branching VASS (BVASS) generalise vector addition systems with states by allowing for special branching transitions that can non-deterministically distribute a counter value between two control states. A run of a BVASS consequently becomes a tree, and reachability is to decide whether a given configuration is the root of a reachability tree. This paper shows P-completeness of reachability in BVASS in dimension one, the first decidability result for reachability in a subclass of BVASS known so far. Moreover, we show that coverability and boundedness in BVASS in dimension one are P-complete as well.

U2 - 10.4230/LIPIcs.ICALP.2016.105

DO - 10.4230/LIPIcs.ICALP.2016.105

M3 - Conference contribution

T3 - Leibniz International Proceedings in Informatics (LIPIcs)

SP - 105:1-105:13

BT - The 43rd International Colloquium on Automata, Languages and Programming (ICALP 2016), the main European conference in Theoretical Computer Science and annual meeting of the European Association for Theoretical Computer Science (EATCS)

PB - Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany

CY - Rome, Italy

T2 - 43rd International Colloquium on Automata, Languages and Programming (ICALP 2016), the main European conference in Theoretical Computer Science and annual meeting of the European Association for Theoretical Computer Science

Y2 - 12 July 2016 through 15 July 2016

ER -

Goller S, Haase C, Lazic R, Totzke P. A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One. In The 43rd International Colloquium on Automata, Languages and Programming (ICALP 2016), the main European conference in Theoretical Computer Science and annual meeting of the European Association for Theoretical Computer Science (EATCS). Rome, Italy: Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany. 2016. p. 105:1-105:13. 105. (Leibniz International Proceedings in Informatics (LIPIcs)). doi: 10.4230/LIPIcs.ICALP.2016.105

A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One

Abstract

Publication series

Conference

Access to Document

Fingerprint

Projects

Energy Efficient Control

Cite this