A software suite for translating BPMN (Business Process Model and Notation) models to IndiGolog processes and performing formal reasoning tasks over them using the Situation Calculus and ConGolog.
Read the full paper at: Formal semantics for knowledge representation and automated reasoning in BPMN process models.
This project provides a complete pipeline from BPMN models to formal reasoning:
- Translation: Convert BPMN XML files to IndiGolog representations.
- Reasoning: Perform various reasoning tasks (projection, legality checking, conformance, property verification, execution) over the translated models.
- Execution: Run BPMN processes with exogenous event handling.
- Web UI: User-friendly Gradio interface for translation and reasoning.
sitcalc4bpmn/
├── src/
│ ├── bpmn_parser.py # BPMN XML parser
│ ├── bpmn2indi_cli.py # BPMN to IndiGolog CLI translator
│ ├── prolog_templates.py # Template for the IndiGolog code generation
│ ├── prolog_translator.py # Prolog translator to generate IndiGolog code from the parsed BPMN information
│ ├── reason.py # Reasoning task executor
│ ├── reasoning_service.py # Support code for reasoning
│ ├── translator_service.py # Support code for translation
│ └── ui.py # Entry point for the GUI
├── bpmn/ # Input BPMN files
├── pl_models/ # Generated IndiGolog translations
| ├── case_study/ # BPMN and IndiGolog encoding of the case study
│ └── <model_name>/
│ ├── <model_name>.pl # Process encoding
│ └── main.pl # Main IndiGolog loader
├── indigolog/ # IndiGolog (submodule)
└── README.md # This file
- Python (>=v.3.10.12)
- SWI-Prolog (>=v.8.4.2) (
sudo apt-get install swi-prologon Ubuntu/Debian) - IndiGolog (included as submodule)
git clone https://github.com/angelo-casciani/sitcalc4bpmn
cd sitcalc4bpmnAssuming a working version of Python installed on the machine, create a virtual environment in the root folder of the project.
python3 -m venv .venv
source .venv/bin/activateRun the following command to install the necessary packages along with their dependencies in the requirements.txt file using pip:
pip install -r requirements.txtThe easiest way to use the suite is through the web interface:
python src/ui.pyThis will start a local web server (default: http://127.0.0.1:7860) and open the interface in your browser.
-
Translation Tab: Upload BPMN files and translate them to IndiGolog.
- Drag and drop .bpmn or .xml files.
- Specify a model name.
- View the generated Prolog code with syntax highlighting.
-
Load Existing Model Tab: Access previously translated models.
- Select from a dropdown of available models.
- View the translated code.
-
Reasoning Tasks Tab: Execute reasoning over your models.
- Select a reasoning task (projection, legality, etc.).
- Input parameters dynamically adapted on the selected task.
- View the results.
python src/bpmn2indi_cli.py <model_name>Example:
python src/bpmn2indi_cli.py job_applicationThis reads bpmn/job_application.bpmn and generates:
pl_models/job_application/job_application.pl(translated process)pl_models/job_application/main.pl(main IndiGolog file)
Determine if a fluent has a specific value after executing a certain sequence of actions.
python src/reason.py <model_name> projection \
--fluent <fluent_name> \
--actions <action1,action2,...> \
--expected <true|false>Examples:
Check if application(1) is true after preparing application (i.e., if an application object was created for process instance 1):
python src/reason.py job_application projection \
--fluent "application(1)" \
--actions "job_needed(1),prepare_application(end,1)" \
--expected trueCheck if waiting(1,applicant) is true after job_needed:
python src/reason.py job_application projection \
--fluent "waiting(1,applicant)" \
--actions "job_needed(1)" \
--expected trueVerify if an action sequence can be executed (all preconditions satisfied).
python src/reason.py <model_name> legality \
--actions <action1,action2,...> \
[--proc-name <procedure_name>]Examples:
# Legal action
python src/reason.py job_application legality \
--actions "job_needed(1)"
# Illegal action - fails because preconditions aren't met
python src/reason.py job_application legality \
--actions "application_sent(1)"Execute the complete BPMN process with exogenous events.
python src/reason.py <model_name> execute [--controller <number>]This opens the IndiGolog Tkinter window for issuing exogenous events. The execution history is printed at the end.
Examples:
python src/reason.py job_application execute --controller 1Exogenous events can be sent via the GUI (e.g., job_needed(1), prepare_application(end,1), end_indi to finish).
For the specific exogenous events available in the case study, please refer to the README in the pl_models/case_study folder.
Verify if an execution history conforms to the process specification.
python src/reason.py <model_name> conformance \
--history <action1,action2,...>Examples:
python src/reason.py job_application conformance \
--history "job_needed(1),acquire(1,applicant),prepare_application(start,1),prepare_application(end,1),application_sent(1),acquire(1,company)"Output includes:
- Conformance result (CONFORMANT/NON-CONFORMANT)
- Number of inferences
- CPU time
Verify process properties over the whole execution.
python src/reason.py <model_name> verify \
[--proc-name <procedure_name>]
--property <property>Examples:
python src/reason.py job_application verify --proc-name property_verification --property "signed_contract(id), neg(done(application_finalised(id)))"Start an interactive SWI-Prolog session for manual queries.
python src/reason.py job_application interactiveExample queries:
?- initialize(evaluator).
?- eval(application(1), [prepare_application(end,1), job_needed(1)], true).
?- indigolog(test_sequence).
?- halt.# Translation
python src/main.py <model_name>
# Reasoning tasks
python src/reason.py <model_name> projection --fluent <F> --actions <A> --expected <true|false>
python src/reason.py <model_name> legality --actions <A> [--proc-name <P>]
python src/reason.py <model_name> execute [--controller <N>]
python src/reason.py <model_name> conformance --history <H>
python src/reason.py <model_name> verify [--property <P>]
python src/reason.py <model_name> interactive
# Get help
python src/reason.py --help
python src/reason.py <model_name> <task> --helpHere's a complete workflow from BPMN to reasoning:
# 1. Translate BPMN to IndiGolog
python src/main.py job_application
# 2. Test projection queries
python src/reason.py job_application projection \
--fluent "application(1)" \
--actions "job_needed(1),prepare_application(end,1)" \
--expected true
# 3. Check action legality
python src/reason.py job_application legality \
--actions "job_needed(1)"
# 4. Execute the process (opens GUI for exogenous events)
python src/reason.py job_application execute --controller 1
# Send events via GUI: job_needed(1), prepare_application(end,1), end_indi
# 5. Check conformance of an execution trace
python src/reason.py job_application conformance \
--history "job_needed(1),acquire(1,applicant),prepare_application(start,1)"
# 6. Verify custom properties
python src/reason.py job_application verify --property "signed_contract(id), neg(done(application_finalised(id)))"For the dataset, setup, and results of the evaluation for the suite, please refer to the README in the evaluation folder.
See LICENSE for details.
If you use this repository in your research, please cite:
@article{CASCIANI2026102718,
title = {Formal semantics for knowledge representation and automated reasoning in BPMN process models},
journal = {Information Systems},
volume = {140},
pages = {102718},
year = {2026},
issn = {0306-4379},
doi = {https://doi.org/10.1016/j.is.2026.102718},
url = {https://www.sciencedirect.com/science/article/pii/S0306437926000323},
author = {Angelo Casciani and Simone Agostinelli and Yves Lespérance and Andrea Marrella and Sebastian Sardiña},
keywords = {AI-augmented business process management systems, ConGolog, Formal semantics of BPMN, Knowledge representation and automated reasoning, Process modeling, Situation Calculus},
abstract = {The Business Process Modeling Notation (BPMN) is the de facto standard for business process modeling. While widely adopted for its intuitive graphical notation, its execution semantics described in natural language lacks a commonly agreed formal foundation, leading to variability in execution across different BPM systems (BPMSs) and increasing the risk of creating models with semantic errors costly to correct at runtime. Although many formalisms have been used to model portions of BPMN, their reasoning capabilities are mostly restricted to control-flow, making them unsuitable for semantic analysis where data and global exception handling play a central role in execution. To address this, we propose a formalization from BPMN to ConGolog, a logical concurrent processes language based on the Situation Calculus, for representing and reasoning about dynamic domains. A major innovation is using ConGolog to rigorously capture the semantics of BPMN global exceptions. Our framework supports advanced reasoning, allowing for semantic analysis of BPMN models before execution to predict runtime errors within a safe simulation setting, while laying the foundation for reasoning layers in next-generation AI-augmented BPMSs. We validate the approach through a prototype and comprehensive evaluation, demonstrating the computational feasibility of the translation and the semantic correctness of reasoning tasks.}
}