论文标题
使用算术的数据感知动态系统的线性时间验证
Linear-Time Verification of Data-Aware Dynamic Systems with Arithmetic
论文作者
论文摘要
动态系统及其运行的数据的结合建模和验证在AI和几个应用程序域中都获得了动力。我们研究了数据感知动态系统（DDS）的表达性而简洁的框架，以线性算术扩展并提供以下贡献。首先，我们引入了“有限摘要”的新语义属性，该属性保证了忠实的有限国家抽象的存在。我们依靠这一点来表明，检查是否存在有限摘要的DDS来确定证人是否存在线性时间，有限痕迹的属性。其次，我们证明了以形式方法和数据库理论研究的几种可确定性条件可以看作是该属性的具体，可检查实例。这也带来了新的可决定性结果。第三，我们展示有限摘要的抽象，均匀的属性如何导致模块化结果：如果可以将其适当地分配到具有该属性的较小系统中，则系统可以享受有限的摘要。我们的结果使我们能够分析早期方法无法触及的系统。最后，我们证明了我们在原型实现中的可行性。
Combined modeling and verification of dynamic systems and the data they operate on has gained momentum in AI and in several application domains. We investigate the expressive yet concise framework of data-aware dynamic systems (DDS), extending it with linear arithmetic, and provide the following contributions. First, we introduce a new, semantic property of "finite summary", which guarantees the existence of a faithful finite-state abstraction. We rely on this to show that checking whether a witness exists for a linear-time, finite-trace property is decidable for DDSs with finite summary. Second, we demonstrate that several decidability conditions studied in formal methods and database theory can be seen as concrete, checkable instances of this property. This also gives rise to new decidability results. Third, we show how the abstract, uniform property of finite summary leads to modularity results: a system enjoys finite summary if it can be partitioned appropriately into smaller systems that possess the property. Our results allow us to analyze systems that were out of reach in earlier approaches. Finally, we demonstrate the feasibility of our approach in a prototype implementation.
