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 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. (c) 2007 Elsevier B.V All rights reserved.
model checking temporal epistemic logics interpreted systems real time systems