Model checking Business Processes with Multi-Agent Systems

VCLA will be hosting a talk by Andreas Griesmayer from the Imperial College London on October 22nd, 2012.

ABSTRACT

Business artifacts allow to manage operations of business processes by capturing the key concepts and relevant information to guide their work flow. The Guard-Stage-Milestone (GSM) meta-model is a novel formalism for designing business artifacts that features declarative description of the intended behaviour without requiring an explicit specification of the control flow. Its concept of hierarchical structures of stages and explicit rules for the fulfilment of their guards and milestones supports the designing process but poses a challenge for formal verification. I will give an overview of the language and show how to develop a symbolic representation amenable to model checking.

In a second step, I will show how to verify interactions with the model by extension to a multi-agent systems. The properties checked are written in CTL-K, an extension of CTL by epistemic operators that allow to reason about the "knowledge" of agents. I will give a quick introduction to epistemic logic, applications of artifact systems and show how to compute the satisfying states for CTL-K.