Runtime Verification of LTL-Based Declarative Process Models
ZusammenfassungLinear 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 presentation, 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. Joint work with: Michael Westergaard, Marco Montali and Wil van der Aalst.
Zur PersonFabrizio Maria Maggi received his PhD degree in Computer Science in 2010, and is currently a Post-Doc researcher at the Architecture of Information Systems (AIS) research group - Department of Mathematics and Computer Science - Eindhoven University of Technology. His PhD dissertation was entitled "Process Modelling, Implementation and Improvement". He authored more than 20 articles on process mining, automated revision of business process models through learning, (declarative) business process modeling and business constraints/rules, monitoring of business constraints at runtime, service oriented architectures, service choreographies and service composition.