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

The need to model and analyse dynamic systems operating over complex data isubiquitous in AI and neighboring areas, in particular business processmanagement. Analysing such data-aware systems is a notoriously difficultproblem, as they are intrinsically infinite-state. Existing approaches work forspecific datatypes, and/or limit themselves to the verification of safetyproperties. In this paper, we lift both such limitations, studying for thefirst time linear-time verification for so-called data-aware processes modulotheories (DMTs), from the foundational and practical point of view. The DMTmodel is very general, as it supports processes operating over variables thatcan store arbitrary types of data, ranging over infinite domains and equippedwith domain-specific predicates. Specifically, we provide four contributions.First, we devise a semi-decision procedure for linear-time verification ofDMTs, which works for a very large class of datatypes obeying to mildmodel-theoretic assumptions. The procedure relies on a unique combination ofautomata-theoretic and cover computation techniques to respectively deal withlinear-time properties and datatypes. Second, we identify an abstract, semanticproperty that guarantees the existence of a faithful finite-state abstractionof the original system, and show that our method becomes a decision procedurein this case. Third, we identify concrete, checkable classes of systems thatsatisfy this property, generalising several results in the literature. Finally,we present an implementation and a first experimental evaluation.

Linear-Time Verification of Data-Aware Processes Modulo Theories via Covers and Automata (Extended Version)