Advertisement

Symbolic Model Checking of Logics with Actions

  • Charles Pecheur
  • Franco Raimondi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4428)

Abstract

Reasoning about agents and modalities such as knowledge and belief leads to models where different relations over states co-exist, or equivalently, where information (labels, actions) is associated to state transitions. This paper discusses how to augment classical CTL symbolic model-checking to support logics with actions such as A-CTL (action-CTL), and how this can be implemented using BDDs in tools such as the SMV/NuSMV package. Considering general action-state structures, we first propose a natural extension of CTL to actions, called Action-Restricted CTL (ARCTL) and adapt classical results from CTL to express model checking based on three functions eax, eau and eag. On these grounds, we present two different implementations of symbolic model checking with actions. The first approach encodes action-state models and logics into pure state-based models and logics, that can be checked with existing model-checkers. The second approach consists in a native implementation of the three extended operators. We report on our prototype implementation of both approaches based on NuSMV and give an overview of how this is used to model-check the temporal epistemic logic CTLK.

Keywords

Model Check Label Transition System Kripke Structure Computation Tree Logic Symbolic Model Check 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: a new symbolic model verifier. In: Proc. of International Conference on Computer-Aided Verification (1999)Google Scholar
  2. 2.
    Penczek, W., Lomuscio, A.: Verifying epistemic properties of multi-agent systems via bounded model checking. Fundamenta Informaticae 55, 167–185 (2003)zbMATHMathSciNetGoogle Scholar
  3. 3.
    Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems 8, 244–263 (1986)zbMATHCrossRefGoogle Scholar
  4. 4.
    Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  5. 5.
    Nicola, R.D., Vaandrager, F.: Action versus state based logics for transition systems. In: Guessarian, I. (ed.) Semantics of Systems of Concurrent Processes. LNCS, vol. 469, pp. 407–419. Springer, Heidelberg (1990)Google Scholar
  6. 6.
    Mateescu, R.: Logiques temporelles basées sur actions pour la vérification des systèmes asynchrones. Rapport de recherche 5032, INRIA (2003)Google Scholar
  7. 7.
    Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, J.: Symbolic model checking: 1020 states and beyond. Information and Computation 98, 142–170 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: a new symbolic model verifier. In: Proc. of International Conference on Computer-Aided Verification (1999)Google Scholar
  9. 9.
    Kernighan, B., Ritchie, D.: The M4 Macro Processor. Bell Laboratories (1977)Google Scholar
  10. 10.
    Lomuscio, A., Pecheur, C., Raimondi, F.: Automatic verification of knowledge and time with NuSMV. In: Proceedings of IJCAI 2007, Hyderabad, India (to appear) (2007)Google Scholar
  11. 11.
    Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. MIT Press, Cambridge (1995)zbMATHGoogle Scholar
  12. 12.
    Raimondi, F., Pecheur, C., Lomuscio, A.: Applications of model checking for multi-agent systems: verification of diagnosability and recoverability. In: Proceedings of Concurrency, Specification & Programming (CS&P), Warsaw University, pp. 433–444 (2005)Google Scholar
  13. 13.
    Meolic, R., Kapus, T., Brezocnik, Z.: An action computation tree logic with unless operator. In: Proceedings of the 1st South-East European workshop on formal methods SEEFM 2003, pp. 100–114 (2003)Google Scholar
  14. 14.
    Meolic, R., Kapus, T., Brezocnik, Z.: Verification of concurrent systems using ACTL. In: Hamza, M.H., (ed.) Applied informatics: proceedings of the IASTED international conference AI 2000, IASTED/ACTA Press, pp. 663–669 (2000)Google Scholar
  15. 15.
    Meolic, R., Kapus, T., Brezocnik, Z.: The Efficient Symbolic Tools package. In: 8th International Conference Software, Telecommunications and Computer Networks (SoftCOM 2000), pp. 147–156 (2000)Google Scholar
  16. 16.
    Fantechi, A., Gnesi, S., Mazzanti, F., Pugliese, R., Tronci, E.: A symbolic model checker for ACTL. In: Hutter, D., Traverso, P. (eds.) Applied Formal Methods - FM-Trends 98. LNCS, vol. 1641, pp. 228–242. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  17. 17.
    Enders, R., Filkorn, T., Taubner, D.: Generating BDDs for symbolic model checking in CCS. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, Springer, Heidelberg (1992)Google Scholar
  18. 18.
    Dsouza, A., Bloom, B.: Generating BDD models for process algebra terms. In: Proceedings of the 7th International Conference on Computer Aided Verification, London, UK, pp. 16–30. Springer, Heidelberg (1995)Google Scholar
  19. 19.
    Brinksma, E., Rensink, A., Vogler, W.: Fair testing. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 313–327. Springer, Heidelberg (1995)Google Scholar
  20. 20.
    Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49, 672–713 (2002)CrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Charles Pecheur
    • 1
  • Franco Raimondi
    • 2
  1. 1.Université catholique de Louvain 
  2. 2.University College London 

Personalised recommendations