Logic Mining from Process Logs: Towards Automated Specification and Verification

• URL: http://arxiv.org/abs/2506.08628v1
• Date: Tue, 10 Jun 2025 09:44:19 GMT
• Title: Logic Mining from Process Logs: Towards Automated Specification and Verification
• Authors: Radoslaw Klimek, Julia Witek,
• Abstract summary: This article presents an approach for generating logical specifications from process models discovered via workflow.<n>The study examines the impact of quality data, particularly noise, on the structure and testability of generated specifications.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Re-evaluation of Logical Specification in Behavioural Verification [0.0]
  This study empirically validates automated logical specification methods for behavioural models.<n>We identify performance irregularities that suggest the need for adaptive performance irregularities in automated reasoning.<n>Addressing these inefficiencies through self-optimising solvers could enhance the stability of automated reasoning.
  arXiv  Detail & Related papers  (2025-05-23T14:46:39Z)
• Evaluating Large Language Models for Real-World Engineering Tasks [75.97299249823972]
  This paper introduces a curated database comprising over 100 questions derived from authentic, production-oriented engineering scenarios.<n>Using this dataset, we evaluate four state-of-the-art Large Language Models (LLMs)<n>Our results show that LLMs demonstrate strengths in basic temporal and structural reasoning but struggle significantly with abstract reasoning, formal modeling, and context-sensitive engineering logic.
  arXiv  Detail & Related papers  (2025-05-12T14:05:23Z)
• Formal Analysis of the Contract Automata Runtime Environment with Uppaal: Modelling, Verification and Testing [0.3807314298073301]
  A distributed runtime application called tt CARE has been introduced to realise service applications specified using a dialect of finite-state automata.<n>We detail the formal modelling, verification and testing of tt CARE.
  arXiv  Detail & Related papers  (2025-01-22T15:03:25Z)
• Surrogate Neural Networks Local Stability for Aircraft Predictive Maintenance [1.6703148532130556]
  Surrogate Neural Networks are routinely used in industry as substitutes for computationally demanding engineering simulations. Due to their performance and time-efficiency, these surrogate models are now being developed for use in safety-critical applications.
  arXiv  Detail & Related papers  (2024-01-11T21:04:28Z)
• An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic [57.24311218570012]
  This approach allows for the computer-assisted analysis of abstract dialectical frameworks. Exemplary applications include the formal analysis and verification of meta-theoretical properties.
  arXiv  Detail & Related papers  (2023-12-08T09:32:26Z)
• Using Ontologies for the Formalization and Recognition of Criticality for Automated Driving [0.0]
  Recent advances suggest the ability to leverage relevant knowledge in handling the inherently open and complex context of the traffic world. This paper demonstrates to be a powerful tool for modeling and formalization of factors associated with criticality in the environment of automated vehicles. We elaborate on the modular approach, present a publicly available implementation, and evaluate the method by means of a large-scale drone data set of urban traffic scenarios.
  arXiv  Detail & Related papers  (2022-05-03T14:32:11Z)
• Explainability in Process Outcome Prediction: Guidelines to Obtain Interpretable and Faithful Models [77.34726150561087]
  We define explainability through the interpretability of the explanations and the faithfulness of the explainability model in the field of process outcome prediction. This paper contributes a set of guidelines named X-MOP which allows selecting the appropriate model based on the event log specifications.
  arXiv  Detail & Related papers  (2022-03-30T05:59:50Z)
• Modeling and Automating Public Announcement Logic with Relativized Common Knowledge as a Fragment of HOL in LogiKEy [0.0]
  This article presents a semantical embedding for public announcement logic with relativized common knowledge. It enables the first-time automation of this logic with off-the-shelf theorem provers for classical higher-order logic. The work constitutes an important addition to the pluralist LogiKEy knowledge engineering methodology.
  arXiv  Detail & Related papers  (2021-11-02T15:14:52Z)
• Automated Evolutionary Approach for the Design of Composite Machine Learning Pipelines [48.7576911714538]
  The proposed approach is aimed to automate the design of composite machine learning pipelines. It designs the pipelines with a customizable graph-based structure, analyzes the obtained results, and reproduces them. The software implementation on this approach is presented as an open-source framework.
  arXiv  Detail & Related papers  (2021-06-26T23:19:06Z)
• CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT (Extended Version) [62.96267257163426]
  We introduce the CoCoMoT (Computing Conformance Modulo Theories) framework. First, we show how SAT-based encodings studied in the pure control-flow setting can be lifted to our data-aware case. Second, we introduce a novel preprocessing technique based on a notion of property-preserving clustering.
  arXiv  Detail & Related papers  (2021-03-18T20:22:50Z)
• Multi-Agent Reinforcement Learning with Temporal Logic Specifications [65.79056365594654]
  We study the problem of learning to satisfy temporal logic specifications with a group of agents in an unknown environment. We develop the first multi-agent reinforcement learning technique for temporal logic specifications. We provide correctness and convergence guarantees for our main algorithm.
  arXiv  Detail & Related papers  (2021-02-01T01:13:03Z)
• Machine Learning to Tackle the Challenges of Transient and Soft Errors in Complex Circuits [0.16311150636417257]
  Machine learning models are used to predict accurate per-instance Functional De-Rating data for the full list of circuit instances. The presented methodology is applied on a practical example and various machine learning models are evaluated and compared.
  arXiv  Detail & Related papers  (2020-02-18T18:38:54Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.