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.

翻译：在人工智能及其邻近领域（尤其是业务流程管理）中，对操作复杂数据的动态系统进行建模与分析的需求十分普遍。分析此类数据感知系统是一个公认的难题，因为它们本质上是无限状态的。现有方法仅适用于特定数据类型，且/或局限于安全性性质的验证。本文首次从基础和实践角度同时突破了这两项限制，研究了所谓的“基于理论模的数据感知过程”（DMTs）的线性时间验证问题。DMT模型具有高度通用性，支持对可存储任意数据类型（涵盖无限域并配备领域特定谓词）的变量进行操作的过程。具体而言，我们做出四项贡献：第一，提出了一种用于DMTs线性时间验证的半决策过程，该方法适用于满足温和模型论假设的极广泛数据类型，通过独特组合自动化理论技术（处理线性时间性质）和覆盖计算技术（处理数据类型）实现；第二，识别出一种保证原始系统存在忠实有限状态抽象的抽象语义性质，并证明在此情况下我们的方法可转化为决策过程；第三，识别出满足该性质的具体可检验系统类别，推广了文献中的多项结果；最后，给出了实现方案及初步实验评估。