Runtime verification of LTL-based declarative process models

F.M. Maggi, M. Westergaard, M. Montali, W.M.P. Aalst, van der

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

58 Citations (Scopus)
2 Downloads (Pure)


Linear Temporal Logic (LTL) on finite traces has proven to be a good basis for the analysis and enactment of flexible constraint-based business processes. The Declare language and system benefit from this basis. Moreover, LTL-based languages like Declare can also be used for runtime verification. As there are often many interacting constraints, it is important to keep track of individual constraints and combinations of potentially conflicting constraints. In this paper, we operationalize the notion of conflicting constraints and demonstrate how innovative automata-based techniques can be applied to monitor running process instances. Conflicting constraints are detected immediately and our toolset (realized using Declare and ProM) provides meaningful diagnostics.
Original languageEnglish
Title of host publicationRuntime Verification (Second International Conference, RV 2011, San Francisco CA, USA, September 27-30, 2011, Revised Selected Papers)
EditorsS. Kurshid, K. Sen
Place of PublicationBerlin
ISBN (Print)978-3-642-29859-2
Publication statusPublished - 2012

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


Dive into the research topics of 'Runtime verification of LTL-based declarative process models'. Together they form a unique fingerprint.

Cite this