SAT-based bounded model checking for propositional projection temporal logic

This paper presents a bounded model checking (BMC) approach for propositional projection temporal logic (PPTL). To this end, first PPTL is briefly introduced. Then, bounded semantics of PPTL is defined according to its semantics in logic theory. Further, a reduction method from BMC to SAT is given in detail. In addition, an example is presented to illustrate how the approach works. Finally, miniSAT is employed to solve the SAT based BMC problem by means of verifying RMS algorithm in detail. Our experience shows that SAT based BMC approach for PPTL proposed in the paper is useful and feasible.

Authors

• Zhenhua Duan Xidian University
• Cong Tian Xidian University
• Nan Zhang
• Chaofeng Yu
• Mengfei Yang
• Jia He Chinese People’s Liberation Army 95841 troops

Keywords

• Propositional projection temporal logic
• Bounded model checking
• Rate monotonic scheduling