{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,17]],"date-time":"2026-06-17T15:18:56Z","timestamp":1781709536791,"version":"3.54.5"},"reference-count":36,"publisher":"ASME International","issue":"1","content-domain":{"domain":["asmedigitalcollection.asme.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2013,3,1]]},"abstract":"<jats:p>We present a framework for modeling and analysis of real-world business workflows. We present a formalized core subset of the business process modeling and notation (BPMN) and then proceed to extend this language with probabilistic nondeterministic branching and general-purpose reward annotations. We present an algorithm for the translation of such models into Markov decision processes (MDP) expressed in the syntax of the PRISM model checker. This enables precise quantitative analysis of business processes for the following properties: transient and steady-state probabilities, the timing, occurrence and ordering of events, reward-based properties, and best- and worst- case scenarios. We develop a simple example of medical workflow and demonstrate the utility of this analysis in accurate provisioning of drug stocks. Finally, we suggest a path to building upon these techniques to cover the entire BPMN language, allow for more complex annotations and ultimately to automatically synthesize workflows by composing predefined subprocesses, in order to achieve a configuration that is optimal for parameters of interest.<\/jats:p>","DOI":"10.1115\/1.4023362","type":"journal-article","created":{"date-parts":[[2013,3,22]],"date-time":"2013-03-22T15:37:45Z","timestamp":1363966665000},"update-policy":"https:\/\/doi.org\/10.1115\/crossmarkpolicy-asme","source":"Crossref","is-referenced-by-count":14,"title":["Precise Quantitative Analysis of Probabilistic Business Process Model and Notation Workflows"],"prefix":"10.1115","volume":"13","author":[{"given":"Luke","family":"Herbert","sequence":"first","affiliation":[{"name":"Doctoral Candidate e-mail:"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Robin","family":"Sharp","sequence":"additional","affiliation":[{"name":"Associate Professor e-mail:\u2002 Informatics Department, Technical University of Denmark, 2300 Lyngby, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"33","published-online":{"date-parts":[[2013,3,15]]},"reference":[{"key":"2019100604093862000_B1","volume-title":"Enterprise Architecture as Strategy: Creating a Foundation for Business Execution","year":"2006"},{"key":"2019100604093862000_B2","article-title":"The Economic Impacts of Inadequate Infrastructure for Software Testing","year":"2002"},{"key":"2019100604093862000_B3","article-title":"Economic Impact of Inadequate Infrastructure for Supply Chain Integration","year":"2004"},{"issue":"1","key":"2019100604093862000_B4","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1109\/TSMCC.2007.905812","article-title":"Business Process Analysis and Optimization: Beyond Reengineering","volume":"38","year":"2008","journal-title":"IEEE Trans. Syst., Man Cybern., Part C Appl. Rev."},{"key":"2019100604093862000_B5","article-title":"Business Process Model and Notation (BPMN) 2.0","author":"Object Management Group","year":"2011"},{"key":"2019100604093862000_B6","article-title":"Xml Process Definition Language","author":"Workflow Management Coalition","year":"2008"},{"key":"2019100604093862000_B7","article-title":"Omg Unified Modeling Language (omg uml), Infrastructure","author":"Object Management Group","year":"2011"},{"key":"2019100604093862000_B8","doi-asserted-by":"crossref","first-page":"1024","DOI":"10.4018\/978-1-61520-670-4.ch049","article-title":"Healthcare Process Development With BPMN","volume-title":"Handbook of Research on Developments in E-Health and Telemedicine: Technological and Social Perspectives","year":"2010"},{"key":"2019100604093862000_B9","first-page":"1","article-title":"An Evaluation Framework for Business Process Modeling Languages in Healthcare","volume":"4","year":"2009","journal-title":"J. Theor. Appl. Electron. Commerce Res."},{"key":"2019100604093862000_B10","first-page":"123","article-title":"Automating the Dissemination of Information Entities to Healthcare Professionals","volume-title":"Advances in Information Technology","year":"2009"},{"key":"2019100604093862000_B11","doi-asserted-by":"crossref","unstructured":"Rojo, M. G., Rolon, E., Calahorra, L., Garcia, F. O., Sanchez, R. P., Ruiz, F., Ballester, N., Armenteros, M., Rodriguez, T., and Espartero, R. M., 2008, \u201cImplementation of the Business Process Modelling Notation (BPMN) in the Modelling of Anatomic Pathology Processes,\u201d Proceedings of the 9th European Congress on Telepathology and 3rd International Congress on Virtual Microscopy, Vol. 3 (Suppl 1), BioMed Central Ltd.","DOI":"10.1186\/1746-1596-3-S1-S22"},{"key":"2019100604093862000_B12","first-page":"587","article-title":"Could Automation Improve Efficieny and Help Pharmacies With Cost Saving?","volume":"285","year":"2010","journal-title":"Pharm. J."},{"key":"2019100604093862000_B13","first-page":"179","article-title":"Factors Predictive of Intravenous Fluid Administration Errors in Australian Surgical Care Wards","volume":"14","year":"2004","journal-title":"Qual. Saf. Health Care"},{"issue":"22","key":"2019100604093862000_B14","doi-asserted-by":"crossref","first-page":"2042","DOI":"10.2146\/ajhp080540","article-title":"Effect of Lean Process Improvement Techniques on a University Hospital Inpatient Pharmacy","volume":"66","year":"2009","journal-title":"Am. J. Health-Syst. Pharm."},{"issue":"9","key":"2019100604093862000_B15","first-page":"779","article-title":"Impact of Automation on Pharmacist Interventions and Medication Errors in a Correctional Health Care System","volume":"59","year":"2001","journal-title":"Am. J. Health-Syst. Pharm."},{"issue":"13","key":"2019100604093862000_B16","doi-asserted-by":"crossref","first-page":"1427","DOI":"10.2146\/ajhp060313","article-title":"Dispensing Error Rate After Implementation of an Automated Pharmacy Carousel System","volume":"64","year":"2007","journal-title":"Am. J. Health-Syst. Pharm."},{"issue":"5","key":"2019100604093862000_B17","first-page":"94","article-title":"Disruptive Change: When Trying Harder is Part of the Problem","volume":"80","year":"2002","journal-title":"Harvard Bus. Rev."},{"key":"2019100604093862000_B18","volume-title":"Principles of Model Checking, The","year":"2008"},{"key":"2019100604093862000_B19","doi-asserted-by":"crossref","unstructured":"Wong, P. Y., and Gibbons, J., 2008, \u201cA Process Semantics for BPMN,\u201d Proceedings of the 10th International Conference on Formal Methods and Software Engineering, International Conference on Formal Methods and Software Engineering 2008, Springer-Verlag, pp. 355\u2013374.","DOI":"10.1007\/978-3-540-88194-0_22"},{"issue":"1","key":"2019100604093862000_B20","doi-asserted-by":"crossref","first-page":"100","DOI":"10.1145\/357980.358021","article-title":"Communicating Sequential Processes","volume":"26","year":"1983","journal-title":"Commun. ACM"},{"key":"2019100604093862000_B21","doi-asserted-by":"crossref","unstructured":"Broadfoot, P. J., and Roscoe, A. W., 2000, \u201cTutorial on FDR and Its Applications,\u201d Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, Springer-Verlag, p. 322.","DOI":"10.1007\/10722468_18"},{"key":"2019100604093862000_B22","doi-asserted-by":"crossref","unstructured":"Ouyang, C., Dumas, M., ter Hofstede, A. H. M., and van der Aalst, W. M. P., 2006, \u201cFrom BPMN Process Models to BPEL Web Services,\u201d Proceedings of the IEEE International Conference on Web Services, IEEE Computer Society, pp. 285\u2013292.","DOI":"10.1109\/ICWS.2006.67"},{"key":"2019100604093862000_B23","doi-asserted-by":"crossref","first-page":"1281","DOI":"10.1016\/j.infsof.2008.02.006","article-title":"Semantics and Analysis of Business Process Models in BPMN","volume":"50","year":"2008","journal-title":"Inf. Softw. Technol."},{"key":"2019100604093862000_B24","doi-asserted-by":"crossref","unstructured":"Prandi, D., Quaglia, P., and Zannone, N., 2008, \u201cFormal Analysis of BPMN via a Translation Into COWS,\u201d Proceedings of the 10th international conference on Coordination models and languages, Coordination 2008, Springer-Verlag, pp. 249\u2013263.","DOI":"10.1007\/978-3-540-68265-3_16"},{"key":"2019100604093862000_B25","unstructured":"Kwiatkowska, M. Z., Norman, G., and Parker, D., 2011, \u201cPRISM 4.0: Verification of Probabilistic Real-Time Systems,\u201d Proceedings of 23rd International Conference on Computer Aided Verification (CAV\u201911), Vol. 6806 of Lecture Notes in Computer Science, Springer-Verlag, pp. 585\u2013591."},{"issue":"1","key":"2019100604093862000_B26","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1016\/j.csi.2011.06.002","article-title":"BPMN: An Introduction to the Standard","volume":"34","year":"2012","journal-title":"Comput. Stand. Interfaces"},{"key":"2019100604093862000_B27","unstructured":"Muehlen, M. Z., and Recker, J., 2008, \u201cHow Much Language is Enough? Theoretical and Practical Use of the Business Process Modeling Notation,\u201d Proceedings of the 20th international conference on Advanced Information Systems Engineering, Conference on Advanced Information Systems Engineering 2008, Springer-Verlag, pp. 465\u2013479."},{"key":"2019100604093862000_B28","first-page":"585","article-title":"Towards a BPMN Semantics Using UML Models","volume-title":"Business Process Management Workshops","year":"2009"},{"key":"2019100604093862000_B29","doi-asserted-by":"crossref","unstructured":"Ye, J., Sun, S., Song, W., and Wen, L., 2008, \u201cFormal Semantics of BPMN Process Models Using YAWL,\u201d Proceedings of the 2008 Second International Symposium on Intelligent Information Technology Application, Vol. 2, IEEE Computer Society, pp. 70\u201374.","DOI":"10.1109\/IITA.2008.68"},{"key":"2019100604093862000_B30","doi-asserted-by":"crossref","unstructured":"Christiansen, D. R., Carbone, M., and Hildebrandt, T., 2011, \u201cFormal Semantics and Implementation of BPMN 2.0 Inclusive Gateways,\u201d Proceedings of the 7th international conference on Web services and formal methods, Web Services and Formal Methods 2010, Springer-Verlag, pp. 146\u2013160.","DOI":"10.1007\/978-3-642-19589-1_10"},{"key":"2019100604093862000_B31","volume-title":"Markov Decision Processes","year":"1993"},{"key":"2019100604093862000_B32","first-page":"126","article-title":"Advances in Probabilistic Model Checking","volume-title":"Software Safety and Security\u2014Tools for Analysis and Verification","year":"2012"},{"issue":"5","key":"2019100604093862000_B33","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1007\/BF01211866","article-title":"A Logic for Reasoning About Time and Reliability","volume":"6","year":"1994","journal-title":"Formal Aspects Comput."},{"issue":"1","key":"2019100604093862000_B34","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1008739929481","article-title":"Reactive Modules","volume":"15","year":"1999","journal-title":"Formal Methods Syst. Des."},{"key":"2019100604093862000_B35","year":"2012"},{"key":"2019100604093862000_B36","first-page":"98","article-title":"Using Stochastic Model Checking to Provision Complex Business Services","year":"2012"}],"container-title":["Journal of Computing and Information Science in Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/asmedigitalcollection.asme.org\/computingengineering\/article-pdf\/doi\/10.1115\/1.4023362\/6098971\/jcis_13_1_011007.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"http:\/\/asmedigitalcollection.asme.org\/computingengineering\/article-pdf\/doi\/10.1115\/1.4023362\/6098971\/jcis_13_1_011007.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,6]],"date-time":"2019-10-06T04:09:55Z","timestamp":1570334995000},"score":1,"resource":{"primary":{"URL":"https:\/\/asmedigitalcollection.asme.org\/computingengineering\/article\/doi\/10.1115\/1.4023362\/371379\/Precise-Quantitative-Analysis-of-Probabilistic"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,3,1]]},"references-count":36,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,3,1]]}},"URL":"https:\/\/doi.org\/10.1115\/1.4023362","relation":{},"ISSN":["1530-9827","1944-7078"],"issn-type":[{"value":"1530-9827","type":"print"},{"value":"1944-7078","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,3,1]]},"article-number":"011007"}}