(1.華東師范大學(xué) 上海市高可信計(jì)算重點(diǎn)實(shí)驗(yàn)室， 上海 200062；2. 桂林電子科技大學(xué) 數(shù)學(xué)與計(jì)算科學(xué)學(xué)院，廣西 桂林 541004)

摘 要：

在Petri網(wǎng)的驗(yàn)證中，代數(shù)不變式起著非常重要的作用。將Petri網(wǎng)建模為半代數(shù)變遷系統(tǒng)，提出了自動(dòng)生成不變式的算法，該不變式有助于更好地分析Petri網(wǎng)可達(dá)空間。算法首先將Petri網(wǎng)的不變式假定為一個(gè)含參數(shù)系統(tǒng)，然后通過求解半代數(shù)系統(tǒng)來求解不變式中的參數(shù)；最后，基于DISCOVERER和QEPCAD等Maple軟件包實(shí)現(xiàn)了該算法，并通過實(shí)例說明了算法的有效性。

關(guān)鍵詞：Petri網(wǎng)； 不變式； 半代數(shù)系統(tǒng)； 半代數(shù)變遷系統(tǒng)

中圖分類號(hào)：TP301文獻(xiàn)標(biāo)志碼：A

文章編號(hào)：1001-3695(2009)04-1320-03

Discovering invariants for Petri nets with DISCOVERER

BI Zhong-qin1， SHAN Mei-jing1， CHEN Guang-xi2

(1. Shanghai Key Laboratory of Trustworthy Computing， East China Normal University， Shanghai 200062，China； 2.School of Mathematics Computing Science， Guilin University of Electronic Technology， Guilin Guangxi 541004， China)

Abstract:

This paper transformed Petri nets into a semi-algebraic transition system and presented an algorithm for generating the invariant of Petri nets， which was helpful to increase the accuracy of structural methods in calculating approximations of the reachability space. The method firstly assumed the invariant of Petri nets as a parameterized system， and then evaluated para-meters in the invariant by solving the corresponding semi-algebraic system. And implemented this method associated with the computer algebra software package-DISCOVERER and QEPCAD. From preliminary experimental results， the performance of this method is significant.

Key words：Petri nets; invariant; semi-algebraic system; semi-algebraic transition system

0 引言

Petri網(wǎng)是用于建模、分析和仿真并行分布式系統(tǒng)的一種模型，該模型在分析并行系統(tǒng)的狀態(tài)行為時(shí)，具有直觀、簡(jiǎn)單等特點(diǎn)。由于模型本身表示意義的復(fù)雜性，分析Petri網(wǎng)的行為非常困難。Petri網(wǎng)中的一個(gè)關(guān)鍵性問題就是可達(dá)性分析，它就是系統(tǒng)的狀態(tài)、行為分析的基礎(chǔ)。可達(dá)性分析就是研究系統(tǒng)可能達(dá)到的狀態(tài)和狀態(tài)間的聯(lián)系。Petri網(wǎng)的很多行為特征均可歸結(jié)為可達(dá)性的研究。

可達(dá)性分析的最基本方法就是構(gòu)造可達(dá)樹，遍歷Petri網(wǎng)的所有狀態(tài)和過程，是一種最徹底但也是最低效的方法。該方法對(duì)于規(guī)模較小的Petri網(wǎng)非常有效，但隨著問題規(guī)模的增大，效率會(huì)越來越低，將面臨的一個(gè)最大的困難就是組合爆炸問題。同時(shí)，國(guó)內(nèi)外很多專家學(xué)者通過將Petri網(wǎng)的可達(dá)性問題轉(zhuǎn)換成一些其他問題求解，如文獻(xiàn)[1]中將Petri網(wǎng)轉(zhuǎn)換成代數(shù)問題，再利用Grbner基進(jìn)行判斷，該方法只對(duì)可逆的Petri網(wǎng)有效；文獻(xiàn)[2]中利用進(jìn)程代數(shù)將問題分而治之來控制組合狀態(tài)爆炸。

在Petri網(wǎng)的驗(yàn)證中，代數(shù)不變式起著較為重要的作用。本文嘗試通過求解Petri網(wǎng)的不變式來進(jìn)一步精化Petri網(wǎng)的可達(dá)狀態(tài)空間。該方法首先將Petri網(wǎng)模型映射為半代數(shù)變遷系統(tǒng)，然后將求解半代數(shù)變遷系統(tǒng)的不變式問題轉(zhuǎn)換成半代數(shù)系統(tǒng)的實(shí)解分類問題，從而用求解半代數(shù)系統(tǒng)實(shí)解分類的軟件包DISCOVERER來求解這個(gè)半代數(shù)系統(tǒng)，最終生成原Petri網(wǎng)的不變式。

