Linear-Time Verification of Data-Aware Dynamic Systems with Arithmetic
This work addresses the challenge of combined modeling and verification of dynamic systems with data for AI and application domains, providing new decidability and modularity results that extend beyond earlier approaches.
The paper tackles the problem of verifying data-aware dynamic systems extended with linear arithmetic by introducing the property of 'finite summary', which ensures a faithful finite-state abstraction, and shows that checking for witnesses of linear-time, finite-trace properties is decidable for such systems, with a prototype implementation demonstrating feasibility.
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.