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

TL;DR

This paper introduces a novel linear-time verification method for data-aware processes with complex data types, combining automata and cover techniques to handle infinite states and support safety property analysis.

Contribution

It presents the first semi-decision procedure for linear-time verification of data-aware processes modulo theories, extending applicability beyond specific datatypes and safety properties.

Findings

The procedure works for a large class of datatypes with mild assumptions.

A semantic property guarantees finite-state abstraction, making the method a decision procedure.

Implementation and initial experiments demonstrate practical viability.

Abstract

The need to model and analyse dynamic systems operating over complex data is ubiquitous in AI and neighboring areas, in particular business process management. Analysing such data-aware systems is a notoriously difficult problem, as they are intrinsically infinite-state. Existing approaches work for specific datatypes, and/or limit themselves to the verification of safety properties. In this paper, we lift both such limitations, studying for the first time linear-time verification for so-called data-aware processes modulo theories (DMTs), from the foundational and practical point of view. The DMT model is very general, as it supports processes operating over variables that can store arbitrary types of data, ranging over infinite domains and equipped with domain-specific predicates. Specifically, we provide four contributions. First, we devise a semi-decision procedure for linear-time verification of DMTs, which works for a very large class of datatypes obeying to mild model-theoretic assumptions. The procedure relies on a unique combination of automata-theoretic and cover computation techniques to respectively deal with linear-time properties and datatypes. Second, we identify an abstract, semantic property that guarantees the existence of a faithful finite-state abstraction of the original system, and show that our method becomes a decision procedure in this case. Third, we identify concrete, checkable classes of systems that satisfy this property, generalising several results in the literature. Finally, we present an implementation and a first experimental evaluation.