验证具有有限幺半群性质的平面仿射计数器系统有多难？
计算复杂性
2016-05-20 v1 计算机科学中的逻辑
摘要
我们研究了具有由凸多面体定义的守卫和由仿射变换定义的更新的计数器系统的若干决策问题。一般而言，此类系统的可达性问题是不可判定的。可通过施加两个限制实现可判定性：(i) 计数器系统的控制结构是平面的，即禁止嵌套循环；(ii) 对于系统中任意仿射更新矩阵，其矩阵幂集合是有限的。我们给出了此类系统若干决策问题的精确复杂度界，证明可达性以及过去线性时序逻辑的模型检测对于多项式层级第二层 是完全的，而一阶逻辑的模型检测是 PSPACE-完全的。
引用
@article{arxiv.1605.05836,
title = {How hard is it to verify flat affine counter systems with the finite monoid property ?},
author = {Radu Iosif and Arnaud Sangnier},
journal= {arXiv preprint arXiv:1605.05836},
year = {2016}
}