基于Presburger归纳不变量的广义向量加法系统可达性问题
计算机科学中的逻辑
2015-07-01 v2
摘要
向量加法系统(VASs)的可达性问题是网论的核心问题。已知该一般问题可由完全基于经典Kosaraju-Lambert-Mayr-Sacerdote-Tenney分解的算法判定。本文利用该分解证明了VASs识别语言的Parikh像是半伪线性的；该类别扩展了半线性集，即Presburger算术中可定义的集合。我们给出了该结果的一个应用；我们证明了当且仅当存在一个包含初始配置但不包含终止配置的半线性归纳不变量时，无法从初始配置到达终止配置。由于我们可以判定Presburger公式是否表示归纳不变量，因此我们推导出存在可检验的不可达性证书。具体而言，存在一种基于两个半算法的简单算法来判定广义VAS可达性问题。第一个半算法通过枚举有限动作序列来尝试证明可达性，第二个半算法通过枚举Presburger公式来尝试证明不可达性。
引用
@article{arxiv.1009.1076,
title = {The General Vector Addition System Reachability Problem by Presburger Inductive Invariants},
author = {leroux jerome},
journal= {arXiv preprint arXiv:1009.1076},
year = {2015}
}