This repository contains the implementation and experimental toolbench presented in the paper “From Sound Workflow Nets to LTLf Declarative Specifications by Casting Three Spells" 🧙 submitted at the 23rd International Conference on Business Process Management (BPM 2025).The work presents a systematic approach to synthesizing declarative process specifications from safe and sound Workflow Nets (WF nets), ensuring full behavioral preservation. Here you’ll find the complete toolchain and experimental setup, tested on both synthetic and real-world datasets, used to analyze the correctness and performance of the implemented algorithm.
Sp3llsWizard has the ability to formally synthesize DECLARE specifications from safe and sound Workflow Nets. This proof-of-concept implementation automatically generates LTLf constraints from an input WF net provided as a .pnml file.
git clone https://github.com/l2brb/Sp3llsWizard.git
cd Sp3llsWizard
conda create -n sp3lls-env python=3.13 -y -f environment.yml
conda activate sp3lls-env
python3 main.py declare-synth --pnml-file ${INPUT_WN} --output-format json --output-path ${OUTPUT_PATH}The main content of the repository is structured as follows:
- /src/: the root folder of the implementation source code
- /src/declare_translator: contains the algorithm's implementation
- /evaluation/: folder containing code, datasets and results of our tests
- /evaluation/bisimulation/ contains the bisimulation test data
- /evaluation/set_cardinality/ includes test data on memory usage and execution time as the cardinality of the constraint set varies.
- /evaluation/formula_size/ includes tests data on memory usage and execution time under varying constraints formula size
- /evaluation/realworld/ includes the memory usage and execution time tests data for real-world process models
- /diagnostics/: folder containing a downstream application of our algorithm for process diagnostics
- Running on Python 3.13.0.
- Tested on:
- Ubuntu Linux 24.04.1
- macOS
- Windows 11 (via WSL or Unix-like shell)
- No installation is required — just clone, create the python environment with dependencies and run.
python3 main.py declare-synth --pnml-file ${INPUT_WN} --output-format json --output-path ${OUTPUT_PATH}
We evaluated our algorithm on a range of both synthetic and real-world data. For the real-world testbed, we take as input processes discovered by a well-known imperative process mining algorithm from a collection of openly available event logs. We conducted the performance tests on an AMD Ryzen 9 8945HS CPU at 4.00 GHz with 32 GB RAM running Ubuntu 24.04.1.
To experimentally validate the correctness of our approach, we run a bisimualtion test. To this end, we collected a set of WF nets both from synthetic generation and literature. We performed the comparison of the reachability FSA of WF nets and the specification FSA consisting of the Declare constraints returned by our tool.
Generating Reachability FSA from WF nets
To generate the Reachability FSA, execute:
bisimulation.pyThis script:
- Loads the WF net.
- Constructs its Reachability Graph.
- Converts it to an FSA suitable for bisimulation comparison.
Specification FSA
To generate the Specification FSA from DECLARE constraints, execute the MINERfulSimplifier module included in MINERful:
./run-MINERfulSimplifier -iSF ${INPUT_MODEL} -iSE json -autoDOT ${OUTPUT_PATH} This comparison allows to verify that our DECLARE specifications faithfully represent the behavior of the original Workflow Nets. The bisimulation test results are available in /output/.
To evaluate the runtime memory utilization and execution time of our Sp3llsWizard implementation, we run a performance test, split into two different configurations.
We rely on an iterative expansion mechanism, implemented in /expansion_rules/, that applies four soundness-preserving transformation rules to progressively grow a Workflow net. Starting from a base net, we fix a central transition (t1) as a pivot and preserve the initial and final places (p1, p2). At each iteration:
- A transition is split into two, extending the activity sequence.
- Parallel paths are introduced to add concurrency.
- Conditional branches are added to create alternative paths.
- Loops are added for iteration.
This process is repeated for 1000 iterations, each time expanding the net and applying our algorithm.
Results are available in /cardinality_test_results/.
Here, we configure the test on memory usage and execution time to investigate the algorithm’s performance while handling an expanding constraints’ formula size (i.e., with an increasing number of disjuncts). To this end, we progressively broaden the Workflow net by applying the soundness-preserving conditional expansion rule.
To evaluate the performance of our algorithm on real process models, we run memory usage and execution time tests on workflow nets derived from real-world event logs. First, we generate workflow nets by applying the Inductive Miner algorithm, available in pm4py.
python3 miner.pyWe run our algorithm on the generated workflow nets to derive the corresponding Declare specification in JSON format. The scripts record memory usage (in MB) and execution time (in ms) during processing.
| Event log | Trans. | Places | Nodes | Mem.usage [MB] | Exec.time [ms] | Model |
|---|---|---|---|---|---|---|
| BPIC 12 | 78 | 54 | 174 | 19.97 | 5.11 | bpic12.pnml |
| BPIC 13cp | 19 | 54 | 44 | 19.76 | 1.70 | bpic13cp.pnml |
| BPIC 13inc | 23 | 17 | 50 | 19.89 | 2.03 | bpic13inc.pnml |
| BPIC 14f | 46 | 35 | 102 | 19.90 | 3.31 | bpic14f.pnml |
| BPIC 151f | 135 | 89 | 286 | 20.44 | 8.39 | bpic151f.pnml |
| BPIC 152f | 200 | 123 | 422 | 20.91 | 12.30 | bpic152f.pnml |
| BPIC 153f | 178 | 122 | 396 | 20.77 | 11.49 | bpic153f.pnml |
| BPIC 154f | 168 | 115 | 368 | 20.55 | 11.38 | bpic154f.pnml |
| BPIC 155f | 150 | 99 | 320 | 20.43 | 9.16 | bpic155f.pnml |
| BPIC 17 | 87 | 55 | 184 | 19.91 | 5.67 | bpic17.pnml |
| RTFMP | 34 | 29 | 82 | 19.81 | 3.47 | rtfmp.pnml |
| Sepsis | 50 | 39 | 116 | 19.75 | 3.65 | sepsis.pnml |
This module tests the usage of the synthesized constraints as determinants of process diagnosis. We aim to demonstrate how we can single out the violated rules constituting the process model behavior, thereby spotlighting points of non-compliance with processes.
To this end, we developed a dedicated diagnostic module that extends a declarative specification miner for constraint checking via the replay of runs on semi-symbolic automata.
./run-MINERfulFitnessChecker-unstable.sh -iLF ${INPUT_LOG} -iLF xes -oCSV ${OUTPUT_PATH}As a test case, we use real-world data from BPIC 15_5f. After preprocessing (975 valid traces), the diagnostic pipeline works as follows:
- Discover a process model from the event log using the α-algorithm.
- Translate the resulting Workflow Net into a DECLARE specification via our synthesis algorithm.
- Check the original event log against the declarative model to observe which constraints are satisfied or violated.