Bounded model checking for knowledge and real time
作者：
Highlights：
•
摘要
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.
论文关键词：Temporal epistemic logics,Model checking,Interpreted systems,Real time systems
论文评审过程：Received 23 August 2006, Revised 2 April 2007, Accepted 11 May 2007, Available online 24 May 2007.
论文官网地址：https://doi.org/10.1016/j.artint.2007.05.005