近年來，許多海內(nèi)外學(xué)者對(duì)Petri網(wǎng)的不變式進(jìn)行了大量研究。文獻(xiàn)[3]基于Farkass引理生成Petri網(wǎng)的線性不變式；文獻(xiàn)[4]利用抽象解釋的方法來得到Petri網(wǎng)的不變式；文獻(xiàn)[5，6]利用Presburger代數(shù)和實(shí)代數(shù)來表示Petri網(wǎng)的狀態(tài)空間，從而求得線性不等式作為Petri網(wǎng)的不變式。

本文介紹了Petri網(wǎng)、半代數(shù)系統(tǒng)以及DISCOVERER軟件包、半代數(shù)變遷系統(tǒng)和不變式等相關(guān)概念和定理，給出了Petri網(wǎng)不變式自動(dòng)生成的算法，并通過實(shí)例對(duì)算法進(jìn)行了詳細(xì)的描述。

1 預(yù)備知識(shí)

1.1 Petri網(wǎng)

定義1 Petri網(wǎng)P=(P，T，F(xiàn)，ω，μ(0))是一個(gè)五元組。其中：

P是一個(gè)庫(kù)所的有限集合{p1，p2，…，pn};

T是一個(gè)變遷的有限集合{t1，t2，…，tm}；

F(P×T)∪(T×P)是庫(kù)所與變遷之間的有向弧集；

ω:F→N+是有向弧上的權(quán)重函數(shù)，ω(p，t)表示從庫(kù)所到變遷需要消耗的令牌數(shù)，ω(t，p)表示從變遷到庫(kù)所將產(chǎn)生的令牌數(shù)，其中p∈P，t∈T；

μ(0):P→N+表示模型的初始標(biāo)記狀態(tài)，對(duì)于每個(gè)庫(kù)所p∈P，存在np∈N+個(gè)令牌。

一個(gè)變遷t∈T在某個(gè)標(biāo)記狀態(tài)μ下是可以引發(fā)的，當(dāng)且僅當(dāng)p∈I(t)，μ(p)≥ω(p，t)。其中I(t)表示變遷t∈T的輸入庫(kù)所集。一個(gè)Petri網(wǎng)總是從一個(gè)初始標(biāo)記狀態(tài)開始，然后由可以引發(fā)的變遷引發(fā)狀態(tài)的改變。每個(gè)引發(fā)變遷的作用是從輸入庫(kù)所中消耗令牌而在輸出庫(kù)所中產(chǎn)生令牌。

所有能從某初始標(biāo)記狀態(tài)μ(0)到達(dá)的狀態(tài)集合記為R(P，μ(0))。Petri網(wǎng)的可達(dá)性分析可以表示成給定某個(gè)狀態(tài)標(biāo)記μ(i)，判定μ(i)∈R(P，μ(0))是否成立。

1.2 半代數(shù)系統(tǒng)和DISCOVERER

本節(jié)將簡(jiǎn)要介紹半代數(shù)系統(tǒng)和DISCOVERER軟件包，感興趣的讀者可以參考文獻(xiàn)[7，8]。

Q表示有理數(shù)域，Q(u1，…，ud，x1，…，xs)表示Q上變?cè)獮閡1，…，ud，x1，…，xs的多項(xiàng)式集合。其中s＞0，d≥0。在下文中，把變?cè)殖蓛蓚€(gè)部分：u=(u1，…，ud)和x=(x1，…，xs)分別稱為多項(xiàng)式中的參數(shù)和變量。

定義2 半代數(shù)系統(tǒng)（semi-algebraic system）。 一個(gè)半代數(shù)系統(tǒng)是具有如下形式的系統(tǒng)

p1(u，x)=0，p2(u，x)=0，…，ps(u，x)=0

g1(u，x)≥0，g2(u，x)≥0，…，gr(u，x)≥0

gr+1(u，x)＞0，gr+2(u，x)＞0，…，gt(u，x)＞0

h1(u，x)≠0，h2(u，x)≠0，…，hm(u，x)≠0(1)

