Probabilistic Model Checking of Constraints in a Supply Chain Business Process

Tamara Mendt, Olga Tveretina, Carsten Sinz

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)


Business process models represent corporate activities, their dependencies and relations, as far as they are needed to reach a specific company goal. In practice, they often exhibit stochastic behavior, e.g., to deal with uncertain information. In this paper, we consider the problem of verifying properties over business processes that deal with such uncertain information. We employ a probabilistic model checking algorithm for verification, and demonstrate the applicability of this approach by a case study. Modeling and verification is achieved using the model checking tool PRISM. Based on the results, general specifications for modeling business processes using a probabilistic model checker are identified. Also, the difference between declarative and procedural business process modeling approaches is discussed. We propose to combine declarative and procedural techniques, thereby gaining increased expressiveness in modeling business processes, but still maintain verification feasible
Original languageEnglish
Title of host publicationBusiness Information Systems
Subtitle of host publication14th International Conference, BIS 2011
PublisherSpringer Nature
ISBN (Electronic)978-3-642-21863-7
ISBN (Print)978-3-642-21829-3
Publication statusPublished - 2011

Publication series

NameLecture Notes in Business Information Processing
PublisherSpringer Berlin Heidelberg
ISSN (Print)1865-1348


  • Supply chain, business processes compliance, probabilistic model checking, PRISM


Dive into the research topics of 'Probabilistic Model Checking of Constraints in a Supply Chain Business Process'. Together they form a unique fingerprint.

Cite this