Upper-Bounded Model Checking for Declarative Process Models

Fiche du document

Date

24 novembre 2021

Type de document
Périmètre
Langue
Identifiants
Relations

Ce document est lié à :
info:eu-repo/semantics/altIdentifier/doi/10.1007/978-3-030-91279-6_14

Collection

Archives ouvertes

Licence

http://creativecommons.org/licenses/by/




Citer ce document

Nicolai Schützenmeier et al., « Upper-Bounded Model Checking for Declarative Process Models », HAL-SHS : sciences de l'information, de la communication et des bibliothèques, ID : 10.1007/978-3-030-91279-6_14


Métriques


Partage / Export

Résumé En

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.

document thumbnail

Par les mêmes auteurs

Sur les mêmes sujets

Sur les mêmes disciplines

Exporter en