其中：s＞0，t≥r≥0，m≥0；而pi、gj、hk皆是Q(u，x)\\Q上的多項(xiàng)式，通常簡(jiǎn)記為SAS。當(dāng)一個(gè)SAS不含參數(shù)，即d=0時(shí)，稱其為常系數(shù)半代數(shù)系統(tǒng)，否則稱其為參系數(shù)半代數(shù)系統(tǒng)。

通常，形如式(1)的半代數(shù)系統(tǒng)簡(jiǎn)單地表示成：[[P]，[G1]，[G2]，[H]]。其中：

P={p1(u，x)，p2(u，x)，…，ps(u，x)}

G1={g1(u，x)，g2(u，x)，…，gr(u，x)}

G2={gr+1(u，x)，gr+2(u，x)，…，gt(u，x)}

H={h1(u，x)，h2(u，x)，…，hm(u，x)}

對(duì)于一個(gè)常系數(shù)半代數(shù)系統(tǒng)，如何隔離常系數(shù)半代數(shù)系統(tǒng)的實(shí)根是一個(gè)非常重要的問題。對(duì)于參系數(shù)半代數(shù)系統(tǒng)，筆者關(guān)心的問題則是實(shí)根分類，即考慮參數(shù)滿足什么條件原系統(tǒng)有實(shí)解、參數(shù)滿足什么條件原系統(tǒng)有正維數(shù)實(shí)解以及參數(shù)滿足什么條件原系統(tǒng)有指定數(shù)目的實(shí)解。文獻(xiàn)[7，8]基于多項(xiàng)式判別系統(tǒng)以及柱形代數(shù)分解很好地解決了這兩類問題并在DISCOVERER中實(shí)現(xiàn)了這些算法。

DISCOVERER實(shí)現(xiàn)的算法主要包括：參系數(shù)半代數(shù)系統(tǒng)實(shí)解分類；常系數(shù)半代數(shù)系統(tǒng)實(shí)解隔離；部分柱形代數(shù)分解(PCAD)算法等。這里主要介紹兩個(gè)本文中要用到的指令tofind和Tofind的調(diào)用方式。對(duì)形如式(1)的參系數(shù)半代數(shù)系統(tǒng)S， tofind的調(diào)用方式是：

tofind([p1，p2，…，ps]，[g1，g2，…，gr]，[gr+1，gr+2，…，gt]，[h1，h2，…，hm]，[x1，x2，…，xs]，[u1，u2，…，ud]，α)

其中α可以有以下三種輸入：

a）一個(gè)非負(fù)整數(shù)b，求系統(tǒng)S恰有b個(gè)互異實(shí)解的條件；

b)一個(gè)范圍b..c（b，c是非負(fù)整數(shù)且b＜0），求系統(tǒng)S的互異實(shí)解數(shù)目介于b與c之間的條件；

c)一個(gè)范圍b..ω（b是一個(gè)非負(fù)整數(shù)，ω是一個(gè)沒有值的名稱)，求系統(tǒng)S的互異實(shí)解數(shù)目不少于b的條件。

一般情況下，tofind得到的是除了邊界情況之外的充要條件。如果對(duì)系統(tǒng)S調(diào)用tofind得到充要條件，并且得到退化的邊界條件R1=0，R2=0，…，Rl=0此時(shí)調(diào)用Tofind函數(shù)就可以得到包含退化情況的充要條件。Tofind的調(diào)用方式如下：

Tofind([p1，p2，…，ps，R1，R2，…，Rl]，[g1，g2，…，gr]，[gr+1，gr+2，…，gt]，[h1，h2，…，hm]，[x1，x2，…，xs]，[u1，u2，…，ud]，α)

其中α的取值與tofind中一樣。

1.3 半代數(shù)變遷系統(tǒng)和不變式

定義3 變遷系統(tǒng)ψ是一個(gè)五元組〈V，L，T，l0，Θ〉。其中：

V是有限變量集合，某個(gè)時(shí)刻變量的值稱為該時(shí)刻變量的狀態(tài)；

L是有限位置集合；

T是狀態(tài)變遷集，T中的元素狀態(tài)變遷τ是一個(gè)三元組〈l，l′，ρτ〉，其中l(wèi)，l′∈L，分別表示變遷之前和之后的位置，ρτ是一個(gè)變遷關(guān)系，它是V∪V′上的一個(gè)斷言，V表示當(dāng)前狀態(tài)變量集合，V′表示變遷后的狀態(tài)變量集合；

