文章基本信息

标题：A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One
本地全文：下载
作者：Stefan G{\"o}ller ; Christoph Haase ; Ranko Lazic 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2016
卷号：55
页码：105:1-105:13
DOI：10.4230/LIPIcs.ICALP.2016.105
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：branching vector addition systems; reachability; coverability; boundedness