Bounded Model Checking Real-Time Multi-agent Systems with Clock Differences: Theory and Implementation

  • Alessio Lomuscio
  • Bożena Woźna
  • Andrzej Zbrzezny
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4428)


We present a methodology for verifying epistemic and real-time temporal properties of multi-agent systems. We introduce an interpreted systems semantics based on diagonal timed automata and use a real-time temporal epistemic language to describe properties of multi-agent systems. We develop a bounded model checking algorithm for this setting and present experimental results for a real-time version of the alternating bit-transmission problem obtained by means of a preliminary implementation of the technique.


Model Check Multiagent System Epistemic Logic Boolean Formula Propositional Formula 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Asarin, E., Bozga, M., Kerbrat, A., Maler, O., Pnueli, A., Rasse, A.: Data-structures for the verification of Timed Automata. In: Maler, O. (ed.) HART 1997. LNCS, vol. 1201, pp. 346–360. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  2. 2.
    Behrmann, G., Larsen, K., Pearson, J., Weise, C., Yi, W.: Efficient Timed Reachability Analysis Using Clock Difference Diagrams. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 341–353. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  3. 3.
    Bérard, B., Petit, A., Diekert, V., Gastin, P.: Characterization of the expressive power of silent transitions in timed automata. Fundamenta Informaticae 36(2-3), 145–182 (1998)zbMATHMathSciNetGoogle Scholar
  4. 4.
    Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) ETAPS 1999 and TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  5. 5.
    Bouyer, P., Laroussinie, F., Reynier, P.: Diagonal constraints in timed automata: Forward analysis of timed systems. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 112–126. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  6. 6.
    Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV2: An open-source tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  7. 7.
    Dembiński, P., Janowska, A., Janowski, P., Penczek, W., Pólrola, A., Szreter, M., Woźna, B., Zbrzezny, A.: VerICS: A tool for verifying Timed Automata and Estelle specifications. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol. 2619, pp. 278–283. Springer, Heidelberg (2003)Google Scholar
  8. 8.
    Dill, D.: Timing assumptions and verification of finite state concurrent systems. In: Sifakis, J. (ed.) Automatic Verification Methods for Finite State Systems. LNCS, vol. 407, pp. 197–212. Springer, Heidelberg (1990)Google Scholar
  9. 9.
  10. 10.
    Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. MIT Press, Cambridge (1995)zbMATHGoogle Scholar
  11. 11.
    Kacprzak, M., Lomuscio, A., Penczek, W.: Verification of multiagent systems via unbounded model checking. In: Jennings, N.R., Sierra, C., Sonenberg, L., Tambe, M. (eds.) Proceedings of the Third International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2004), vol. II, pp. 638–645. ACM, New York (2004)Google Scholar
  12. 12.
    Lomuscio, A., Raimondi, F.: MCMAS: A model checker for multi-agent systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol. 3920, pp. 450–454. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  13. 13.
    Lomuscio, A., Sergot, M.: A formalisation of violation, error recovery, and enforcement in the bit transmission problem. Journal of Applied Logic 2(1), 93–116 (2004)zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    Lomuscio, A., Woźna, B., Zbrzezny, A.: Bounded model checking real-time multi-agent systems with clock differences: theory and implementation. Technical Report RN/06/03, Department of Computer Science, University College London, Gower Street, London WC1E 6BT, United Kingdom (2006)Google Scholar
  15. 15.
    Nabialek, W., Niewiadomski, A., Penczek, W., Pólrola, A., Szreter, M.: VerICS 2004: A model checker for real time and multi-agent systems. In: Proceedings of the International Workshop on Concurrency, Specification and Programming (CS&P 2004), Informatik-Berichte,Humboldt University, vol. 170, pp. 88–99 (2004)Google Scholar
  16. 16.
    Penczek, W., Lomuscio, A.: Verifying epistemic properties of multi-agent systems via bounded model checking. Fundamenta Informaticae 55(2), 167–185 (2003)zbMATHMathSciNetGoogle Scholar
  17. 17.
    Penczek, W., Woźna, B., Zbrzezny, A.: Towards bounded model checking for the universal fragment of TCTL. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 265–288. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  18. 18.
    Raimondi, F., Lomuscio, A.: Automatic verification of multi-agent systems by model checking via OBDDs. Journal of Applied Logic, 2007. Special issue on Logic-based agent verification (to appear, 2007)Google Scholar
  19. 19.
    Tripakis, S., Yovine, S.: Analysis of timed systems using time-abstracting bisimulations. Formal Methods in System Design 18(1), 25–68 (2001)zbMATHCrossRefGoogle Scholar
  20. 20.
    van der Meyden, R., Su, K.: Symbolic model checking the knowledge of the dining cryptographers. In: Proceedings of the 17th IEEE Computer Security Foundations Workshop (CSFW 2004), pp. 280–291. IEEE Computer Society Press, Washington, DC, USA (2004)CrossRefGoogle Scholar
  21. 21.
    Woźna, B., Lomuscio, A., Penczek, W.: Bounded model checking for knowledge over real time. In: Proceedings of the 4st International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS 2005), July 2005, vol. 1, pp. 165–172. ACM Press, New York (2005)CrossRefGoogle Scholar
  22. 22.
    Zbrzezny, A.: SAT-based reachability checking for timed automata with diagonal constraints. Fundamenta Informaticae 67(1-3), 303–322 (2005)zbMATHMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Alessio Lomuscio
    • 1
  • Bożena Woźna
    • 2
  • Andrzej Zbrzezny
    • 2
  1. 1.Department of Computing, Imperial College London, London SW72BZUK
  2. 2.IMCS, Jan Długosz University. Al. Armii Krajowej 13/15, 42-200 CzȩstochowaPoland

Personalised recommendations