Heerko Groefsema

For our research we implemented and use a number of Java packages that allow us to specify, unfold, and verify process compositions such as business process models and service compositions. These packages require some work, including new functionality, replacing old dependencies, adding different output formats, replacing log functionality, refactoring to use certain programming patterns, and more. In this project, we would like a number of students to improve, refactor, and add functionality. This project is available for up to 5 students, which will work on separate sub-projects such as: - Adding rich Event Log generation from random executions of annotated Petri net models. - Separating embedded data annotations and allowing execution of Petri nets using data. - Adding functionality for colored Petri nets. - Implementing improved Prime Event Structures (PES) representations of processes and unfolding (i.e., creation of PES) from Petri nets. - Replacing old dependencies and refactoring.

References:
Peot, M. A., & Smith, D. E. (1992, January). Conditional nonlinear planning. In Artificial Intelligence Planning Systems (pp. 189-197). Morgan Kaufmann. Blythe, J. (1999). An overview of planning under uncertainty. Artificial intelligence today, 85-110. Rintanen, J. (1999). Constructing conditional plans by a theorem-prover. Journal of Artificial Intelligence Research, 10, 323-352. Karlsson, L. (2001, January). Conditional progressive planning under uncertainty. In IJCAI (pp. 431-438).

References:
Groefsema, H., Beest, N.R.T.P.v., Governatori, G. (2022). On the Use of the Conformance and Compliance Keywords During Verification of Business Processes. In: Business Process Management Forum. BPM 2022. Lecture Notes in Business Information Processing, vol 458. Springer. H. Groefsema, N.R.T.P. van Beest, A. Armas-Cervantes, Efficient conditional compliance checking of business process models, Computers in Industry, Volume 115, 2020. Alin Deutsch, Richard Hull, Fabio Patrizi, and Victor Vianu. 2009. Automatic verification of data-centric business processes. In Proceedings of the 12th International Conference on Database Theory (ICDT '09). N. van Beest, H. Groefsema, A. Cryer, G. Governatori, S. C. Tosatto and H. Burke, Cross-Instance Regulatory Compliance Checking of Business Process Event Logs, in IEEE Transactions on Software Engineering, vol. 49, no. 11, pp. 4917-4931, Nov. 2023.

The practice of checking conformance of business process models has revolutionized the industry through the amount of insight it creates into the process flows of businesses. Conformance checking entails matching an event log (which details events of past executions) against a business process model (which details the prescribed process flow) through a so called alignment. Any deviation from the prescribed process flow is detected and reported. Generally, alignments are obtained by matching the so called token replay of process models (e.g., Petri nets) against events in logs. Our Transition Graphs are also obtained from token replays, but offer further insight into parallel executions than regular Reachability Graphs. As a result, we are interested in the applicability of obtaining alignments using Transition Graphs, especially when matched against event logs that include lifecycle events and thus offer parallel execution data. In this project we ask the student to implement and evaluate the applicability of such an approach.
References:
H. Groefsema, N.R.T.P. van Beest, and M. Aiello (2016) A Formal Model for Compliance Verification of Service Compositions. IEEE Transactions on Service Computing. Carmona, Josep, et al. "Conformance checking." Switzerland: Springer.[Google Scholar] (2018). BPMVerification package

The practice of checking conformance of business process models has revolutionized the industry through the amount of insight it creates into the process flows of businesses. Conformance checking entails matching an event log (which details events of past executions) against a business process model (which details the prescribed process flow) through a so called alignment. Any deviation from the prescribed process flow is detected and reported. Generally, alignments are obtained by matching the so called token replay of process models (e.g., Petri nets) against events in logs. Instead, we would like to investigate comparing event logs against a specification of ordering relations to achieve a significant performance increase.