带资源无限系统的建模与验证
计算机科学中的逻辑
2015-07-01 v2
摘要
我们考虑具有资源消耗的递归程序的形式化验证。我们引入了带有非负整数计数器的前缀替换系统，这些计数器可以递增并重置为零，作为此类程序的形式模型。在这些系统中，我们研究了可达性问题的资源消耗界限。受此问题的启发，我们引入了带资源的关系结构和基于这些结构的定量一阶逻辑。我们将资源自动结构定义为这些结构的一个子类，并提供了一种有效的方法来计算该子类上逻辑的语义。随后，我们利用该框架解决了资源前缀替换系统的有界可达性问题。我们通过将著名的饱和方法扩展至带注释的前缀替换系统来实现这一结果。最后，我们建立了与 cost-WMSO 逻辑研究的联系。
引用
@article{arxiv.1311.1043,
title = {Modeling and Verification of Infinite Systems with Resources},
author = {Martin Lang and Christof Löding},
journal= {arXiv preprint arXiv:1311.1043},
year = {2015}
}