l0是初始位置；

Θ是在V上描述初始狀態(tài)的斷言。

變遷系統(tǒng)是用于表示各類程序的標(biāo)準(zhǔn)計(jì)算模型，有關(guān)變遷系統(tǒng)的詳細(xì)介紹請(qǐng)參考文獻(xiàn)[9]。

定義4 代數(shù)變遷系統(tǒng)。該系統(tǒng)是一個(gè)變遷系統(tǒng)〈V，L，T，l0，Θ〉。其中：對(duì)于每個(gè)變遷τ∈T， 變遷關(guān)系ρτ是一個(gè)V∪V′上的代數(shù)斷言，初始狀態(tài)Θ是V上的一個(gè)代數(shù)斷言。

定義5 半代數(shù)變遷系統(tǒng)。該系統(tǒng)[10]是一個(gè)特殊的代數(shù)變遷系統(tǒng)〈V，L，T，l0，Θ〉，每個(gè)變遷τ∈T是一個(gè)四元組〈l1，l2，ρτ，θτ〉。其中：l1、l2以及ρτ與變遷系統(tǒng)中的定義相同，θτ是變遷發(fā)生的條件，它可以是多項(xiàng)式等式也可以是多項(xiàng)式不等式。只有當(dāng)θτ為真時(shí)，該變遷才會(huì)被觸發(fā)。Θ是初始條件，可以是多項(xiàng)式等式也可以是多項(xiàng)式不等式。

根據(jù)Petri網(wǎng)系統(tǒng)的特點(diǎn)，可以將Petri網(wǎng)系統(tǒng)映射成為一個(gè)等價(jià)的半代數(shù)變遷系統(tǒng)。給定一個(gè)Petri網(wǎng)P:(P，T，F(xiàn)，ω，μ(0))，如果一個(gè)半代數(shù)變遷系統(tǒng)Ψ:〈V，L，T，l0，Θ〉滿足下列條件：

a)對(duì)于每個(gè)pi∈P， 總存在一個(gè)變量xi∈V與其對(duì)應(yīng)；

b)對(duì)于每個(gè)變遷t∈T總存在一個(gè)變遷τ∈T與其對(duì)應(yīng)，并且ρτ對(duì)應(yīng)的變遷關(guān)系是x′i=(xi+ωpi(O(t))-ωpi(I(t)))，變遷觸發(fā)的條件是∧p∈Pxi≥ωpi(I(t));

c)Θ=∧p∈P(xi=μ(0)(p))，則稱半代數(shù)變遷系統(tǒng)Ψ是與Petri網(wǎng)P相關(guān)聯(lián)的半代數(shù)變遷系統(tǒng)。

如圖1所示的Petri網(wǎng)系統(tǒng)，與其相關(guān)聯(lián)的半代數(shù)變遷系統(tǒng)可以表示成：

V={x1，x2，x3}，T={τ1，τ2}，Θ=(x1=1∧x2=2∧x3=2)，

ρτ1=(x′1=x1-1∧x′2=x2+1∧x′3=x3-2)，

θτ1=(x1≥1∧x2≥2∧x3≥2)，

ρτ2=(x′1=x1+1∧x′2=x2-2∧x′3=x3-2)，

θτ3=(x1≥0∧x2≥2∧x3≥2)(2)

定義6 不變式。設(shè)Ψ:〈V，L，T，l0，Θ〉是一個(gè)半代數(shù)變遷系統(tǒng)。某個(gè)位置l∈L上的不變式是指對(duì)于到達(dá)位置l的所有狀態(tài)均為真的斷言。一個(gè)半代數(shù)變遷系統(tǒng)的不變式是指在半代數(shù)變遷系統(tǒng)的所有位置均為真的斷言。

定義7 歸納斷言映射。 一個(gè)斷言映射η是歸納的當(dāng)且僅當(dāng)下列條件成立：

a)初始條件(initiation)。在初始位置l0，斷言成立，即

Θ η(l0)

b)承接條件(consecution)。對(duì)于每一個(gè)從li到lj的變遷τ，有

η(li)∧ρτ∧θτη(lj)

