Logic Mining from Process Logs: Towards Automated Specification and Verification

TL;DR

This paper introduces a method to automatically generate logical specifications from process logs using pattern-based translation and automated reasoning, facilitating formal analysis of complex systems.

Contribution

It presents a novel approach combining workflow mining with automated theorem proving to derive and validate logical specifications from process models.

Findings

Effective on both general and real-case logs

Data quality impacts specification structure and testability

Automated reasoning validates logical properties

Abstract

Logical specifications play a key role in the formal analysis of behavioural models. Automating the derivation of such specifications is particularly valuable in complex systems, where manual construction is time-consuming and error-prone. This article presents an approach for generating logical specifications from process models discovered via workflow mining, combining pattern-based translation with automated reasoning techniques. In contrast to earlier work, we evaluate the method on both general-purpose and real-case event logs, enabling a broader empirical assessment. The study examines the impact of data quality, particularly noise, on the structure and testability of generated specifications. Using automated theorem provers, we validate a variety of logical properties, including satisfiability, internal consistency, and alignment with predefined requirements. The results support the applicability of the approach in realistic settings and its potential integration into empirical software engineering practices.