Petri nets, equivalently presentable as vector addition systems with states, are an established model of concurrency with widespread applications. The reachability problem, where we ask whether from a given initial configuration there exists a sequence of valid execution steps reaching a given final configuration, is the central algorithmic problem for this model. The complexity of the problem has remained, until recently, one of the hardest open questions in verification of concurrent systems. A first upper bound has been provided only in 2015 by Leroux and Schmitz, then refined by the same authors to non-primitive recursive Ackermannian upper bound in 2019. The exponential space lower bound, shown by Lipton already in 1976, remained the only known for over 40 years until a breakthrough non-elementary lower bound by Czerwi{\'n}ski, Lasota, Lazic, Leroux and Mazowiecki in 2019. Finally, a matching Ackermannian lower bound announced this year by Czerwi{\'n}ski and Orlikowski, and independently by Leroux, established the complexity of the problem. Our contribution is an improvement of the former construction, making it conceptually simpler and more direct. On the way we improve the lower bound for vector addition systems with states in fixed dimension (or, equivalently, Petri nets with fixed number of places): while Czerwi{\'n}ski and Orlikowski prove $F_k$-hardness (hardness for $k$th level in Grzegorczyk Hierarchy) in dimension $6k$, and Leroux in dimension $4k+5$, our simplified construction yields $F_k$-hardness already in dimension $3k+2$.


翻译:与各州的矢量添加系统完全相似的彼得罗网(Petrinet)是州级的矢量添加系统,是一种成熟的固定货币模式,其应用范围广泛。在最初配置中,我们询问是否存在一个有效的执行步骤序列,从而达到某个最终配置,因此,这种模式的中心算法问题。直到最近,问题的复杂性仍然是并行系统核查中最难解的问题之一。直到2015年才提供了第一个上层约束,由勒鲁和施密茨提供,然后由同一位作者改进为2019年非原始再现的阿克曼尼亚上限。利普顿(Lipton)已经于1976年展示的指数性低空间约束,在40多年后仍是唯一已知的非元素执行步骤,直到2019年Czerwi_nski、Lasota、Lazic、Lerouux和Mazowieecki。最后,由Czerfrumannial $(Czeru) 和 Orliksyalow) 已经独立地确定了问题的复杂程度。我们的贡献是,在前的固定的建筑和固定水平上,我们更简化了固定的固定的系统。

0
下载
关闭预览

相关内容

开源书:PyTorch深度学习起步
专知会员服务
51+阅读 · 2019年10月11日
MIT新书《强化学习与最优控制》
专知会员服务
282+阅读 · 2019年10月9日
CCF A类 | 顶级会议RTSS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年4月17日
人工智能类 | 国际会议/SCI期刊专刊信息9条
Call4Papers
4+阅读 · 2018年7月10日
条件GAN重大改进!cGANs with Projection Discriminator
CreateAMind
8+阅读 · 2018年2月7日
人工智能 | 国际会议截稿信息5条
Call4Papers
6+阅读 · 2017年11月22日
【计算机类】期刊专刊/国际会议截稿信息6条
Call4Papers
3+阅读 · 2017年10月13日
Arxiv
0+阅读 · 2021年9月4日
Arxiv
0+阅读 · 2021年9月3日
VIP会员
相关VIP内容
相关资讯
CCF A类 | 顶级会议RTSS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年4月17日
人工智能类 | 国际会议/SCI期刊专刊信息9条
Call4Papers
4+阅读 · 2018年7月10日
条件GAN重大改进!cGANs with Projection Discriminator
CreateAMind
8+阅读 · 2018年2月7日
人工智能 | 国际会议截稿信息5条
Call4Papers
6+阅读 · 2017年11月22日
【计算机类】期刊专刊/国际会议截稿信息6条
Call4Papers
3+阅读 · 2017年10月13日
相关论文
Arxiv
0+阅读 · 2021年9月4日
Arxiv
0+阅读 · 2021年9月3日
Top
微信扫码咨询专知VIP会员