眾所周知，任何一個(gè)歸納斷言都是不變式[11，12]，并且現(xiàn)如今所有的不變式的生成過程都是利用歸納斷言產(chǎn)生的。對(duì)于某個(gè)代數(shù)斷言，假設(shè)它是某半代數(shù)變遷系統(tǒng)的不變式，則要求其滿足歸納斷言的初始條件和承接條件。

從以上定義可以得到如下定理：

定理1 假設(shè)ψ=〈V，L，T，l0，Θ〉是一個(gè)半代數(shù)系統(tǒng)，η是一個(gè)代數(shù)斷言，η(l)是ψ的不變式當(dāng)且僅當(dāng)下面的條件滿足：

2 不變式自動(dòng)生成

根據(jù)上面的定理1，可以得到如下求解Petri網(wǎng)不變式的算法：

a)利用Petri網(wǎng)與半代數(shù)變遷系統(tǒng)的對(duì)應(yīng)關(guān)系，將Petri網(wǎng)模型映射成相關(guān)聯(lián)的半代數(shù)變遷系統(tǒng)；

b)假設(shè)存在某個(gè)參數(shù)形式的斷言η(l)是該半代數(shù)變遷系統(tǒng)的不變式；

c)根據(jù)定理1的初始條件，計(jì)算滿足初始條件所需要的參數(shù)約束條件；

d)根據(jù)定理1的承接條件，對(duì)每個(gè)狀態(tài)變遷 τ，計(jì)算滿足承接條件所需要的參數(shù)約束條件；

e)由c)d)得到的約束條件得到一個(gè)約束求解問題，利用量詞消去得到滿足參數(shù)約束條件的解，從而得到不變式。

下面用一個(gè)簡(jiǎn)單例子(圖1)來說明該算法的詳細(xì)過程。

a)按照Petri網(wǎng)到半代數(shù)變遷系統(tǒng)的映射，將圖1所示的Petri網(wǎng)轉(zhuǎn)換成如式（2）所示的半代數(shù)變遷系統(tǒng)。

b)假設(shè)該半代數(shù)變遷系統(tǒng)具有如下形式的不變式：

a1x1+a2x2+a3x3+a4=0

令inv=a1x1+a2x2+a3x3+a4。

c)根據(jù)定理1的初始條件，調(diào)用DISCOVERER中的tofind函數(shù)得到滿足初始條件所需要的參數(shù)約束條件。調(diào)用方式如下：

tofind([x1-1，x2-2，x3-2]，[]，[]，[inv]，[x1，x2，x3]，[a1，a2，a3，a4]，0)

得到參數(shù)的約束條件為a4+2a3+2a2+a1=0。

d)根據(jù)定理1，對(duì)每個(gè)狀態(tài)變遷計(jì)算滿足承接條件所需要的參數(shù)約束條件。

(a)對(duì)于狀態(tài)變遷τ1，通過如下調(diào)用：

tofind ([inv]，[x1-1，x2-2，x3-2]，[]，[subs({x1=x1-1，x2=x2+1，x3=x3-2}，inv)]，

[x1，x2，x3]，[a1，a2，a3，a4]，0);

得到參數(shù)約束條件為2a3-a2+a1=0或a3(a1x1+a2x2+a4+2a3)＞0。其中第二個(gè)條件對(duì)于所有的x1≥1，x2≥2都必須成立。利用量詞消去工具QEPCAD[13]得到此條件等價(jià)于a1≥0∧a2≥0∧a4+2a3≥0∧a1a2(a4+2a3)≠0。

(b)對(duì)于狀態(tài)變遷τ2，通過如下調(diào)用：

 tofind([inv]，[x1，x2-2，x3-2]，[]

[subs({x1=x1+1，x2=x2-2，x3=x3-2}，inv)]，

[x1，x2，x3]，[a1，a2，a3，a4]，0);

得到參數(shù)約束條件為-2a3+a1-2a2=0或者a3(a1x1+a2x2+a4+2a3)＞0。同理，其中第二個(gè)條件對(duì)于所有的x1≥0，x2≥2都必須成立。利用量詞消去工具QEPCAD得到此條件等價(jià)于a1≥0∧a2≥0∧a4+2a3≥0∧a1a2(a4+2a3)≠0。

e)通過以上步驟可以得出如下的參數(shù)約束條件:

(a4+2a3+2a2+a1=0)∧[(2a3-a2+a1=0)∨

(a1≥0∧a2≥0∧a4+2a3≥0∧a1a2(a4+2a3)≠0)]∧

