程序验证(六):纳尔逊-欧朋算法(Nelson-Oppen Procedure)

Tattoo

发布日期: 2020-06-30 13:27:01 浏览量: 23
评分:
star star star star star star star star star star
*转载请注明来自write-bug.com

版权声明:本文为CSDN博主「swy_swy_swy」的原创文章,遵循CC 4.0 BY-SA版权协议,转载请附上原文出处链接及本声明。
原文链接:https://blog.csdn.net/swy_swy_swy/article/details/106633999

一、动机

截至目前,我们学习了一些一阶理论,每一个都是关于某一种数据类型。然而,现实中的公式并不是由单一的理论组成,如:

i.0ina[i]a[i+1]\forall i.0\le i\le n\to a[i]\le a[i+1]

这个公式实际上包含了两个理论:等价与数组。

我们需要找到一个方法,将复杂的一阶逻辑公式转化为简单的一阶逻辑公式

二、一些概念

2.1 复合理论

给定T1T_1T2T_2,且Σ1Σ2={=}\Sigma_1\cap \Sigma_2 = \lbrace = \rbrace,那么复合理论T1T2T_1\cup T_2有:

  • 符号集Σ1Σ2\Sigma_1 \cup \Sigma_2

  • 公理集A1A2A_1 \cup A_2

纳尔逊-欧朋(Nelson-Oppen)复合方法:T1T2T_1\cup T_2是可判定的,如果T1T_1T2T_2均满足:

  • 是量词自由的合取的片段(Quantifier-free, conjunctive fragments)

  • 可判定的

  • 稳定无限的(stably-infinite)

2.2 稳定无限的理论

一个建立在符号集Σ\Sigma上的理论TT是稳定无限的,如果对于每个量词自由的公式FF,只要FFTT-可满足的,存在一个解释,它的大小(cardinality)是无限的。

例如这样的一个理论:

Σ={a,b,=}\Sigma =\{a,b,=\}

公理x.x=ax=b\forall x.x=a\vee x=b

这个理论不是稳定无限的,因为每个解释(D,I)(D,I)都有这样的性质:DD包含至多两个元素,即D2|D|\le 2

但是大多数我们关心的理论,即TE,TA,TZT_E,T_A,T_Z等等,都是稳定无限的。

三、纳尔逊-欧朋算法

3.1 概况

输入:由复合理论T1T2T_1\cup T_2得到的公式FF

输出:等价的公式F1F2F_1\wedge F_2,这里:

  • 其中F1F_1是一个T1T_1公式

  • 其中F2F_2是一个T2T_2公式

这个算法的功能

  • FF净化为F1F_1F2F_2

  • F1F_1F2F_2中共享的变量做等价变换

3.2 步骤1:变量抽象

3.2.1 理论

目标FF中所有的文字或者属于T1T_1,或者属于T2T_2,但不能是二者共有

方法:将以下两个转化方法不断使用,直到不能再用为止:

  • 对于任何一项f(..,t,..)f(.. , t, ..),满足fΣif\in \Sigma_itΣit\notin \Sigma_i,将tt用一个新的(fresh)变量ww替换,并在最后合取上t=wt=w

  • 对于任一谓词p(..,t,..)p(.. ,t, ..),满足pΣip\in \Sigma_itΣit\notin \Sigma_i,将tt用一个新的(fresh)变量ww替换,并在最后合取上t=wt=w

  • 结束的时候,我们就可以把FF分为F1F_1F2F_2

3.2.2 举例

考虑TETZT_E\cup T_Z公式FF

F:1xx2f(x)f(1)f(x)f(2)F:1\le x\wedge x\le 2\wedge f(x)\ne f(1)\wedge f(x)\ne f(2)

  • TET_E中的非逻辑符是哪些?f,=f,=

  • TZT_Z中的非逻辑符是哪些? 1,2,,=1,2,\le,=

  • 净化:用f(w1)f(w_1)代替f(1)f(1),用f(w2)f(w_2)代替f(2)f(2),加入w1=1w_1=1w2=2w_2=2,得到

1xx2f(x)f(w1)f(x)f(w2)w1=1w2=21\le x\wedge x\le 2\wedge f(x)\ne f(w_1)\wedge f(x)\ne f(w_2)\wedge w_1=1\wedge w_2=2

  • 其中FE:f(x)f(w1)f(x)f(w2)F_E:f(x)\ne f(w_1)\wedge f(x)\ne f(w_2)

  • 其中FZ:1xx2w1=1w2=2F_Z:1\le x\wedge x\le 2\wedge w_1 = 1\wedge w_2 = 2

3.3 步骤2:猜测与检查(guess and check)

3.3.1 理论

给定F1F_1F2F_2,定义共享变量集VV

V=free(F1)free(F2)V=free(F_1)\cap free(F_2)

EEVV上的一个等价关系,由EE生成的arrangement α(V,E)\alpha (V,E)即为:

α(V,E):u,vV.uEvu=vu,vV.¬(uEv)u¬v\alpha (V,E): \bigwedge _{u,v\in V.uEv} u=v \wedge\bigwedge _{u,v\in V.\neg (uEv)} u\neg v

公式F=F1F2F=F_1 \wedge F_2(T1T2)(T_1\cup T_2)-可满足的当且仅当存在这样的α(V,E)\alpha (V,E)使得:

  • 其中F1α(V,E)F_1\wedge \alpha (V,E)T1T_1-可满足的

  • 其中F2α(V,E)F_2\wedge \alpha (V,E)T2T_2-可满足的

