Sciweavers

Share
ATAL
2005
Springer

Bounded model checking for knowledge and real time

10 years 1 months ago
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.
Bozena Wozna, Alessio Lomuscio, Wojciech Penczek
Added 26 Jun 2010
Updated 26 Jun 2010
Type Conference
Year 2005
Where ATAL
Authors Bozena Wozna, Alessio Lomuscio, Wojciech Penczek
Comments (0)
books