迁移系统中多面体不变量存在性的可判定性
编程语言
2018-05-16 v2 计算机科学中的逻辑
摘要
自动化程序验证通常通过给出蕴含所需性质的归纳不变量来进行。对于数值性质，一类经典的不变量是凸多面体：线性方程组（不等式）的解集。四十年来关于凸多面体不变量的研究一方面集中于识别“较易”的子类，另一方面集中于寻找一般凸多面体的启发式方法。然而，这些启发式方法不能保证在凸多面体归纳不变量存在时找到它们。据我们所知，多面体归纳不变量的存在性从未被证明是不可判定的。在本文中，我们证明了凸多面体不变量的存在性是不可判定的，即使除“坏”状态外只有一个控制状态。如果不允许任何非线性约束，该问题仍然开放。
引用
@article{arxiv.1709.04382,
title = {On the decidability of the existence of polyhedral invariants in transition systems},
author = {David Monniaux},
journal= {arXiv preprint arXiv:1709.04382},
year = {2018}
}