Linear-Time Verification of Data-Aware Dynamic Systems with Arithmetic
Keywords:Knowledge Representation And Reasoning (KRR)
AbstractCombined 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 providing 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.
How to Cite
Felli, P., Montali, M., & Winkler, S. (2022). Linear-Time Verification of Data-Aware Dynamic Systems with Arithmetic. Proceedings of the AAAI Conference on Artificial Intelligence, 36(5), 5642-5650. https://doi.org/10.1609/aaai.v36i5.20505
AAAI Technical Track on Knowledge Representation and Reasoning