Upper-Bounded Model Checking for Declarative Process Models

Schützenmeier N, Käppel M, Petter S, Jablonski S (2021)

Publication Language: English

Publication Type: Conference contribution, Conference Contribution

Publication year: 2021

Publisher: Springer

Series: Lecture Notes in Business Information Processing

City/Town: Cham

Book Volume: 432

Pages Range: 195–211

Conference Proceedings Title: The Practice of Enterprise Modeling 14th IFIP WG 8.1 Working Conference, PoEM 2021, Riga, Latvia, November 24–26, 2021, Proceedings

Event location: Riga LV

ISBN: 978-3-030-91278-9

URI: https://link.springer.com/chapter/10.1007/978-3-030-91279-6_14

DOI: 10.1007/978-3-030-91279-6_14

Abstract

Declarative process modelling languages like Declare focus on describing a process by restrictions over the behaviour, which must be satisified throughout process execution. Although this paradigm allows more flexibility, it has been shown that such models are often hard to read and understand, which affects their modelling, execution and maintenance in a negative way. A larger degree of flexibility leads to a multitude of different process models that describe the same process. Often it is difficult for the modeller to keep the model as simple as possible without over- or underspecification. Hence, model checking, especially comparing declarative process models on equality becomes an important task. In this paper, we determine and prove a theoretical upper bound for the trace length up to which the process executions of Declare models must be compared, to decide with certainty whether two process models are equal or not.

Authors with CRIS profile

Martin Käppel Lehrstuhl für Digital Industrial Service Systems

Involved external institutions

Universität Bayreuth DE Germany (DE)

How to cite

APA:

Schützenmeier, N., Käppel, M., Petter, S., & Jablonski, S. (2021). Upper-Bounded Model Checking for Declarative Process Models. In Serral, Estefanía Stirna, Janis Ralyté, Jolita Grabis, Jānis (Eds.), The Practice of Enterprise Modeling 14th IFIP WG 8.1 Working Conference, PoEM 2021, Riga, Latvia, November 24–26, 2021, Proceedings (pp. 195–211). Riga, LV: Cham: Springer.

MLA:

Schützenmeier, Nicolai, et al. "Upper-Bounded Model Checking for Declarative Process Models." Proceedings of the IFIP Working Conference on The Practice of Enterprise Modeling, Riga Ed. Serral, Estefanía Stirna, Janis Ralyté, Jolita Grabis, Jānis, Cham: Springer, 2021. 195–211.

BibTeX: Download