We present an extension of a bounded model checking algorithm to deal
with temporal epistemic formulas. We use the algorithm to solve a
variant of the bit transmission problem.
Keywords :
interpreted systems, temporal logic, logic of knowledge,
bounded model checking, translation to SAT, system verification
