English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Combined modeling and verification of dynamic systems and the data theyoperate on has gained momentum in AI and in several application domains. Weinvestigate the expressive yet concise framework of data-aware dynamic systems(DDS), extending it with linear arithmetic, and provide the followingcontributions. First, we introduce a new, semantic property of "finitesummary", which guarantees the existence of a faithful finite-stateabstraction. We rely on this to show that checking whether a witness exists fora linear-time, finite-trace property is decidable for DDSs with finite summary.Second, we demonstrate that several decidability conditions studied in formalmethods and database theory can be seen as concrete, checkable instances ofthis property. This also gives rise to new decidability results. Third, we showhow the abstract, uniform property of finite summary leads to modularityresults: a system enjoys finite summary if it can be partitioned appropriatelyinto smaller systems that possess the property. Our results allow us to analyzesystems that were out of reach in earlier approaches. Finally, we demonstratethe feasibility of our approach in a prototype implementation.

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