Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Direct Encoding of Declare Constraints in ASP

Francesco Chiariello, Valeria Fionda, Antonio Ielo, Francesco Ricca

TL;DR

This paper addresses direct encoding of Declare constraints in ASP, avoiding intermediate $LTL_f$ or automata representations. It introduces an ad-hoc, direct ASP encoding for Declare templates and evaluates it on conformance checking and template query checking, comparing against automata- and syntax-tree-based encodings as well as the Declare4Py Python library, with a common input fact schema. Experiments on real logs (e.g., Sepsis Cases and BPI challenges) show the direct encoding (ASP_D) outperforms other ASP encodings and the Python library in runtime, while memory usage favors dedicated libraries in some settings; the work discusses trade-offs and potential extensions. Overall, the approach demonstrates that ASP can succinctly and efficiently encode Declare constraints, with potential for extension to data-aware and probabilistic variants in Process Mining.

Abstract

Answer Set Programming (ASP), a well-known declarative logic programming paradigm, has recently found practical application in Process Mining. In particular, ASP has been used to model tasks involving declarative specifications of business processes. In this area, Declare stands out as the most widely adopted declarative process modeling language, offering a means to model processes through sets of constraints valid traces must satisfy, that can be expressed in Linear Temporal Logic over Finite Traces (LTLf). Existing ASP-based solutions encode Declare constraints by modeling the corresponding LTLf formula or its equivalent automaton which can be obtained using established techniques. In this paper, we introduce a novel encoding for Declare constraints that directly models their semantics as ASP rules, eliminating the need for intermediate representations. We assess the effectiveness of this novel approach on two Process Mining tasks by comparing it with alternative ASP encodings and a Python library for Declare. Under consideration in Theory and Practice of Logic Programming (TPLP).

Direct Encoding of Declare Constraints in ASP

TL;DR

This paper addresses direct encoding of Declare constraints in ASP, avoiding intermediate or automata representations. It introduces an ad-hoc, direct ASP encoding for Declare templates and evaluates it on conformance checking and template query checking, comparing against automata- and syntax-tree-based encodings as well as the Declare4Py Python library, with a common input fact schema. Experiments on real logs (e.g., Sepsis Cases and BPI challenges) show the direct encoding (ASP_D) outperforms other ASP encodings and the Python library in runtime, while memory usage favors dedicated libraries in some settings; the work discusses trade-offs and potential extensions. Overall, the approach demonstrates that ASP can succinctly and efficiently encode Declare constraints, with potential for extension to data-aware and probabilistic variants in Process Mining.

Abstract

Answer Set Programming (ASP), a well-known declarative logic programming paradigm, has recently found practical application in Process Mining. In particular, ASP has been used to model tasks involving declarative specifications of business processes. In this area, Declare stands out as the most widely adopted declarative process modeling language, offering a means to model processes through sets of constraints valid traces must satisfy, that can be expressed in Linear Temporal Logic over Finite Traces (LTLf). Existing ASP-based solutions encode Declare constraints by modeling the corresponding LTLf formula or its equivalent automaton which can be obtained using established techniques. In this paper, we introduce a novel encoding for Declare constraints that directly models their semantics as ASP rules, eliminating the need for intermediate representations. We assess the effectiveness of this novel approach on two Process Mining tasks by comparing it with alternative ASP encodings and a Python library for Declare. Under consideration in Theory and Practice of Logic Programming (TPLP).

Paper Structure

This paper contains 4 sections, 1 equation, 1 figure, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Process Mining
  4. Linear Temporal Logic over Finite Traces

Figures (1)

  • Figure 1: Left: Minimal automaton for the LTL$_\text{f}$ formula $\varphi = \textsf{G}(a \rightarrow \textsf{X}\textsf{F} b)$. Models (labeling the transitions) represent sets of symbols; Right: Minimal automaton for $\varphi$ interpreted as a LTL$_\text{p}$ formula, where $*$ denotes any $x \in \mathcal{A} \setminus \{a, b\}$. A comma on edges denotes multiple transitions.