Source-linked AI summary
Conformance Checking Based on Multi-Perspective Declarative Process Models
Andrea Burattin, Fabrizio Maria Maggi, Alessandro Sperduti
TL;DR
The paper addresses the limited support for conformance checking with declarative models when data, time, and control-flow perspectives must be considered together. It proposes MP-Declare and a template-based checking framework, implemented in ProM, with linear dependence on traces, constraints, and trace events and evaluation on artificial and real logs.
Problem
Conformance checking needs declarative models for complex, variable processes, but integrated support for data, temporal, and control-flow perspectives is limited.
Method
The paper defines MP-Declare using Metric First-Order Linear Temporal Logic and develops a template-based framework for checking event logs against its constraints.
Results
The framework is linear in the number of traces, constraints, and events per trace, with worst-case quadratic complexity, and is evaluated on logs up to 5 million events plus three real business processes.
Takeaways & Limitations
MP-Declare provides a framework for conformance checking that jointly represents data, temporal, and control-flow conditions and supports the entire set of MP-Declare templates in ProM.
Takeaways & Limitations
The approach assumes that all XES attributes are globally visible and accessible or manipulable.
Abstract
from arXiv · showhide
Process mining is a family of techniques that aim at analyzing business process execution data recorded in event logs. Conformance checking is a branch of this discipline embracing approaches for verifying whether the behavior of a process, as recorded in a log, is in line with some expected behaviors provided in the form of a process model. The majority of these approaches require the input process model to be procedural (e.g., a Petri net). However, in turbulent environments, characterized by high variability, the process behavior is less stable and predictable. In these environments, procedural process models are less suitable to describe a business process. Declarative specifications, working in an open world assumption, allow the modeler to express several possible execution paths as a compact set of constraints. Any process execution that does not contradict these constraints is allowed. One of the open challenges in the context of conformance checking with declarative models is the capability of supporting multi-perspective specifications. In this paper, we close this gap by providing a framework for conformance checking based on MP-Declare, a multi-perspective version of the declarative process modeling language Declare. The approach has been implemented in the process mining tool ProM and has been experimented in three real life case studies.
1. Introduction
The paper addresses conformance checking in dynamic, complex processes where procedural models become unwieldy and declarative models need integrated multi-perspective support. It proposes MP-Declare and an efficient checking framework, evaluated on artificial and real event logs.
- Dynamic markets require frequent process modifications, making conformance checking against intended business models important.
- Procedural formalisms can produce intricate “spaghetti”-like workflows that are difficult to visualize for complex processes.
- Declarative models avoid such workflows by specifying constraints that allow any behavior not violating them, while prior approaches offered limited integrated multi-perspective checking.
- MP-Declare extends Declare with jointly defined data, temporal, and control-flow conditions using Metric First-Order Linear Temporal Logic.
- The proposed framework is linear in traces, constraints, and events per trace, with worst-case quadratic time complexity across template procedures.
- Evaluation uses artificial logs containing up to 5 million events and real logs from three business processes.
2. Related Work
Related work covers procedural and declarative conformance checking, including logic- and automata-based approaches, runtime monitoring, alignments, and medical applications. The paper distinguishes its contribution by formally connecting control-flow, data, and temporal perspectives.
- Conformance checking traditionally compares event-log behavior with procedural process models.
- Declarative conformance approaches have used abductive logic programming, LTL with automata, and service-choreography validation.
- MFOTL-based compliance work focuses on monitoring and enforcing security policies, including distinctions between controllable and observable activities.
- Declare has been applied to medical guidelines, but those analyses omit both data and time perspectives.
- Other Declare approaches identify fulfilled and violated constraints or produce aligned traces, but do not fully integrate data and temporal perspectives.
- This paper connects data, temporal, and control-flow perspectives within a formal MP-Declare semantics.
3. Preliminaries
The preliminaries introduce event logs, MFOTL, Declare’s open-world constraint semantics, and activation-based conformance concepts. Declare templates express permitted activity relationships without explicitly enumerating execution paths.
- Process Mining and XES: Process mining starts from event logs that support discovering, monitoring, and improving processes.
- Process Mining and XES: Each trace is a time-ordered sequence of case events that may include resources, timestamps, event attributes, and case attributes.
- Metric First Order Temporal Logic: MFOTL combines first-order logic with metric temporal modalities for finite traces.
- Metric First Order Temporal Logic: A timed temporal structure is a finite sequence of structures paired with monotonically increasing natural-number timestamps and constant domains.
- Metric First Order Temporal Logic: MFOTL formulas use equality, relations, logical connectives, quantification, and timed future, past, until, and since operators.
- Declare: Declare uses constraints and templates to specify an open set of allowed activity orderings rather than a closed procedural workflow.
- Declare: Response requires a later target after each activation, while alternate and chain templates impose progressively stronger alternation or adjacency requirements.
- Declare: A constraint activation is fulfilled or violated depending on whether its required behavior occurs; violation and fulfillment ratios measure these outcomes over activations.
4. MFOTL Semantics for Multi-Perspective Business Constraints
MP-Declare extends Declare with MFOTL-based data and time conditions linked to control-flow templates. Its semantics distinguish activation, correlation, and timing requirements across response variants.
- MP-Declare enriches Declare with integrated data and time perspectives and provides semantics suitable for conformance-checking algorithms.
- An event’s activity and payload attributes are interpreted through XES valuations in the temporal semantics.
- MP-Declare templates use an activation and a target parameter, with data conditions extending timed Declare semantics.
- The activation condition determines whether an occurrence activates a constraint, while the correlation condition must hold when the target occurs.
- Response requires a qualifying target within a specified time interval; alternate response forbids qualifying repeated activations before that target.
- Chain response requires the target to occur next, with fulfillment or violation depending on correlation and time conditions.
5. Conformance Checking Algorithms
The paper defines algorithms for checking event-log conformance against MP-Declare constraints that jointly capture control-flow, temporal, and data conditions. A general framework processes traces and constraints using template-specific procedures for identifying fulfillments and violations.
- General framework: CheckLogConformance compares an event log with an MP-Declare model by evaluating every trace against every constraint.It returns fulfilling and violating traces or constraints through CheckTraceConformance.
- Template procedures: The framework requires opening, activation, fulfillment, violation, and closing operations for each supported constraint template.Opening and closing run once per trace, while activation, fulfillment, and violation process trace events.
- Multi-perspective constraints: MP-Declare constraints combine activation, correlation, and time conditions over activation and target activities.The constraint representation includes a template, activation and target sets, and conditions ϕa, ϕc, and ϕτ.
- Response templates: Response procedures fulfill pending activations when correlated targets satisfy time and correlation conditions, while unresolved activations become violations.The response template checks activation conditions when adding pending activations and classifies unmatched pending activations after trace processing.
- Response templates: Alternate response permits fulfillment through possible targets while enforcing at most one pending activation in the relevant checks.Its procedures maintain a possibleTargets structure and classify a pending activation as fulfilled or violated based on target, time, and correlation conditions.
- Response templates: Chain response checks the single pending activation against the current target and marks it fulfilled only when the temporal and correlation conditions hold.The paper presents response, alternate response, and chain response procedures, deriving precedence variants by parsing traces in reverse.
- Complexity: The main algorithm is linear in the number of traces, constraints, and events per trace, while template procedures add template-dependent costs.For response and alternate response, fulfillment and closing can be linear in pending activations or possible targets; chain response operations are mostly constant except closing.
6. Implementation and Benchmarks
The approach was implemented in ProM with visual tools for log-wide and case-level conformance inspection, then benchmarked across logs of varying sizes and trace lengths. Execution time increased with both trace length and log size, while the largest tested configuration completed in about 4.2 minutes.
- Implementation: The MP-Declare conformance checker was implemented as a ProM plug-in that receives an event log and a model.Trace processing and constraint analysis are independent, allowing parallelization.
- Visualization: The Analysis Result Visualizer summarizes activations, violations, and fulfillments for each constraint across the entire log.Additional windows support detailed case-and-constraint inspection and a birdview overview of possible issues.
- Benchmark design: The benchmark used 20 generated logs with trace lengths of 10–50 events and log sizes of 25,000–100,000 traces.Each log was checked against each model and tested five times to obtain average execution times.
- Benchmark results: Execution time depended directly on both the number of events per trace and the overall log size.Control-flow models were more influenced by trace length, whereas multi-perspective models incurred additional data-validation startup costs per trace.
- Benchmark results: 255 369 milliseconds were required by the most expensive configuration: 50 multi-perspective constraints, 100,000 traces, and 5,000,000 events.The authors report this as approximately 4.2 minutes and state that it demonstrates scalability.
7. Case Studies
Three real-life case studies apply MP-Declare conformance checking to healthcare, financial, and banking event logs. The analyses combine control-flow, data, resource, and temporal constraints while reporting low execution times.
- Case-study settings: Three case studies use real datasets from an academic hospital, a Dutch financial institution, and a bank.The hospital log concerns cancer treatment; the financial log concerns personal loans or overdrafts.
- 7.1. A Large Academic Hospital: The healthcare analysis identifies violations of tumor-marker and consultation constraints, with around 70% of 343 activations violating constraint 1.Some follow-ups were correlated with computed tomography or ultrasound tests rather than the required “ca-125” test.
- 7.2. A Dutch Financial Institution: In the financial case, 13 087 submitted applications yielded 5 113 eventual acceptances, while around 79% of accepted applications were accepted within 24 hours.Acceptance was almost 30% below 10 000 requested and almost half when the requested amount was at least 10 000.
- 7.2. A Dutch Financial Institution: Validation constraints show that almost 99% of scheduled validations started, around 94% started within 7 days, and 97% were completed within at most 1 hour.The execution time for this case study averaged between 2 and 3 seconds.
- 7.3. Rabobank: The banking case found that around 99% of open calls were eventually closed, with urgency-related closure differences between KM0000611 and KM0002043.725 of over 773 KM0002043 calls closed within 12 hours, compared with 60 of over 446 KM0000611 calls; execution times ranged from 4 to 5 seconds.
8. Conclusion and Future Work
The paper presents an implemented MP-Declare conformance-checking framework covering the full set of MP-Declare templates and standard Declare. Experiments on real-life and synthetic logs support applicability in realistic settings, while future work targets online violation detection.
- Conclusion: The proposed framework checks event-log conformance against MP-Declare models, which express control-flow, data, and time constraints.MP-Declare extends Declare for multi-perspective constraint specification.
- Conclusion: The implementation in ProM covers the entire set of MP-Declare templates and can also check standard Declare models.The paper reports wide experimentation using real-life and synthetic logs.
- Conclusion: Real-life and synthetic case studies support the applicability of the implementation in realistic settings.The authors distinguish retrospective deviation recognition from prospective online violation detection.
- Future Work: Future work will adapt the framework for online settings to detect violations as they occur.The paper identifies online detection as a planned extension beyond a-posteriori conformance checking.