Complexity and Algorithms for Monomial and Clausal Predicate Abstraction
Complexity and Algorithms for Monomial and Clausal Predicate Abstraction
复制标题
单项式和从句谓词抽象的复杂性和算法
DOI：
10.1007/978-3-642-02959-2_18
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
S. Qadeer
中科院分区：
文献类型：
--
作者：
Shuvendu K. Lahiri;S. Qadeer
在本文中，我们研究了各种谓词抽象问题的渐近复杂性，相对于在给定断言逻辑中检查注释程序的渐近复杂性。与以往的方法不同，我们将谓词抽象问题作为决策问题，而不是传统的推理问题。对于在最弱（自由）前提和布尔连接下关闭的断言逻辑，我们给出了谓词抽象问题的两个限制，其中两个复杂性匹配。这些限制对应于单项抽象和子句抽象的情况。对于这些限制，我们展示了一种符号编码，它将谓词抽象问题简化为检查单个公式的可满足性，该公式的大小是程序和谓词集大小的多项式。我们还提供了一种新的求解子句抽象问题的迭代算法，可以看作是解决单项抽象问题的胡迪尼算法的对偶。
In this paper, we investigate the asymptotic complexity of various predicate abstraction problems relative to the asymptotic complexity of checking an annotated program in a given assertion logic. Unlike previous approaches, we pose the predicate abstraction problem as a decision problem, instead of the traditional inference problem. For assertion logics closed under weakest (liberal) precondition and Boolean connectives, we show two restrictions of the predicate abstraction problem where the two complexities match. The restrictions correspond to the case of monomial and clausal abstraction. For these restrictions, we show a symbolic encoding that reduces the predicate abstraction problem to checking the satisfiability of a single formula whose size is polynomial in the size of the program and the set of predicates. We also provide a new iterative algorithm for solving the clausal abstraction problem that can be seen as the dual of the Houdini algorithm for solving the monomial abstraction problem.