current tools

These are relevant tools under actual development, either by current/former members of my group, or by colleagues with whom we have actively collaborated (on the tool development, and/or on its foundations).

  • onprom, a toolchain based on semantic technologies for extracting event data from relational databases.
  • ADA - Arithmetic DDS Analyzer, a framework for the linear- and branching-time verification of data-aware dynamic systems and data Petri nets operating over (numerical) data variables (visual interface here).
  • db-driven MCMT, the module of the SMT-based MCMT model checker dedicated to checking safety properties over relational processes with read-only and read-write databases.
  • CoCoMoT, an SMT-based conformance checking tool modulo theories for computing alignments on data Petri nets (also dealing with uncertainty in the log).
  • SAFE - Swarm Safety Detector, a web interface for SMT-based verification of parameterized MASs with different synchronization semantics, via encoding into the MCMT model checker
  • RuM - Rule Mining made simple, a desktop application that provides a comprehensive set of declarative process mining tools in a single unified package.

old tools
(discontinued, but hopefully still working)


jREC is a JAVA+Prolog-based tool for reasoning upon the dynamics of an event-based system with respect to an Event Calculus specification. More specifically, jREC dynamically acquires the event occurrences characterizing a running execution of the system and monitors their effects by updating the evolution of the corresponding fluents (i.e. properties varying over time) according to an Event Calculus theory. jREC is based on a lightweight axiomatization of Chittaro and Montanari's Cached Event Calculus (see the paper Efficient Temporal Reasoning in the Cached Event Calculus), which captures a form of proactive reasoning where the current fluents' maximal validity intervals are cached and then updated/revised as new event occurrences get to be known. In this way, the reasoner avoids restarting from scratch every time a new event happens (which is the case of classical EC deductive reasoners), thus tracking the system's execution efficiently.

jREC combines two modules:

  • jREC (core), the reasoner;
  • jREC UI, a user interface that graphically depicts the evolution of fluents in response to events.
In addition, a jREC tester is available as a runnable JAR. Two other tools are based on jREC: MOBUCON and ComMon.

jREC is the core package containing the reasoner interface, a reasoner implementation consisting of a lightweight Prolog-based axiomatization of the Cached Event Calculus and TuProlog as the Prolog engine, and the JAVA models for storing execution traces and the evolution of fluents.

The Event Calculus ontology (i.e. the predicates supported by the calculus and that can be defined and/or used in the domain-dependent theory) of jRec contains the following predicates:

  • initially(F) - fluent F holds in the initial state;
  • initiates(E,F,T) - event E is able to make F true at time T;
  • terminates(E,F,T) - event E is able to make F false at time T;
  • happens(E,T) - event E occurs at time T (also used ground inside the description of an execution trace);
  • holds_at(F,T) - fluent F is true at time T (usable only in the body of a clause as a tester);
Furthermore, jREC adopts a specific binary term status/2 to model multi-valued fluents, where status(F,S) means that fluent F has current value S. A simple domain-dependent theory can be downloaded here.

The reasoner interface RecEngine contains the following methods:

  • public boolean setModel(String model) throws Exception - sets a domain-dependent theory (embedded in a string).
  • public FluentsModel start() throws Exception - starts the reasoner; the returned fluents' model contains all the fluents that hold initially.
  • public FluentsModel evaluateTrace(RecTrace trace) throws Exception - evaluates a chunk of event occurrences (i.e. a partial or complete trace) extending/revising the previously computed result and returning the fresh one; if the trace is closed, then the reasoner clears the cached result. Note that event occurrences can be also delivered out of order.
  • public long getStats() - returns the ms needed by the reasoner to process the last chunk of events.
  • public boolean shutDown() throws Exception - shuts down the reasoner.


The sources of jREC can be found here. The tool depends on TuProlog and on Log4J. Recall that the the tool is a research prototype, is undocumented and will print a lot of nonsense debug messages. A new, more mature version of the tool is likely to be implemented soon.

jREC UI is a user interface package for the visualization of a fluents' model. Each "normal" fluent is visualized in a row, showing the time intervals in which it holds; all the status fluents referring to the same fluent are packed in the same row, supposing that each fluent can be in a single status at a given time.


The sources of jREC can be found here. The package depends on JFreeChart, on the ui package SlickerBox developed by Fluxicon, and on the two ui packages UItopia and UITopiaResouces (see ProM 6). Recall that the package is still under development.

