BDD-versus SAT-based bounded model checking for the existential fragment of linear temporal logic with knowledge: algorithms and their performance
Artur Męski, Wojciech Penczek, Maciej Szreter, Bożena Woźna-Szcześniak, Andrzej Zbrzezny · Autonomous Agents and Multi-Agent Systems · 2013
The paper deals with symbolic approaches to bounded model checking (BMC) for the existential fragment of linear temporal logic extended with the epistemic component (ELTLK), interpreted over interleaved interpreted systems. Two translations of BMC for ELTLK 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 ELTLK.