Improved Bounded Model Checking for a Fair Branching-Time Temporal Epistemic Logic

摘要

Bounded model checking is a verification technique based on searching for counter-examples to the validity of the specification using an encoding to propositional sastisfiability. The paper identifies a number of inefficiencies in prior encodings for bounded model checking for a logic of knowledge and branching time. An alternate encoding is developed, and theoretical and experimental results are presented that show this leads to improved performance of bounded model checking for a range of examples.