Combining syntactic and semantic encoding for LTL bounded model checking

Bounded model checking (BMC, for short) is a successful application of SAT technique in model checking. In a broad sense, BMC encoding approaches could be categorised into the syntactic fashion and semantic fashion. In this paper, we present a new BMC encoding approach specially tailored for LTL model checking. The key observation is that syntactic encoding and semantic encoding respectively have the superiority in dealing with "next" operator and "until" operator in the specification. The proposed encoding could be implemented in an "on-the-fly" manner, and finally results in a linear scale blow-up. To justify it, the approach is experimentally evaluated by comparing with some of the best known existing encodings.