首页    期刊浏览 2024年11月26日 星期二
登录注册

文章基本信息

  • 标题:Reachability in Fixed Dimension Vector Addition Systems with States
  • 本地全文:下载
  • 作者:Wojciech CzerwiÅ"ski ; S{\l}awomir Lasota ; Ranko LaziÄ
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2020
  • 卷号:171
  • 页码:48:1-48:21
  • DOI:10.4230/LIPIcs.CONCUR.2020.48
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要:The reachability problem is a central decision problem in verification of vector addition systems with states (VASS). In spite of recent progress, the complexity of the reachability problem remains unsettled, and it is closely related to the lengths of shortest VASS runs that witness reachability. We obtain three main results for VASS of fixed dimension. For the first two, we assume that the integers in the input are given in unary, and that the control graph of the given VASS is flat (i.e., without nested cycles). We obtain a family of VASS in dimension 3 whose shortest runs are exponential, and we show that the reachability problem is NP-hard in dimension 7. These results resolve negatively questions that had been posed by the works of Blondin et al. in LICS 2015 and Englert et al. in LICS 2016, and contribute a first construction that distinguishes 3-dimensional flat VASS from 2-dimensional ones. Our third result, by means of a novel family of products of integer fractions, shows that 4-dimensional VASS can have doubly exponentially long shortest runs. The smallest dimension for which this was previously known is 14.
  • 关键词:reachability problem; vector addition systems; Petri nets
国家哲学社会科学文献中心版权所有