Bounded model checking for knowledge and real time

We present TECTLK, a logic to specify knowledge and real time in multi-agent systems. We show that the model checking problem is decidable, and we present an algorithm for TECTLK bounded model checking based on a discretisation method. We exemplify the use of the technique by means of the ”Railroad Crossing System”, a popular example in the multi-agent systems literature. Categories and Subject Descriptors F.3.1 [Specifying and Verifying and Reasoning about Programs]: Specification techniques; D.2.4 [Software/Program Verification]: Model checking; I.2.11 [Distributed Artificial Intelligence]: Multiagent systems General Terms Verification Keywords Model checking, interpreted systems, epistemic logic, real time.

• Type: Conference
• Year: 2005
• Where: ATAL
• Authors: Bozena Wozna, Alessio Lomuscio, Wojciech Penczek
• Keywords: ATAL 2005, Model Checking, Model Checking Problem, Multi-agent Systems