3.3.2 举例

考虑之前的净化后的两个公式,共享变量V={w1,w2,x}V= \lbrace w_1,w_2,x \rbrace

猜测并检查VV上的等价关系:

{{w1},{w2},{x}}\{\{w_1\},\{w_2\},\{x\}\}

{{w1,w2},{x}}\{\{w_1,w_2\},\{x\}\}

{{w1},{w2,x}}\{\{w_1\},\{w_2,x\}\}

{{w2},{w1,x}}\{\{w_2\},\{w_1,x\}\}

{{w1,w2,x}}\{\{w_1,w_2,x\}\}

3.3.3 效率问题

这个guess and check的时间复杂度是指数级的,所以不太实用,所以我们换个方法。

3.4 步骤3:等价推导(equality propagation)

3.4.1 凸理论(convex theory)

一个理论是凸的(convex),如果它对于每个变量自由的公式FF,都满足:

Fi=1nui=viF\Rightarrow \bigvee ^n_{i=1} u_i =v_i

Fui=vi for some i{1,..,n}F\Rightarrow u_i = v_i~for~some~i\in\{1,.. , n\}

其中TZ,TAT_Z, T_A不是凸的,但是TE,TQT_E,T_Q是凸的。

举例:TZT_Z不是凸的

例如,考虑这样的量词自由的合取ΣZ\Sigma_Z -公式

F:1zz2u=1v=2F: 1\le z\wedge z\le 2\wedge u=1\wedge v=2

那么

Fz=uz=vF\Rightarrow z=u\vee z=v

但是无法推出

Fz=uF\Rightarrow z=u

Fz=vF\Rightarrow z=v

3.4.2 等价推导

给定F1F_1F2F_2

  • Ti(i=1,2)T_i (i=1,2)报告任何有关共享变量(包括u,vu, v)的新推出的等价关系

    • 如果TiT_i是凸的,令u=vu=v为新推出的等价关系

    • 如果TiT_i不是凸的,令i(ui=vi)\bigvee_i (u_i = v_i)为推出的等价关系的析取

  • 将新推出的等价关系存储到EE中(EE是已经发现的等价关系的集合)

    • 如果TiT_i是凸的,将u=vu=v添加到EE

    • 如果TiT_i不是凸的,将搜索过程依据不同的析取i(ui=vi)\bigvee_i(u_i = v_i) 分成不同的分支(通过在EEE中添加相应的等价关系)

  • 对于每一个分支,将EEE传播到另一个判定程序(也就是递归进行),重复以上步骤

算法返回

  • satsat如果任一分支得到一个完整的arrangement

  • unsatunsat如果所有的分支都推出矛盾

  • satsat如果所有的分支都不能发现新的等价关系

3.4.3 举例

考虑ΣEΣQ\Sigma_E\cup \Sigma_Q-公式

F:f(f(x)f(y))f(z)xyy+zx0zF:f(f(x)-f(y))\ne f(z)\wedge x\le y\wedge y+z\le x\wedge 0\le z

在第一步后,FF被分为两个公式:

FE:f(w)f(z)u=f(x)v=f(y)F_E:f(w)\ne f(z)\wedge u=f(x)\wedge v=f(y)

FQ:xyy+zx0zw=uvF_Q:x\le y\wedge y+z\le x\wedge 0\le z\wedge w=u-v

V=shared(FE,FQ)={x,y,z,u,v,w}V=shared(F_E,F_Q)=\{x,y,z,u,v,w\}

注意,TET_ETQT_{Q}都是凸理论。

于是

考虑TETZT_E\cup T_{Z}-公式FF

F:1xx2f(x)f(1)f(x)f(2)F:1\le x\wedge x\le 2\wedge f(x)\ne f(1)\wedge f(x)\ne f(2)

在第一步后,FF被分为两个公式:

FE:f(x)f(w1)f(x)f(w2)F_E:f(x)\ne f(w_1)\wedge f(x)\ne f(w_2)

FZ:1xx2w1=1w2=2F_{Z} :1\le x\wedge x\le 2\wedge w_1=1\wedge w_2=2

V=shared(FE,FZ)={w1,w2,x}V=shared(F_E,F_{Z})=\{w_1,w_2,x\}

注意,TET_E是凸的,TZT_{Z}不是。

于是

考虑TETZT_E\cup T_{Z}-公式FF

F:1xx3f(x)f(1)f(x)f(3)f(1)f(2)F: 1\le x\wedge x\le 3\wedge f(x)\ne f(1)\wedge f(x)\ne f(3)\wedge f(1)\ne f(2)

在第一步后,FF被分为两个公式:

FE:f(x)f(w1)f(x)f(w3)f(w1)f(w2)F_E:f(x)\ne f(w_1)\wedge f(x)\ne f(w_3)\wedge f(w_1)\ne f(w_2)

FZ:1xx3w1=1w2=2w3=3F_{Z}:1\le x\wedge x\le 3\wedge w_1=1\wedge w_2=2\wedge w_3=3

V=shared(FE,FZ)={w1,w2,w3,x}V=shared(F_E,F_{Z})=\{w_1,w_2,w_3,x\}

注意,TET_E是凸的,TZT_{Z}不是。

于是

上传的附件

发送私信

人生最好的三个词:久别重逢,失而复得,虚惊一场

48
文章数
33
评论数
最近文章
eject