Precise Parameter Synthesis for Generalised Stochastic Petri Nets with Interval Parameters

  • Milan ČeškaJr.Email author
  • Milan Češka
  • Nicola Paoletti
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10672)


We consider the problem of synthesising parameters affecting transition rates and probabilities in generalised Stochastic Petri Nets (GSPNs). Given a time-bounded property expressed as a probabilisitic temporal logic formula, our method allows computing the parameters values for which the probability of satisfying the property meets a given bound, or is optimised. We develop algorithms based on reducing the parameter synthesis problem for GSPNs to the corresponding problem for continuous-time Markov Chains (CTMCs), for which we can leverage existing synthesis algorithms, while retaining the modelling capabilities and expressive power of GSPNs. We evaluate the usefulness of our approach by synthesising parameters for two case studies.


  1. 1.
    Al-Jaar, R.Y., Desrochers, A.A.: Performance evaluation of automated manufacturing systems using generalized stochastic petri nets. IEEE Trans. Robot. Autom. 6(6), 621–639 (1990)CrossRefGoogle Scholar
  2. 2.
    Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Verifying continuous time Markov chains. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 269–276. Springer, Heidelberg (1996). CrossRefGoogle Scholar
  3. 3.
    Baier, C., et al.: Model checking for performability. Math. Struct. Comput. Sci. 23(4), 751–795 (2013)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Balbo, G.: Introduction to generalized stochastic Petri nets. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol. 4486, pp. 83–131. Springer, Heidelberg (2007). CrossRefGoogle Scholar
  5. 5.
    Češka, M., et al.: Precise parameter synthesis for stochastic biochemical systems. Acta Informatica 54(6), 589–623 (2017)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Češka, M., Pilař, P., Paoletti, N., Brim, L., Kwiatkowska, M.: PRISM-PSY: precise GPU-accelerated parameter synthesis for stochastic systems. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 367–384. Springer, Heidelberg (2016). Google Scholar
  7. 7.
    Ghemawat, S., Gobioff, H., Leung, S.-T.: The Google file system. In: Proceedings of the SOSP 2003, pp. 29–43. ACM (2003)Google Scholar
  8. 8.
    Goss, P.J.E., Peccoud, J.: Quantitative modeling of stochastic systems in molecular biology by using stochastic petri nets. PNAS 95(12), 6750–6755 (1998)CrossRefGoogle Scholar
  9. 9.
    Heiner, M., Gilbert, D., Donaldson, R.: Petri nets for systems and synthetic biology. In: Bernardo, M., Degano, P., Zavattaro, G. (eds.) SFM 2008. LNCS, vol. 5016, pp. 215–264. Springer, Heidelberg (2008). CrossRefGoogle Scholar
  10. 10.
    Huang, C., Ferrell, J.: Ultrasensitivity in the mitogen-activated protein kinase cascade. Proc. Natl. Acad. Sci. 93, 10078–10083 (1996)CrossRefGoogle Scholar
  11. 11.
    Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol. 4486, pp. 220–270. Springer, Heidelberg (2007). CrossRefGoogle Scholar
  12. 12.
    Marsan, M.A., et al.: Modelling with Generalized Stochastic Petri Nets. Wiley, Hoboken (1994)Google Scholar

Copyright information

© Springer International Publishing AG 2018

Authors and Affiliations

  • Milan ČeškaJr.
    • 1
    Email author
  • Milan Češka
    • 1
  • Nicola Paoletti
    • 2
  1. 1.Faculty of Information TechnologyBrno University of TechnologyBrnoCzech Republic
  2. 2.Department of Computer ScienceStony Brook UniversityStony BrookUSA

Personalised recommendations