Bounded Model Checking for the Existential Part of Real-Time CTL and Knowledge

  • Bożena Woźna-Szcześniak
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7054)


A considerably large class of multi-agent systems operate in distributed and real-time environments, and often their correctness specifications require us to express time-critical properties that depend on performed actions of the system. In the paper, we focus on the formal verification of such systems by means of the bounded model checking (BMC) method, where specifications are expressed in the existential fragment of the Real-Time Computation Tree Logic augmented to include standard epistemic operators.


Model Check Global State Propositional Variable Propositional Formula Epistemic Modality 
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.


  1. 1.
    Benedetti, M., Cimatti, A.: Bounded Model Checking for Past LTL. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 18–33. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  2. 2.
    Biere, A., Cimatti, A., Clarke, E., Strichman, O., Zhu, U.: Bounded Model Checking. In: Highly Dependable Software. Advances in Computers, vol. 58. Academic Press (2003)Google Scholar
  3. 3.
    Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge Tracts in Theoretical Computer Science, vol. 53. Cambridge University Press (2001)Google Scholar
  4. 4.
    Bryant, R.: Binary Decision Diagrams and Beyond: Enabling Technologies for Formal Verification. In: Proc. of the ICCAD 1995, pp. 236–243 (1995)Google Scholar
  5. 5.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)Google Scholar
  6. 6.
    Copty, F., Fix, L., Fraer, R., Giunchiglia, E., Kamhi, G., Tacchella, A., Vardi, M.Y.: Benefits of Bounded Model Checking at an Industrial Setting. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 436–453. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  7. 7.
    Emerson, E.A., Mok, A.K., Sistla, A.P., Srinivasan, J.: Quantitative Temporal Reasoning. Real-Time Systems 4(4), 331–352 (1992)CrossRefzbMATHGoogle Scholar
  8. 8.
    Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. MIT Press, Cambridge (1995)zbMATHGoogle Scholar
  9. 9.
    Fagin, R., Halpern, J.Y., Vardi, M.Y.: What Can Machines Know? On the Properties of Knowledge in Distributed Systems. Journal of the ACM 39(2), 328–376 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    van der Hoek, W., Wooldridge, M.: Cooperation, Knowledge, and Time: Alternating-time Temporal Epistemic Logic and its Applications. Studia Logica 75(1), 125–157 (2003)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Penczek, W., Lomuscio, A.: Verifying Epistemic Properties of Multi-agent Systems via Bounded Model Checking. Fundamenta Informaticae 55(2), 167–185 (2003)MathSciNetzbMATHGoogle Scholar
  12. 12.
    Penczek, W., Woźna, B., Zbrzezny, A.: Bounded Model Checking for the Universal Fragment of CTL. Fundamenta Informaticae 51(1-2), 135–156 (2002)MathSciNetzbMATHGoogle Scholar
  13. 13.
    Raimondi, F., Lomuscio, A.: Automatic Verification of Multi-agent Systems by Model Checking via OBDDs. Journal of Applied Logic (2005)Google Scholar
  14. 14.
    Sorea, M.: Bounded Model Checking for Timed Automata. In: Proc. of the MTCS 2002. ENTCS, vol. 68, Elsevier Science Publishers (2002)Google Scholar
  15. 15.
    van der Meyden, R., Su, K.: Symbolic Model Checking the Knowledge of the Dining Cryptographers. In: Proc. of the CSFW 2004, pp. 280–291. IEEE Computer Society (2004)Google Scholar
  16. 16.
    Woźna, B.: Bounded Model Checking for the Universal Fragment of CTL*. Fundamenta Informaticae 63(1), 65–87 (2004)MathSciNetzbMATHGoogle Scholar
  17. 17.
    Woźna, B., Lomuscio, A., Penczek, W.: Bounded Model Checking for Knowledge over Real Time. In: Proc. of the AAMAS 2005, vol. I, pp. 165–172. ACM Press (2005)Google Scholar

Copyright information

© IFIP International Federation for Information Processing 2012

Authors and Affiliations

  • Bożena Woźna-Szcześniak
    • 1
  1. 1.IMCSJan Długosz UniversityCzȩstochowaPoland

Personalised recommendations