Implementation of Epistemic Operators for Model Checking Multi-agent Systems

  • Marina Bagić Babac
  • Marijan Kunštić
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5796)


The problem of multi-agent system (MAS) specification and verification has been introduced in this paper, Epistemic transition system (ETS) represents an agent as the smallest unit in a multi-agent system, while Epistemic synchronous product (ESP) represents the formal model for a multi-agent system. Therefore, a formal framework for epistemic properties of multi-agent systems has been provided. A special extension of Action computation tree logic with unless operator for epistemic reasoning (ACTLW-ER) is used for MAS model checking. Epistemic operators of ACTLW-ER are implemented by symbolic model checking algorithms using binary decision diagrams.


Action Computation Tree Logic with Unless Operator Epistemic Reasoning Multi-agent Systems 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Bagić, M., Kunštić, M.: Verification of Intelligent Agents with ACTL for Epistemic Reasoning. In: Proceedings of International Conference on Intelligent Agents, Web Technologies and Internet Commerce - IAWTIC 2006, p. 76. IEEE, Los Alamitos (2006)Google Scholar
  2. 2.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2001)CrossRefGoogle Scholar
  3. 3.
    Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. The MIT Press, Cambridge (2003)zbMATHGoogle Scholar
  4. 4.
    Fantecji, A.: Enhancing test coverage by back-tracing model-checker counterexamples. Electronic Notes in Computer Science, vol. 116, pp. 199–211 (2005)Google Scholar
  5. 5.
    Huth, M.R.A., Ryan, M.D.: Logic in Computer Science: Modelling and reasoning about systems. Cambridge University Press, Cambridge (2000)zbMATHGoogle Scholar
  6. 6.
    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, Anaheim, Calgary, Zuerich, pp. 663–669. IASTED/ACTA Press, Innsbruck (2000)Google Scholar
  7. 7.
    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, Thessaloniki, Greece, pp. 100–114 (2003)Google Scholar
  8. 8.
    Milner, R.: Communication and Concurrency, Prentice Hall International Series, Computer Science, UK (1989)Google Scholar
  9. 9.
    Pecheur, C., Raimondi, F.: Symbolic model checking of logics with actions. In: Edelkamp, S., Lomuscio, A. (eds.) MoChArt IV. LNCS (LNAI), vol. 4428, pp. 113–128. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  10. 10.
    Raimondi, F., Lomuscio, A.: Automatic verification of deontic and epistemic properties of multi-agent systems by model checking via OBDD’s. In: Proceedings of ECAI 2004, pp. 53–57. IOS Press, Amsterdam (2004)Google Scholar
  11. 11.
    University of Maribor, Laboratory of Microcomputer Systems (2009),

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Marina Bagić Babac
    • 1
  • Marijan Kunštić
    • 1
  1. 1.Faculty of Electrical Engineering and ComputingUniversity of ZagrebZagrebCroatia

Personalised recommendations