Two Approaches to Bounded Model Checking for Linear Time Logic with Knowledge.

The paper deals with symbolic approaches to bounded model checking (BMC) for Linear Time Temporal Logic extended with the epistemic component (LTLK), interpreted over Interleaved Interpreted Systems. Two translations of BMC for LTLK to SAT and to operations on BDDs are presented. The translations have been implemented, tested, and compared with each other as well as with another tool on several benchmarks for MAS. Our experimental results reveal advantages and disadvantages of SAT- versus BDD-based BMC for LTLK.