Modeling and Verification of Infinite Systems with Resources
Modeling and Verification of Infinite Systems with Resources
复制标题
具有资源的无限系统的建模和验证
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Christof Löding
中科院分区：
文献类型：
--
作者：
Martin Lang;Christof Löding
我们考虑形式验证的递归程序的资源消耗。我们引入前缀替换系统与非负整数计数器，可以增加和重置为零，作为一个正式的模型，这样的程序。在这些系统中，我们调查的可达性问题的资源消耗的界限。基于这个问题，我们引入了具有资源的关系结构和这些结构上的定量一阶逻辑。我们定义了资源自动结构作为这些结构的子类，并提供了一种有效的方法来计算这个子类上的逻辑的语义。随后，我们使用这个框架来解决资源前缀替换系统的有界可达性问题。我们实现了这一结果，通过扩展著名的饱和度的方法来注释前缀替换系统。最后，我们提供了一个连接到逻辑成本的研究-WMSO。
We consider formal verification of recursive programs with resource consumption. We introduce prefix replacement systems with non-negative integer counters which can be incremented and reset to zero as a formal model for such programs. In these systems, we investigate bounds on the resource consumption for reachability questions. Motivated by this question, we introduce relational structures with resources and a quantitative first-order logic over these structures. We define resource automatic structures as a subclass of these structures and provide an effective method to compute the semantics of the logic on this subclass. Subsequently, we use this framework to solve the bounded reachability problem for resource prefix replacement systems. We achieve this result by extending the well-known saturation method to annotated prefix replacement systems. Finally, we provide a connection to the study of the logic cost-WMSO.