Optimal Sceduling of Stochastic Production Processes Through Model Checking

  • L. Herbert
  • Z. N. L. Hansen
  • R. Sharp
  • P. Jacobsen
Conference paper


Modelling and subsequently optimising workflow processes has been a key part of efforts to improve efficiency in production and engineering firms since the beginning of the 20th century (Gilbreth & Gilbreth, 1921).


Business Process Model Check Reward Structure Discrete Time Markov Chain Bake Good 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. Van der Aalst, WMP, van Dongen, B. F, Herbst, J., Maruster, L., Schimm, G. & Weijters, A. (2003), Workflow mining: a survey of issues and approaches, Data & knowledge engineering 47 (2), 237-267Google Scholar
  2. Aziz, A. Singhal, V. Balarin, F. Brayton, R. Sangiovanni-Vincentelli, A. (1995) It usually works: The temporal logic of stochastic systems. In P. Wolper, (ed.), 7th International Conference on Computer Aided Verication (CAV’95), 939: 155-165. SpringerGoogle Scholar
  3. Ball, T., Jones, R. (2006). Eds., ser. Lecture Notes in Computer Science, London, UK: Springer-Verlag, 234-248Google Scholar
  4. Basu, A., Bensalem, S., Peled, D. & Sifakis, J. (2011). Priority scheduling of distributed systems based on model checking. Formal Methods in System Design 39(3): 229-245Google Scholar
  5. Baier, C., Katoen, J.-P. (2008). Principles of Model Checking. Cambridge MA, USA: The MIT PressGoogle Scholar
  6. Christensen, M.M., Haar, S. (2013) Supermarkeder presser brødkæmpe i minus. Børsen newspaper 8/08/2013. 151:12-13Google Scholar
  7. Christiansen, D. R., Carbone, M. & Hildebrandt, T. (2011), Formal semantics and implementation of BPMN 2.0 inclusive gateways, in Proc. of the 7th international conference on Web services and formal methods, ser. Web Services and Formal Methods 2010, Berlin, Heidelberg: Springer-Verlag, 146-160Google Scholar
  8. Gilbert, C, Bower, J. L. (2002) Disruptive change. When trying harder is part of the problem. Harv Bus Rev. 80(5):94-101Google Scholar
  9. Gilbreth, F. B, Gilbreth, L. M. (1921) Process Charts: First steps in finding the one best way to do work. American Society of Mechanical Engineers (ASME)Google Scholar
  10. Gröÿer, M., Norman, G., Baier, C. Ciesinski, F., Kwiatkowska, M. & Parker, D. (2006), On reduction criteria for probabilistic reward models, in Proceedings of the 26th international conference on Foundations of Software Technology and Theoretical Computer Science, ser. FSTTCS’06, Berlin, Heidelberg: Springer-Verlag, pp. 309-320Google Scholar
  11. Hansson, H., Jonsson, B. (1994), A logic for reasoning about time and reliability, Formal Aspects of Computing, 6(5): 512-535Google Scholar
  12. Herbert, L., Sharp, R. (2013a) Optimisation of BPMN business models via model checking. Proc. for ASME 2013 International Design Engineering Technical Conferences and computers and information in Engineering Conference (IDETC/CIE2013)Google Scholar
  13. Herbert, L., Sharp, R. (2013b) Precise analysis of probalistic business process model and notation workflows. Journal of Computing and Information Science in Engineering, 13: 2-11Google Scholar
  14. Herbert, L., Sharp, R. (2012a) Quantitative analysis of probabilistic (BPMN) workflows. Proc. for ASME 2012 International Design Engineering Technical Conferences and computers and information in Engineering Conference (IDETC/CIE2012)Google Scholar
  15. Herbert, L. & Sharp, R. (2012b), Using stochastic model checking to provision complex business services, in High-Assurance Systems Engineering (HASE), IEEE 14th International Symposium, 98-105Google Scholar
  16. Kotter, J. P. (1996) Leading Change. Harvard Business PressGoogle Scholar
  17. Kwiatkowska, M. Norman, G. and Parker, D. (2006). Symmetry reduction for probabilistic model checking, in Proc. 18th International Conference on Computer Aided Verification (CAV’06)Google Scholar
  18. Kwiatkowska, M., Norman, G. & Parker, D. (2011). PRISM 4.0: Verification of Probabilistic Real-time Systems. In Proc. 23rd International Conference on Computer Aided Verification (CAV’11), vol. 6806 of LNCS, 585-591, SpringerGoogle Scholar
  19. Kwiatkowska, M., Parker, D. (2012), Advances in probabilistic model checking’, in Software Safety and Security - Tools for Analysis and Verification, T. Nipkow, O. Grumberg and B. Hauptmann, Eds., ser. NATO Science for Peace and Security Series - D: Information and Communication Security, IOS Press, vol. 33: 126-151Google Scholar
  20. Muehlen, M., Recker, J. (2008). How Much Language Is Enough? Theoretical and Practical Use of the Business Process Modeling Notation. Proceedings for CAiSE ‘08 Proceedings of the 20th international conference on Advanced Information Systems Engineering, 465-479Google Scholar
  21. Object Management Group (2011) Business process model and notation (BPMN) 2.0. Standards Document formal/2011-01-03. Webpage:
  22. Parker, D. (2012). PRISM 4.0 manual, avaliable:
  23. Shingo, S. (1981) Study of Toyota Production System from Industrial Engineering Viewpoint. Japan Management AssociationGoogle Scholar
  24. Vergidis, K., Tiwari, A. & Majeed, B. (2008) Business process analysis and optimization: beyond reengineering., IEEE Transactions on Systems, Man, and Cybernetics, Part C, 38(1), 69–82.Google Scholar
  25. White, D. J. (1993), Markov decision processes. John Wiley & SonsGoogle Scholar
  26. Wijs, A. J., Pol, J. C. van de & Bortnik, E. M. (2009). Solving scheduling problems by untimed model checking : the clinical chemical analyser case study. International Journal on Software Tools for Technology Transfer, 11(5), 375-392Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2015

Authors and Affiliations

  • L. Herbert
    • 1
  • Z. N. L. Hansen
    • 1
  • R. Sharp
    • 1
  • P. Jacobsen
    • 1
  1. 1.Technical University of DenmarkLyngbyDenmark

Personalised recommendations