Title of article
Bounded model checking for knowledge and real time Original Research Article
Author/Authors
Alessio Lomuscio، نويسنده , , Wojciech Penczek، نويسنده , , Bo?ena Wo?na، نويسنده ,
Issue Information
روزنامه با شماره پیاپی سال 2007
Pages
28
From page
1011
To page
1038
Abstract
We present TECTLK, a logic to specify knowledge and real time in multi-agent systems. We show that the TECTLK model checking problem is decidable, and we present an algorithm for 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.
Keywords
Interpreted systems , Real time systems , Temporal epistemic logics , Model checking
Journal title
Artificial Intelligence
Serial Year
2007
Journal title
Artificial Intelligence
Record number
1207566
Link To Document