Advertisement

Producing Explanations for Rich Logics

  • Simon Busard
  • Charles Pecheur
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10951)

Abstract

One of the claimed advantages of model checking is its capability to provide a counter-example explaining why a property is violated by a given system. Nevertheless, branching logics such as Computation Tree Logic and its extensions have complex branching counter-examples, and standard model checkers such as NuSMV do not produce complete counter-examples—that is, counter-examples providing all information needed to understand the verification outcome—and are limited to single executions. Many branching logics can be translated into the µ-calculus. To solve this problem of producing complete and complex counter-examples for branching logics, we propose a µ-calculus-based framework with rich explanations. It integrates a µ-calculus model checker that produces complete explanations, and several functionalities to translate them back to the original logic. In addition to the framework itself, we describe its implementation in Python and illustrate its applicability with Alternating Temporal Logic.

References

  1. 1.
    Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672–713 (2002)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, Cambridge (2008)zbMATHGoogle Scholar
  3. 3.
    Buccafurri, F., Eiter, T., Gottlob, G., Leone, N.: On ACTL formulas having linear counterexamples. J. Comput. Syst. Sci. 62(3), 463–515 (2001)MathSciNetCrossRefGoogle Scholar
  4. 4.
    Busard, S.: Symbolic model checking of multi-modal logics: uniform strategies and rich explanations. Ph.D. thesis, Université catholique de Louvain, July 2017Google Scholar
  5. 5.
    Busard, S., Pecheur, C.: Rich counter-examples for temporal-epistemic logic model checking. In: Proceedings Second International Workshop on Interactions, Games and Protocols, IWIGP 2012, Tallinn, Estonia, 25th March 2012, pp. 39–53 (2012). http://dx.doi.org/10.4204/EPTCS.78.4CrossRefGoogle Scholar
  6. 6.
    Busard, S., Pecheur, C.: PyNuSMV: NuSMV as a python library. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 453–458. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-38088-4_33CrossRefGoogle Scholar
  7. 7.
    Chechik, M., Gurfinkel, A.: A framework for counterexample generation and exploration. In: Cerioli, M. (ed.) FASE 2005. LNCS, vol. 3442, pp. 220–236. Springer, Heidelberg (2005).  https://doi.org/10.1007/978-3-540-31984-9_17CrossRefGoogle Scholar
  8. 8.
    Chechik, M., Gurfinkel, A.: A framework for counterexample generation and exploration. Int. J. Softw. Tools Technol. Transfer 9(5–6), 429–445 (2007)CrossRefGoogle Scholar
  9. 9.
    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).  https://doi.org/10.1007/3-540-45657-0_29CrossRefGoogle Scholar
  10. 10.
    Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  11. 11.
    Clarke, E.M., Jha, S., Lu, Y., Veith, H.: Tree-like counterexamples in model checking. In: Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS 2002), pp. 19–29 (2002)Google Scholar
  12. 12.
    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
  13. 13.
    Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244–263 (1986). http://doi.acm.org/10.1145/5397.5399CrossRefGoogle Scholar
  14. 14.
    Cranen, S., Luttik, B., Willemse, T.A.C.: Proof graphs for parameterised boolean equation systems. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013. LNCS, vol. 8052, pp. 470–484. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-40184-8_33CrossRefGoogle Scholar
  15. 15.
    Dong, Y., Ramakrishnan, C.R., Smolka, S.A.: Model checking and evidence exploration. In: Proceedings of the 10th IEEE International Conference on Engineering of Computer-Based Systems (ECBS 2003), pp. 214–223 (2003)Google Scholar
  16. 16.
    Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18(2), 194–211 (1979)MathSciNetCrossRefGoogle Scholar
  17. 17.
    Gammie, P., van der Meyden, R.: MCK: model checking the logic of knowledge. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 479–483. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-27813-9_41CrossRefGoogle Scholar
  18. 18.
    Gurfinkel, A., Chechik, M.: Proof-like counter-examples. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 160–175. Springer, Heidelberg (2003).  https://doi.org/10.1007/3-540-36577-X_12CrossRefGoogle Scholar
  19. 19.
    Jiang, C., Ciardo, G.: Generation of minimum tree-like witnesses for existential CTL. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 328–343. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-89960-2_18CrossRefGoogle Scholar
  20. 20.
    Kick, A.: Generation of witnesses for global \(\mu \)-calculus model checking. Technical report, Universität Karlsruhe, Germany (1995)Google Scholar
  21. 21.
    Kick, A.: Tableaux and witnesses for the \(\mu \)-calculus. Technical report, Universität Karlsruhe, Germany (1995)Google Scholar
  22. 22.
    Kozen, D.: Results on the propositional mu-calculus. Theor. Comput. Sci. 27, 333–354 (1983). http://dx.doi.org/10.1016/0304-3975(82)90125–6CrossRefGoogle Scholar
  23. 23.
    Linssen, C.A.: Diagnostics for Model Checking. Master’s thesis, Eindhoven University of Technology (2011)Google Scholar
  24. 24.
    Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: a model checker for the verification of multi-agent systems. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 682–688. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-02658-4_55CrossRefGoogle Scholar
  25. 25.
    Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: an open-source model checker for the verification of multi-agent systems. Int. J. Softw. Tools Technol. Transfer 1–22 (2015). http://dx.doi.org/10.1007/s10009-015-0378-x
  26. 26.
    Lomuscio, A., Raimondi, F.: mcmas: a model checker for multi-agent systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 450–454. Springer, Heidelberg (2006).  https://doi.org/10.1007/11691372_31CrossRefGoogle Scholar
  27. 27.
    Mateescu, R.: Efficient diagnostic generation for boolean equation systems. In: Graf, S., Schwartzbach, M. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 251–265. Springer, Heidelberg (2000).  https://doi.org/10.1007/3-540-46419-0_18CrossRefzbMATHGoogle Scholar
  28. 28.
    Penczek, W., Lomuscio, A.: Verifying epistemic properties of multi-agent systems via bounded model checking. In: Proceedings of the Second International Joint Conference on Autonomous Agents and Multiagent Systems. AAMAS 2003, pp. 209–216. ACM, New York (2003). http://doi.acm.org/10.1145/860575.860609
  29. 29.
    Rasse, A.: Error diagnosis in finite communicating systems. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 114–124. Springer, Heidelberg (1992).  https://doi.org/10.1007/3-540-55179-4_12CrossRefGoogle Scholar
  30. 30.
    Roychoudhury, A., Ramakrishnan, C., Ramakrishnan, I.: Justifying proofs using memo tables. In: International Conference on Principles and Practice of Declarative Programming: Proceedings of the 2nd ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, pp. 178–189 (2000)Google Scholar
  31. 31.
    Shoham, S., Grumberg, O.: A game-based framework for CTL counterexamples and 3-valued abstraction-refinement. ACM Trans. Comput. Logic (TOCL) 9(1), 1 (2007)MathSciNetCrossRefGoogle Scholar
  32. 32.
    Stirling, C.: Local model checking games (extended abstract). In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 1–11. Springer, Heidelberg (1995).  https://doi.org/10.1007/3-540-60218-6_1CrossRefGoogle Scholar
  33. 33.
    Tan, L., Cleaveland, R.: Evidence-based model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 455–470. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-45657-0_37CrossRefGoogle Scholar
  34. 34.
    Weitl, F., Nakajima, S., Freitag, B.: Structured counterexamples for the temporal description logic ALCCTL. In: 2010 8th IEEE International Conference on Software Engineering and Formal Methods, pp. 232–243. IEEE (2010)Google Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Université catholique de LouvainLouvain-la-NeuveBelgium

Personalised recommendations