Linear-Time Verification of Data-Aware Processes Modulo Theories via Covers and Automata

Authors: Alessandro Gianola, Marco Montali, Sarah Winkler

AAAI 2024 | Conference PDF | Archive PDF | Plain Text | LLM Run Details

Reproducibility Variable Result LLM Response
Research Type Experimental Finally, we present an implementation and an experimental evaluation over a benchmark of real-world dataaware business processes.
Researcher Affiliation Academia 1INESC-ID/Instituto Superior T ecnico, Universidade de Lisboa, Lisbon, Portugal 2Faculty of Engineering, Free University of Bozen-Bolzano, Bolzano, Italy
Pseudocode No The paper describes algorithms and procedures textually but does not include any clearly labeled pseudocode or algorithm blocks.
Open Source Code Yes LINDMT is a command-line tool written in Python, but it is also accessible via a web interface (https://lindmt.unibz.it); sources and benchmarks are available as well.
Open Datasets Yes We curated a benchmark set using data-aware business processes from the literature, especially the VERIFAS problem set (Li, Deutsch, and Vianu 2017).
Dataset Splits No The paper mentions checking properties on a benchmark set but does not provide specific details on how data was split for training, validation, or testing.
Hardware Specification No The paper does not provide specific details about the hardware used for running experiments.
Software Dependencies No The tool interfaces CVC5 (Deters et al. 2014) for SMT checks, and QE in LIRA. ... LINDMT is a command-line tool written in Python... The paper mentions software used (CVC5, Python) but does not provide specific version numbers for these dependencies.
Experiment Setup No The paper mentions 'In the input files for Σ-DMTs, control states (like o1, o2 in Ex. 3) are supported for efficiency,' but it does not provide detailed experimental setup information such as specific hyperparameter values or comprehensive training configurations.