Abstract
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.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
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)
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)
Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge Tracts in Theoretical Computer Science, vol. 53. Cambridge University Press (2001)
Bryant, R.: Binary Decision Diagrams and Beyond: Enabling Technologies for Formal Verification. In: Proc. of the ICCAD 1995, pp. 236–243 (1995)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)
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)
Emerson, E.A., Mok, A.K., Sistla, A.P., Srinivasan, J.: Quantitative Temporal Reasoning. Real-Time Systems 4(4), 331–352 (1992)
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. MIT Press, Cambridge (1995)
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)
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)
Penczek, W., Lomuscio, A.: Verifying Epistemic Properties of Multi-agent Systems via Bounded Model Checking. Fundamenta Informaticae 55(2), 167–185 (2003)
Penczek, W., Woźna, B., Zbrzezny, A.: Bounded Model Checking for the Universal Fragment of CTL. Fundamenta Informaticae 51(1-2), 135–156 (2002)
Raimondi, F., Lomuscio, A.: Automatic Verification of Multi-agent Systems by Model Checking via OBDDs. Journal of Applied Logic (2005)
Sorea, M.: Bounded Model Checking for Timed Automata. In: Proc. of the MTCS 2002. ENTCS, vol. 68, Elsevier Science Publishers (2002)
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)
Woźna, B.: Bounded Model Checking for the Universal Fragment of CTL*. Fundamenta Informaticae 63(1), 65–87 (2004)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 IFIP International Federation for Information Processing
About this paper
Cite this paper
Woźna-Szcześniak, B. (2012). Bounded Model Checking for the Existential Part of Real-Time CTL and Knowledge. In: Szmuc, T., Szpyrka, M., Zendulka, J. (eds) Advances in Software Engineering Techniques. CEE-SET 2009. Lecture Notes in Computer Science, vol 7054. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28038-2_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-28038-2_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28037-5
Online ISBN: 978-3-642-28038-2
eBook Packages: Computer ScienceComputer Science (R0)