Detection of Declarative Process Constraints in LTL Formulas

Title data

Schützenmeier, Nicolai ; Käppel, Martin ; Petter, Sebastian ; Schönig, Stefan ; Jablonski, Stefan:
Detection of Declarative Process Constraints in LTL Formulas.
In: Enterprise and Organizational Modeling and Simulation. (2019) . - pp. 131-145.
ISSN 1865-1356
DOI: https://doi.org/10.1007/978-3-030-35646-0_10

Abstract in another language

Declarative process models consist of temporal constraints that a process must satisfy during execution. Constraint templates are patterns that define parameterized classes of properties. Their semantics can be formalized using formal logics such as Linear Temporal Logic (LTL) over finite traces. There exists a big amount of different constraint templates for different purposes. In practice, the variety of different templates yields complexity and performance issues with regard to model comparison, compliance checking and in particular process mining. In this paper we give a comprehensively overview about existing declare templates and transform their underlying LTL formula into the positive normal form (PNF), a canonical standard form for LTL formulas. On this basis, we present an algorithm for detecting declare templates in any LTL formula fulfilling the conditions for PNF. We reduce the number of process constraints that have to be proven by the algorithm to speed up the runtime and give some advice for further optimizations.

Further data

Item Type:	Article in a journal
Refereed:	Yes
Institutions of the University:	Faculties > Faculty of Mathematics, Physics und Computer Science > Department of Computer Science > Chair Applied Computer Science IV > Chair Applied Computer Science IV - Univ.-Prof. Dr.-Ing. Stefan Jablonski
Result of work at the UBT:	Yes
DDC Subjects:	000 Computer Science, information, general works 000 Computer Science, information, general works > 004 Computer science
Date Deposited:	21 Nov 2019 08:41
Last Modified:	21 Nov 2019 08:41
URI:	https://eref.uni-bayreuth.de/id/eprint/53362