Skip to Main content Skip to Navigation
Journal articles

Beyond Soundness: On the Verification of Semantic Business Process Models

Ingo Weber 1 Joerg Hoffmann 2 Jan Mendling 3 
2 MAIA - Autonomous intelligent machine
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : The verification of control-flow soundness is well understood as an important step before deploying business process models. However, the control flow does not capture what the process activities actually do when they are executed. Semantic annotations offer the opportunity to take this into account. Inspired by semantic Web service approaches such as OWL-S and WSMO, we consider process models in which the individual activities are annotated with logical preconditions and effects, specified relative to an ontology that axiomatizes the underlying business domain. Verification then addresses the overall process behavior, arising from the interaction between control-flow and behavior of individual activities. To this end, we combine notions from the workflow community with notions from the AI actions and change literature. We introduce a formal execution semantics for annotated business processes. We point out four verification tasks that arise, concerning precondition/effect conflicts, reachability, and executability. We examine the borderline between classes of processes that can, or cannot, be verified in polynomial time. For precondition/effect conflicts, we show that the borderline is the same as that of the logic underlying the ontology axioms. For reachability and executability, we identify a class of processes that can be verified in polynomial time by a fixpoint algorithm which we design for that purpose. We show that this class of processes is maximal in the sense that, when generalizing it in any of the most relevant directions, the validation tasks become computationally hard.
Document type :
Journal articles
Complete list of metadata
Contributor : Joerg Hoffmann Connect in order to contact the contributor
Submitted on : Wednesday, November 10, 2010 - 9:30:06 AM
Last modification on : Saturday, June 25, 2022 - 7:41:27 PM
Long-term archiving on: : Friday, February 11, 2011 - 2:27:30 AM


Files produced by the author(s)




Ingo Weber, Joerg Hoffmann, Jan Mendling. Beyond Soundness: On the Verification of Semantic Business Process Models. Distributed and Parallel Databases, Springer, 2010, 27 (3), pp.271-343. ⟨10.1007/s10619-010-7060-9⟩. ⟨inria-00491102⟩



Record views


Files downloads