jREC Tester is a simple tester tool for jREC. It contains a runnable JAR which is composed of the tester, jREC UI and jREC core, together with the needed libraries. It also contains a resources subfolder with two property files for the coloring of normal and status fluents and with the file containing the domain-dependent theory. The screenshots above show the modeling and run panels of the tester. Note that:

  • The save button will always work on that file (overwriting it). In order to preserve a certain domain theory, copy the model.txt file.
  • The domain-dependent theory must use term exec(Event) for representing events, while event occurrences are simply given in the run panel as Event Time, one per row.
  • Each time the log button is pressed, all the event occurrences contained in the panel are delivered to the reasoner.


jREC Tester can be downloaded here. Unzip the file and simply double click on the JAR, without changing the name of the subfolder and of the resource files contained inside it.


jREC has been developed by Marco Montali during his Post-Doc within the AI group at DEIS, University of Bologna.


MOBUCON is a tool for the runtime monitoring of event-based systems with respect to business constraints. It tracks a running execution trace showing how it instantiates the business constraints of interests, reporting for each instance whether it is currently satisfied (i.e. the execution trace complies with it), pending (i.e. further events are needed to achieve compliance) or violated (i.e. the execution trace does not comply with it). More specifically, MOBUCON is composed of:

  • an Event Calculus-based axiomatization of CLIMB constraints, i.e., ConDec constraints extended with metric temporal aspects, data and data-aware conditions;
  • jREC as the underlying dynamic reasoner;
  • an operational decision support provider for ProM 6 for wrapping the reasoning facility and offering it through the ProM operational support service, together with a plug-in for parsing ConDec models exported from the DECLARE system.
  • two test clients for delivering events to the MOBUCON operational support provider, one supporting the manual insertion of events, the other loading traces from a XES event log; the clients graphically report the evolution of the business constraint instances, together with a metric measuring the health of the system (i.e., "how much" it complies with the business constraints).
A description of the framework can be found in our FASE 2012, ACM TIST 2013, and SAC 2013 papers.


MOBUCON is currently under development inside ProM 6. Two tester applications, based on jREC Tester, are available. The first tester supports the specification of ConDec constraints extended with metric temporal conditions. The application is organized in three panels:
  • meta model, containing the Event Calculus formalization of ConDec templates extended with metric temporal conditions;
  • model, containing a list of facts representing the specific ConDec model to be monitored;
  • run, the panel for delivering event occurrences and see the outcome.
See the sample content to have a grasp about the approach. The second tester is related to our SAC 2013 paper, and extends the previous one with non-atomic activities and data-related conditions. A new version of the tool is likely to come soon.


The implementation of MOBUCON has been started by Marco Montali in july 2011, when he was visiting researcher at the Eindhoven University of Technology. A special thank goes to Wil van der Aalst and Fabrizio Maggi, and to the Netherlands Organisation for Scientific Research (NWO), that financially supported the visit.


ComMon is a tool for the runtime monitoring of business interactions against social commitments that are mutually established by the interacting stakeholders. More specifically, ComMon is composed of:

  • an Event Calculus-based axiomatization of the commitments' lifecycle and the operations by manipulating commitments; the axiomatization stems from the seminal paper of Pinar and Singh (Flexible Protocol Specification and Execution: Applying Event Calculus Planning using Commitments), and extends it by supporting also compensating commitments and (existential and universal) timed commitments, i.e., commitments related to a property that must be brought about inside some time interval, or uninterruptedly maintained true along some time interval;
  • jREC as the underlying reactive reasoner.
A description of the framework can be found in our AT2AI 2010, DALT 2011, and JAAMAS papers.


A tester application for ComMon, based on the jREC Tester, can be downloaded here. The tester is organized in three panels:
  • meta model, containing the Event Calculus formalization of the lifecycle of timed commitments;
  • model, containing a list of facts representing the specific commitment model to be monitored;
  • run - the panel for delivering event occurrences and see the outcome.
See the sample content to get a glimpse of the approach (a file trace.txt is provided to show a sample trace).


ComMon has been developed by Marco Montali during his PhD and Post-Doc, when he was part of the AI group at DEIS, University of Bologna.


CLIMB (Computational Logic for the verIfication and Modeling of Business constraints) is a framework based on computational logic (extensions of logic programming in particular) for the declarative, constraint-based specification of event-based systems (such as business processes, service interaction, clinical guidelines, multi-agent interaction protocols), and for providing reasoning and verification support along their entire lifecycle.

CLIMB is extensively described in my monograph Specification and Verification of Declarative Open Interaction Models: a Logic-Based Approach.

The framework is constituted by:

  • ConDec, a graphical constraint-based language for the declarative and open specification of business constraints. The language has been proposed by Maja Pesic and Wil van der Aalst, and is the core of the DECLARE system.
  • SCIFF (based on abductive logic programming) and the Event Calculus as the underlying logic-based formal counterpart. All the ConDec constraints can be automatically translated onto a SCIFF or EC specification.

