# Linear-Time Verification of Data-Aware Dynamic Systems with Arithmetic

arXiv: https://arxiv.org/abs/2203.07982 · HTML: https://mlsanity.com/paper/2203.07982/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 1 of its 33 references that are in the map.
- First posted on arXiv 15 Mar 2022.

## Builds on (most cited first, 1 of 1)

- [Branching-Time Model Checking Gap-Order Constraint Systems (Extended Version)](https://mlsanity.com/paper/1307.4207/) (2013)

## Built on by (most cited first, 4 of 4)

- [Decidable Fragments of LTLf Modulo Theories (Extended Version)](https://mlsanity.com/paper/2307.16840/) (2023)
- [Soundness of Data-Aware Processes with Arithmetic Conditions](https://mlsanity.com/paper/2203.14809/) (2022)
- [Relational Action Bases: Formalization, Effective Safety Verification, and Invariants (Extended Version)](https://mlsanity.com/paper/2208.06377/) (2022)
- [Progression- vs Automata-based Anticipatory Monitoring of LTL over Finite Traces (Extended Version)](https://mlsanity.com/paper/2609.32912/) (2026)

## Abstract (arXiv)

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.