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

Abstract. Bounded model checking is a verification technique based on search-ing 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 exper-imental results are presented that show this leads to improved performance of bounded model checking for a range of examples.