Bounded Model Checking (BMC) is a technique for encoding an LTL model checking problem into a problem of propositial satisfiablity. Since the seminal paper [Biere et al, 1999a], the research on BMC has been primarily directed toward achieving efficiency for solving reachability properties. In this paper, we tackle the problem of improving BMC encodings for the full class of LTL probperties. We start noticing some properties of the encodings of [Biere et al, 1999a], and we exploit them to propose improvements that make the results boolean formuae smaller or simpler to solve
Improving the encoding of LTL Model Checking into SAT
Cimatti, Alessandro;Pistore, Marco;Roveri, Marco;Sebastiani, Roberto
2002-01-01
Abstract
Bounded Model Checking (BMC) is a technique for encoding an LTL model checking problem into a problem of propositial satisfiablity. Since the seminal paper [Biere et al, 1999a], the research on BMC has been primarily directed toward achieving efficiency for solving reachability properties. In this paper, we tackle the problem of improving BMC encodings for the full class of LTL probperties. We start noticing some properties of the encodings of [Biere et al, 1999a], and we exploit them to propose improvements that make the results boolean formuae smaller or simpler to solveFile in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
