Advertisement

Taking Some Burden Off an Explicit CTL Model Checker

  • Torsten Liebke
  • Karsten WolfEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11522)

Abstract

In the CTL category of recent model checking contests, less problems have been solved than in the Reachability and LTL categories. Hence, improving CTL model checking technology deserves particular attention. We propose to relieve a generic explicit CTL model checker. This is done by designing specialised routines that cover a large set of simple (and frequently occurring) formula types. The CTL model checker is then only applied to formulas that do not fall into any special case. For the simple queries, we may apply simple depth-first search instead of recursive search, we may use much more powerful dialects of the stubborn set reduction, and we may add additional tools for verification, such as the state equation. Our approach covers about half of the CTL category of a recent model checking contest and significantly increases the power of CTL model checking.

Keywords

CTL model checking Partial order reduction 

References

  1. 1.
    Bønneland, F., Dyhr, J., Jensen, P.G., Johannsen, M., Srba, J.: Simplification of CTL formulae for efficient model checking of petri nets. In: Khomenko, V., Roux, O.H. (eds.) PETRI NETS 2018. LNCS, vol. 10877, pp. 143–163. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-91268-4_8CrossRefGoogle Scholar
  2. 2.
    Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982).  https://doi.org/10.1007/BFb0025774CrossRefGoogle Scholar
  3. 3.
    Clarke, E.M., Draghicescu, I.A.: Expressibility results for linear-time and branching-time logics. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1988. LNCS, vol. 354, pp. 428–437. Springer, Heidelberg (1989).  https://doi.org/10.1007/BFb0013029CrossRefGoogle Scholar
  4. 4.
    Commoner, F.: Deadlocks in Petri Nets. Applied Data Research Inc., Wakefield, Massachusetts, Report CA-7206-2311 (1972)Google Scholar
  5. 5.
    Courcoubetis, C., Vardi, M.Y., Wolper, P., Yannakakis, M.: Memory-efficient algorithms for the verification of temporal properties. Formal Methods Syst. Des. 1(2/3), 275–288 (1992)CrossRefGoogle Scholar
  6. 6.
    Couvreur, J.-M., Duret-Lutz, A., Poitrenaud, D.: On-the-fly emptiness checks for generalized Büchi automata. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, pp. 169–184. Springer, Heidelberg (2005).  https://doi.org/10.1007/11537328_15CrossRefGoogle Scholar
  7. 7.
    David, A., Jacobsen, L., Jacobsen, M., Jørgensen, K.Y., Møller, M.H., Srba, J.: TAPAAL 2.0: integrated development environment for timed-arc petri nets. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 492–497. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-28756-5_36CrossRefzbMATHGoogle Scholar
  8. 8.
    Dehnert, J., Rittgen, P.: Relaxed soundness of business processes. In: Dittrich, K.R., Geppert, A., Norrie, M.C. (eds.) CAiSE 2001. LNCS, vol. 2068, pp. 157–170. Springer, Heidelberg (2001).  https://doi.org/10.1007/3-540-45341-5_11CrossRefGoogle Scholar
  9. 9.
    Kordon, F., et al.: Homepage of the Model Checking Contest, June 2018. http://mcc.lip6.fr/
  10. 10.
    Geldenhuys, J., Valmari, A.: More efficient on-the-fly LTL verification with tarjan’s algorithm. Theor. Comput. Sci. 345(1), 60–82 (2005)MathSciNetCrossRefGoogle Scholar
  11. 11.
    Gerth, R., Kuiper, R., Peled, D.A., Penczek, W.: A partial order approach to branching time logic model checking. Inf. Comput. 150(2), 132–152 (1999)MathSciNetCrossRefGoogle Scholar
  12. 12.
    Godefroid, P., Wolper, P.: A partial approach to model checking. Inf. Comput. 110(2), 305–326 (1994)MathSciNetCrossRefGoogle Scholar
  13. 13.
    Hack, M.H.T.: Analysis of Production Schemata by Petri Nets. Master’s thesis, MIT, Dept. Electrical Engineering, Cambridge (1972)Google Scholar
  14. 14.
    Holzmann, G.J., Peled, D.A., Yannakakis, M.: On nested depth first search. In: Proceedings 2nd SPIN Workshop, pp. 23–32 (1996)CrossRefGoogle Scholar
  15. 15.
    Kristensen, L.M., Schmidt, K., Valmari, A.: Question-guided stubborn set methods for state properties. Formal Methods Syst. Des. 29(3), 215–251 (2006)CrossRefGoogle Scholar
  16. 16.
    Maidl, M.: The common fragment of CTL and LTL. In: Proceedings of FOCS, pp. 643–652. IEEE Computer Society (2000)Google Scholar
  17. 17.
    Oanea, O., Wimmel, H., Wolf, K.: New algorithms for deciding the siphon-trap property. In: Lilius, J., Penczek, W. (eds.) PETRI NETS 2010. LNCS, vol. 6128, pp. 267–286. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-13675-7_16CrossRefGoogle Scholar
  18. 18.
    Peled, D.: All from one, one for all: on model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409–423. Springer, Heidelberg (1993).  https://doi.org/10.1007/3-540-56922-7_34CrossRefGoogle Scholar
  19. 19.
    Schmidt, K.: Stubborn sets for standard properties. In: Donatelli, S., Kleijn, J. (eds.) ICATPN 1999. LNCS, vol. 1639, pp. 46–65. Springer, Heidelberg (1999).  https://doi.org/10.1007/3-540-48745-X_4CrossRefGoogle Scholar
  20. 20.
    Schmidt, K.: Stubborn sets for model checking the EF/AG fragment of CTL. Fundam. Inform. 43(1–4), 331–341 (2000)MathSciNetzbMATHGoogle Scholar
  21. 21.
    Tarjan, R.E.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1(2), 146–160 (1972)MathSciNetCrossRefGoogle Scholar
  22. 22.
    Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) ICATPN 1989. LNCS, vol. 483, pp. 491–515. Springer, Heidelberg (1991).  https://doi.org/10.1007/3-540-53863-1_36CrossRefGoogle Scholar
  23. 23.
    Valmari, A.: The state explosion problem. In: Reisig, W., Rozenberg, G. (eds.) ACPN 1996. LNCS, vol. 1491, pp. 429–528. Springer, Heidelberg (1998).  https://doi.org/10.1007/3-540-65306-6_21CrossRefGoogle Scholar
  24. 24.
    Valmari, A.: Stubborn set methods for process algebras. In: Proceedings of DIMACS Workshop on Partial Order Methods in Verification, vol. 29, pp. 213–231 (1997)CrossRefGoogle Scholar
  25. 25.
    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).  https://doi.org/10.1007/978-3-662-55862-1_7CrossRefGoogle Scholar
  26. 26.
    Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol. 1043, pp. 238–266. Springer, Heidelberg (1996).  https://doi.org/10.1007/3-540-60915-6_6CrossRefGoogle Scholar
  27. 27.
    Vergauwen, B., Lewi, J.: A linear local model checking algorithm for CTL. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 447–461. Springer, Heidelberg (1993).  https://doi.org/10.1007/3-540-57208-2_31CrossRefGoogle Scholar
  28. 28.
    Wimmel, H., Wolf, K.: Applying CEGAR to the Petri net state equation. Logical Methods Comput. Sci. 8(3) (2012)Google Scholar
  29. 29.
    Wolf, K.: Petri net model checking with LoLA 2. In: Khomenko, V., Roux, O.H. (eds.) PETRI NETS 2018. LNCS, vol. 10877, pp. 351–362. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-91268-4_18CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Universität Rostock, Institut für InformatikRostockGermany

Personalised recommendations