[(-2a3+a1-2a2=0)∨(a1≥0∧a2≥0∧a4+2a3≥0∧a1a2(a4+2a3)≠0)]

通過約束求解可以得到

a1=-6a3， a2=-4a3， a4=12a3

從而得到原Petri網(wǎng)的不變式為

6x1+4x2-x3-12=0

對(duì)于圖2所示的Petri網(wǎng)模型，利用同樣的方法可以得到不變式為

2x1+x2+x3+x4+x5-2=0



3 結(jié)束語

本文通過將Petri網(wǎng)模型映射成為半代數(shù)變遷系統(tǒng)，然后利用實(shí)代數(shù)中的半代數(shù)系統(tǒng)實(shí)根分類的方法來求解原Petri網(wǎng)模型的不變式，利用該不變式可以對(duì)Petri網(wǎng)模型的可達(dá)性分析起到精化作用，所有的可達(dá)狀態(tài)必須滿足該不變式。本算法在Maple軟件包DISCOVERER的基礎(chǔ)上得到了實(shí)現(xiàn)，并驗(yàn)證了其有效性。下一步考慮將算法推廣到求解Petri網(wǎng)的多項(xiàng)式形式不變式，從而可以基于符號(hào)計(jì)算、數(shù)值計(jì)算以及混合計(jì)算等科學(xué)計(jì)算領(lǐng)域眾多求解半代數(shù)系統(tǒng)的高效能算法，對(duì)Petri網(wǎng)的可達(dá)性進(jìn)行更有效的分析。

參考文獻(xiàn)：

[1]CAPROTTI O， FERSCHA A， HONG H. Reachability test in Petri nets by Grbner bases [R]. Linz， Austria:Research Institute for Symbolic Computation， Johannes Kepler University， 1995.

[2]YEH W J， YOUNG M. Compositional reachability analysis using process algebra[C]//Proc of Symposium on Testing， Analysis， and Verification. New York: ACM Press， 1991:49-59.

[3]SANKARANARAYANAN S， SIPMA H， MANNA Z. Petri net analysis using invariant generation[C]//Proc of Verification: Theory and Practice. Berlin: Springer-Verlag， 2003: 682-701.

[4]CLARISR， RODR GUEZ-CARBONELL E， CORTADELLA J. Derivation of non-structural invariants of Petri nets using abstract interpretation[C]//Proc of the 26th International Conference on Applications and Theory of Petri Nets. Berlin: Springer-Verlag， 2005: 188-207.

[5]BRARD B， FRIBOURG L. Reachability analysis of (timed) Petri nets using real arithmetic[C]//Proc of the 10th International Confe-rence on Concurrency Theory. London: Springer-Verlag， 1999: 178-193.

[6]FRIBOURG L， OLSN H. Proving safety properties of infinite state systems by compilation into Presburger arithmetics[C]//Proc of the 8th International Conference on Concurrency Theory. London:Sprin-ger-Verlag， 1997:213-227.

[7]HOARE C A R. An axiomatic basis for computer programming[J]. Communications of the ACM， 1969， 12(10): 576-580.

[8]楊路，夏壁燦. 不等式機(jī)器證明與自動(dòng)發(fā)現(xiàn)[M]. 北京: 科學(xué)出版社， 2008.

[9]MANNA Z， PNUELI A. Temporal verification of reactive systems: safety[M]. New York: Springer-Verlag， 1995.

[10]CHEN Ying-hua， XIA Bi-can， YANG Lu， et al. Generating polynomial invariants with DISCOVERER and QEPCAD[C]//Formal Methods and Hybrid Real-time. Berlin: Springer-Verlag， 2007: 67-82.

[11]DIJKSTRA E W. A discipline of programming[M]. New Jersey: Prentice-Hall Inc， 1976.

[12]FLOYD R W. Assigning meanings to programs[C]//Proc of Symposium in Applied Mathematics.[S.l.]:Providence American Mathematical Society， 1967: 19-37.

[13]BROWN C W. QEPCAD B: a program for computing with semi-algebraic sets using CADs[J]. ACM SIGSAM Bulletin， 2003，37(4): 97-100.

[14]YANG Lu， XIA Bi-can. Real solution classifications of a class of parametric semi-algebraic systems[C]//Proc of Int Conf on Algorithmic Algebra and Logic. Norderstedt: Herstellung und Verlag， 2005: 281-289.