(Stochastic) Model Checking in GreatSPN

  • Elvio Gilberto Amparore
  • Marco Beccuti
  • Susanna Donatelli
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8489)


GreatSPN is a tool for the definition and solution of Generalized Stochastic Petri Nets (GSPN). This paper presents the model checking features that have been recently introduced in GreatSPN. Through a new (Java-based) graphical interface for the GSPN model definition, the user can now access model checking of three different logics: the classical branching temporal logic CTL, and two stochastic logics, CSL and its superset CSLTA. This allows to integrate easily classical and probabilistic verification. A distinctive feature of the CTL model checker is the ability of generating counterexamples and witnesses. The CTL model checker employs symbolic data structures (decision diagrams) implemented in the Meddly library [6], developed Iowa State University, while the CSLTA model checker uses advanced solution methods, recently published, for Markov Renewal Processes.


Model Check Graphical User Interface Reachable State Large State Space Markov Renewal Process 
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. 1.
    Amparore, E.G., Donatelli, S.: A Component-Based Solution Method for Non-ergodic Markov Regenerative Processes. In: Aldini, A., Bernardo, M., Bononi, L., Cortellessa, V. (eds.) EPEW 2010. LNCS, vol. 6342, pp. 236–251. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  2. 2.
    Amparore, E.G., Donatelli, S.: Improving and assessing the efficiency of the MC4CSLTA model checker. In: Balsamo, M.S., Knottenbelt, W.J., Marin, A. (eds.) EPEW 2013. LNCS, vol. 8168, pp. 206–220. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  3. 3.
    Amparore, E.G., Donatelli, S.: A component-based solution for reducible Markov regenerative processes. Performance Evaluation 70(6), 400–422 (2013)CrossRefGoogle Scholar
  4. 4.
    Baarir, S., Beccuti, M., Cerotti, D., De Pierro, M., Donatelli, S., Franceschinis, G.: The GreatSPN tool: recent enhancements. SIGMETRICS Perform. Eval. Rev. 36(4), 4–9 (2009)CrossRefGoogle Scholar
  5. 5.
    Babar, J., Beccuti, M., Donatelli, S., Miner, A.: GreatSPN Enhanced with Decision Diagram Data Structures. In: Lilius, J., Penczek, W. (eds.) PETRI NETS 2010. LNCS, vol. 6128, pp. 308–317. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  6. 6.
    Babar, J., Miner, A.: Meddly: Multi-terminal and edge-valued decision diagram library. In: International Conference on Quantitative Evaluation of Systems, pp. 195–196. IEEE Computer Society, Los Alamitos (2010)Google Scholar
  7. 7.
    Ballarini, P., Djafri, H., Duflot, M., Haddad, S., Pekergin, N.: COSMOS: a statistical model checker for the hybrid automata stochastic logic. In: QEST 2011, pp. 143–144. IEEE Computer Society Press, Aachen (2011)Google Scholar
  8. 8.
    Chiola, G., Dutheillet, C., Franceschinis, G., Haddad, S.: Stochastic well-formed coloured nets for symmetric modelling applications. IEEE Trans. on Comp. 42(11), 1343–1360 (1993)CrossRefGoogle Scholar
  9. 9.
    Ciardo, G., Jones III, R.L., Miner, A.S., Siminiceanu, R.I.: Logic and stochastic modeling with SMART. Perform. Eval. 63(6), 578–608 (2006)CrossRefGoogle Scholar
  10. 10.
    Ciardo, G., Lüttgen, G., Siminiceanu, R.: Saturation: An efficient iteration strategy for symbolic state-space generation. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 328–342. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  11. 11.
    Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  12. 12.
    Clarke, E., Jha, S., Lu, Y., Veith, H.: Tree-like counterexamples in model checking. In: Proceedings of the 17th IEEE Symposium on Logic in Computer Science, pp. 19–29 (2002)Google Scholar
  13. 13.
    Emerson, E., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Science of Computer Programming 2(3), 241–266 (1982)CrossRefGoogle Scholar
  14. 14.
    Gaeta, R.: Efficient Discrete-Event Simulation of Colored Petri Nets. IEEE Trans. Softw. Eng. 22(9), 629–639 (1996)CrossRefGoogle Scholar
  15. 15.
    Katoen, J.P., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker MRMC. Performance Evaluation 68(2), 90–104 (2011)CrossRefGoogle Scholar
  16. 16.
    Marsan, M.A., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G.: Modeling with Generalized Stochastic Petri Nets. J. Wiley, New York (1995)zbMATHGoogle Scholar
  17. 17.
    Schwarick, M., Heiner, M., Rohr, C.: MARCIE - Model Checking and Reachability Analysis Done EffiCIEntly. In: Proceedings of QEST 2011, pp. 91–100 (2011)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Elvio Gilberto Amparore
    • 1
  • Marco Beccuti
    • 1
  • Susanna Donatelli
    • 1
  1. 1.Dipartimento di InformaticaUniversità di TorinoItaly

Personalised recommendations