Research map / Learning theory and algorithms / Combinatorial and search optimization
Linear-Time Verification of Data-Aware Processes Modulo Theories via Covers and Automata
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Gives a semi-decision procedure for LTLf verification of data-aware processes modulo theories (DMTs), combining automata for temporal properties with cover computation for datatypes, plus decidable classes and an SMT-based tool evaluated on BPM benchmarks.
Problem
Linear-time (LTLf) verification of infinite-state data-aware business processes whose variables range over arbitrary theory-based datatypes (arithmetic, EUF, read-only databases), where prior work covered only safety or specific datatypes.
Approach
Combine an NFA for data-LTLf properties with cover computation in the background theory to build a product automaton over symbolic formulas; define a finite data history criterion under which this becomes a decision procedure, and identify checkable decidable classes (acyclic signatures, monotonicity constraints, local finiteness, bounded lookback).
Key results
- All 18 benchmark DMT problems, each with five properties checked, are solved in under 20 seconds per problem (the maximum is 54.23 s total for problem 10, with 17.38 s max per property).
- About 36% of computation time is spent on SMT checks and 29% on quantifier elimination and cover computation.
- Benchmark processes all fall into the decidable classes I-IV, indicating these classes cover practically relevant systems.
Surprising findings
- Transition formulae with large depth (e.g., airline check-in, problem 10) noticeably degrade performance.
Limitations
- Semi-decision procedure in general; termination only guaranteed in decidable classes
- LTLf verification is undecidable for numeric variables in general, so the task is undecidable without restrictions
- Read-only databases only; database updates are excluded
Experimental setup
Datasets: VERIFAS problem set
Benchmarks: VERIFAS problem set (real-world data-aware business processes)
Metrics: computation time in seconds number of SMT checks
Baselines: VERIFAS
Builds on: LTLf cover computation (Calvanese et al.) model completion Felli et al. 2022 DDS verification SMT-based verification of artifact systems
Closest papers by meaning
- Foundations of Reactive Synthesis for Declarative Process Specifications (AAAI 2024 · similarity 0.86)
- MAS-ProVe: Understanding the Process Verification of Multi-Agent Systems (ICML 2026 · similarity 0.85)
- DABL: Detecting Semantic Anomalies in Business Processes Using Large Language Models (AAAI 2025 · similarity 0.83)
- interwhen: A Generalizable Framework for Steering Reasoning Models with Test-time Verification (NeurIPS 2026 · similarity 0.82)
- DAComp: Benchmarking Data Agents across the Full Data Intelligence Lifecycle (ICLR 2026 · similarity 0.82)
- Taming Imperfect Process Verifiers: A Sampling Perspective on Backtracking (ICLR 2026 · similarity 0.81)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.