The following reasoners and tools can be used to provide support along the entire lifecycle of a ConDec specification, or of a third-party interaction model:

  • Properties verification, a-priori compliance verification and composition are tackled by the g-SCIFF proof procedure, the generative variant of the SCIFF proof procedure (see Ch. 8, 9, 10 and 11 of the book). A special SCIFF template project (see the SCIFF manual), dealing with the specification and verification of CLIMB constraints, can be downloaded here. The project provides a facility for automatically producing, starting from a simple description of a CLIMB model (see the sample file, the corresponding SCIFF representation; it is executed when the project is loaded. Furthermore, it provides a number of utilities for properties verification, such as conflicts detection and discovery of dead activities (see
  • On-the-fly compliance verification is tackled by the SCIFF proof procedure, interleaving it with g-SCIFF in case of speculative runtime verification (see Ch. 13 of the book).
  • Monitoring is tackled by means of the Event Calculus and corresponding runtime reasoners (see Ch. 14 of the book). The currently supported runtime reasoner is jREC, and the monitoring tool for extended ConDec models is MOBUCON. Alternatively, a reactive EC reasoner again based on SCIFF is described in Ch. 14 of the book and in the paper A Logic-Based, Reactive Calculus of Events.
  • Enactment is managed by interleaving monitoring and speculative runtime verification (see Ch. 14 of the book).
  • Declarative process mining (model discovery and trace analysis) are respectively handled by SCIFF or Prolog and by the Inductive Logic Programming algorithm described in the paper Exploiting Inductive Logic Programming Techniques for Declarative Process Mining. Two ProM plug-ins have been developed for dealing with these tasks: SCIFF Checker for conformance checking and DecMiner for model discovery.


The CLIMB framework has been investigated by Marco Montali during his PhD and Post-Doc, when he was part of the AI group at DEIS, University of Bologna. The SCIFF framework has been developed by the AI Groups at DEIS, University of Bologna, and ENDIF, University of Ferrara. DecMiner has been developed by Evelina Lamma, Fabrizio Riguzzi, and Sergio Storari (AI Group at ENDIF, University of Ferrara). Part of this investigation has been carried out visiting the AIS group at the Eindhoven University of Technology, and in particular collaborating with Prof. Wil van der Aalst, Maja Pesic and Fabrizio Maggi.

SCIFF Checker

SCIFF Checker is a process mining tool for conformance checking and ex-post analysis of event logs. It is implemented in JAVA+Prolog as a plug-in of ProM. The plug-in classifies the execution traces contained inside an event log as compliant or noncompliant with respect to a business rule. Rules are expressed in a pseudo-natural language notation and are inspired by the patterns of the ConDec language extended with metric time constraints and originators.

Step 1
The user selects an abstract business rule from a set of templates. Rules contain event patterns and expectations, which are in turn associated to an activity name, an event type (e.g. start, complete, abort of an activity), an originator and an execution time.
Step 2
By clicking on the "customize" button, all the editable parts of the rule becomes visible and active. An element can be edited by fixing its value and/or adding specific constraints. Customized rules can be saved for future re-use.
Step 3
Finally, the user can fix the time granularity used for the analysis and launch the analysis task. Such a task is carried out in Prolog, using the approach described in the paper Checking Compliance of Execution Traces to Business Rules. The final result is a partition of the input log into a compliant and noncompliant set. A new analysis phase can be then carried out by considering the whole log or only one of the two sets. Such sets can also separately feed other plug-ins.


The tool is currently under porting on ProM 6.
The version for ProM 5 can be downloaded here. The zip file contains two subfolders, which mirror the ones contained in the ProM distribution:
  • plugins contains the jar of the plug-in (SCIFFChecker.jar) and a subfolder (SCIFFChecker) which includes two xml files that store the abstract rule templates and the user-defined rules. Both the jar and the subfolder must be copied into the <Prom Distribution>/lib/plugins/ folder of ProM.
  • external contains the external libraries required by SCIFF Checker, i.e. TuProlog and JFreeChart, which in turn requires JCommon. All these three jar files must be copied into the <Prom Distribution>/lib/external/ folder of ProM.
The last step to make SCIFF Checker work is to modify the property file <ProM Distribution>/analyses.ini, adding a new line
<NEW KEY>=org.processmining.analysis.sciffchecker.SCIFFChecker
where <NEW KEY> is a unique alpha-numeric key. SCIFF Checker will consequently appear inside the analysis menu of ProM.


SCIFF Checker has been developed by Marco Montali in the context of a research contract within the AI group at DEIS, University of Bologna. The Prolog-based analysis task is a joint work with Federico Chesani and Paola Mello (AI group at DEIS, University of Bologna) and Fabrizio Riguzzi (AI group at ENDIF, University of Ferrara).