Verifying CTL with Unfoldings of Petri Nets

  • Lanlan Dong
  • Guanjun LiuEmail author
  • Dongming Xiang
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11337)


There are many studies on verifying Computation Tree Logic (CTL) based on reachable graphs of Petri nets. However, they often suffer from the state explosion problem. In order to avoid/alleviate this problem, we use the unfolding technique of Petri nets to verify CTL. For highly concurrent systems, this technique implicitly represents all reachable states and greatly saves storage space. We construct verification algorithms and develop a related tool. Experiments show the advantages of our method.


Computation Tree Logic Model checking Petri nets Unfolding 



Authors would like to thank reviewers for their helpful comments. This paper is partially supported by the National Natural Science Foundation of China under grant no. 61572360.


  1. 1.
    Dai, Y.Y., Brayton, R.K.: Verification and synthesis of clock-gated circuits. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. PP(99), 1 (2017)Google Scholar
  2. 2.
    Griggio, A., Roveri, M.: Comparing different variants of the IC3 algorithm for hardware model checking. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 35(6), 1026–1039 (2016)CrossRefGoogle Scholar
  3. 3.
    Gnesi S, Margaria T.: Practical applications of probabilistic model checking to communication protocols, pp. 133–150. Wiley-IEEE Press (2013)Google Scholar
  4. 4.
    Wang, H., Zhao, T., Ren, F., et al.: Integrated modular avionics system safety analysis based on model checking. In: Reliability and Maintainability Symposium, pp. 1–6. IEEE (2017)Google Scholar
  5. 5.
    Hegde, M.S., Jnanamurthy, H.K., Singh, S.: Modelling and verification of extensible authentication protocol using spin model checker. Int. J. Netw. Secur. Its Appl. 4(6), 81–98 (2012)Google Scholar
  6. 6.
    Petri, C.A.: Kommunikation mit Automaten. Ph.D. Thesis, Institut Fuer Instrumentelle Mathematik (1962)Google Scholar
  7. 7.
    Clarke, E.M., Grumberg, O., Hiraishi, H., et al.: Verification of the Futurebus+ cache coherence protocol. Form. Methods Syst. Des. 6, 217–232 (1995)CrossRefGoogle Scholar
  8. 8.
    Bryant, R.E., Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. 35(8), 677–691 (1986)CrossRefGoogle Scholar
  9. 9.
    Burch, J.R., et al.: Symbolic model checking: 10 20, states and beyond. Inf. Comput. 98(2), 142–170 (1992)MathSciNetCrossRefGoogle Scholar
  10. 10.
    Burch, J.R., Clarke, E.M., Long, D.E.: Symbolic model checking with partitioned transition relations. Computer Science Department, pp. 49–58 (1991)Google Scholar
  11. 11.
    Valmari, A., Hansen, H.: Stubborn set intuition explained. In: Koutny, M., Kleijn, J., Penczek, W. (eds.) Transactions on Petri Nets and Other Models of Concurrency XII. LNCS, vol. 10470, pp. 140–165. Springer, Heidelberg (2017). Scholar
  12. 12.
    Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. ACM SIGPLAN Not. 40(1), 110–121 (2005)CrossRefGoogle Scholar
  13. 13.
    Boucheneb, H., Barkaoui, K.: Delay-dependent partial order reduction technique for real time systems. Real-Time Syst. 54(2), 278–306 (2018)CrossRefGoogle Scholar
  14. 14.
    Si, Y., Sun, J., Liu, Y., Wang, T.: Improving model checking stateful timed CSP with non-zenoness through clock-symmetry reduction. In: Groves, L., Sun, J. (eds.) ICFEM 2013. LNCS, vol. 8144, pp. 182–198. Springer, Heidelberg (2013). Scholar
  15. 15.
    Podelski, A., Rybalchenko, A.: ARMC: the logical choice for software model checking with abstraction refinement. In: Hanus, M. (ed.) PADL 2007. LNCS, vol. 4354, pp. 245–259. Springer, Heidelberg (2006). Scholar
  16. 16.
    Nouri, A., Raman, B., Bozga, M., Legay, A., Bensalem, S.: Faster statistical model checking by means of abstraction and learning. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 340–355. Springer, Cham (2014). Scholar
  17. 17.
    Liu, G., Reisig, W., Jiang, C., et al.: A branching-process-based method to check soundness of workflow systems. IEEE Access 4, 4104–4118 (2016)CrossRefGoogle Scholar
  18. 18.
    Liu, G., Zhang, K., Jiang, C.: Deciding the deadlock and livelock in a petri net with a target marking based on its basic unfolding. In: Carretero, J., Garcia-Blas, J., Ko, R.K.L., Mueller, P., Nakano, K. (eds.) ICA3PP 2016. LNCS, vol. 10048, pp. 98–105. Springer, Cham (2016). Scholar
  19. 19.
    Xiang, D., Liu, G., Yan, C., et al.: Detecting data inconsistency based on the unfolding technique of petri nets. IEEE Trans. Ind. Inform. 13, 2995–3005 (2017)CrossRefGoogle Scholar
  20. 20.
    Esparza, J., Heljanko, K.: Implementing LTL model checking with net unfoldings. In: Dwyer, M. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 37–56. Springer, Heidelberg (2001). Scholar
  21. 21.
    Katoen, J.-P.: Principles of Model Checking. The MIT Press, Cambridge (2008)Google Scholar
  22. 22.
    Esparza, J., Vogler, W.: An improvement of McMillan’s unfolding algorithm. LNCS 1099(3), 285–310 (2002)zbMATHGoogle Scholar
  23. 23.
    Himmel, A.S., Molter, H., Niedermeier, R., et al.: Adapting the BronCKerbosch algorithm for enumerating maximal cliques in temporal graphs. Soc. Netw. Anal. Min. 7(1), 35 (2017)Google Scholar
  24. 24.
    Bonnet-Torrés, O., Domenech, P., Lesire, C., Tessier, C.: Exhost-PIPE: PIPE extended for two classes of monitoring petri nets. In: Donatelli, S., Thiagarajan, P.S. (eds.) ICATPN 2006. LNCS, vol. 4024, pp. 391–400. Springer, Heidelberg (2006). Scholar
  25. 25.
    Roch, S., Starke, P.H.: INA: Integrated Net Analyzer (2002).

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Department of Computer ScienceTongji UniversityShanghaiChina

Personalised recommendations