Bounded Model Checking (BMC) is a technique for encoding an LTL model checking problem into a problem of propositional satisfiability. Since the seminal paper by [Biere et al.'99], the research on BMC has been primarily directed at achieving higher efficiency for solving reachability properties. In this paper, we tackle the problem of improving BMC encodings for the full class of LTL properties. We start noticing some properties of the encoding of [Biere et al.'99], and we exploit them to define improvements that make the resulting boolean formulas smaller or simpler to solve.
展开▼
机译：边界模型检查（BMC）是一种将LTL模型检查问题编码为命题可满足性问题的技术。自从[Biere et al.'99]发表具有开创性的论文以来，对BMC的研究一直主要致力于实现更高的效率来解决可达性问题。在本文中，我们解决了为整个LTL属性类改进BMC编码的问题。我们开始注意到[Biere et al.'99]编码的某些属性，并利用它们来定义改进，从而使生成的布尔公式更小或更易于求解。
展开▼
