信息系統(tǒng)更新的自動機

曹發(fā)生

中山大學(xué)邏輯與認(rèn)知研究所

caofasheng@163.com

信息系統(tǒng)更新的自動機

曹發(fā)生

中山大學(xué)邏輯與認(rèn)知研究所

caofasheng@163.com

通過引入信息等價和信息范式這兩個主要概念，給出了信息系統(tǒng)更新的自動機。用自動機理論給出信息系統(tǒng)更新的模型的刻畫，證明了星動作算子在信息系統(tǒng)的動態(tài)更新的邏輯系統(tǒng)的引入的不必要性，并且得到了自動機的語言和信息更新的聯(lián)系。最后利用自動機理論研究了信息系統(tǒng)及其更新邏輯系統(tǒng)的模型檢測的時間復(fù)雜性。

信息系統(tǒng)；動態(tài)；自動機；模型檢測

粗糙集理論中的知識表達方式（[12,13]）一般采用信息表或稱為信息系統(tǒng)的形式，對于粗糙集理論的邏輯推理系統(tǒng)來說，粗糙集公理系統(tǒng)是至關(guān)重要的。自從Lin在文[9]首次用公理化方法研究粗糙集之后，出現(xiàn)了許多關(guān)于粗糙集理論公理化方法方面的研究。（[3,8,10,11,15,17]）Khan利用公理化方法在文[6,7]中給出完全和不完全信息系統(tǒng)的邏輯系統(tǒng)。他們用框架語義建立邏輯系統(tǒng)的模型，這種模型是建立在粗糙集理論基礎(chǔ)之上的，并且給出邏輯系統(tǒng)的可靠性和完全性。

如何表達信息系統(tǒng)的更新過程，以至形成邏輯系統(tǒng)，有助于計算機對信息系統(tǒng)做形式推演。本文致力于表達清楚信息系統(tǒng)的更新過程，具體表現(xiàn)為：刻畫出從初始信息系統(tǒng)到終結(jié)信息系統(tǒng)的更新過程中的形式語言。形式自動機（[16]）是能夠識別形式語言的數(shù)學(xué)系統(tǒng)，它可以用來檢驗輸入的符號串是不是語言中符合語法的句子。如果是符合語法的句子，自動機就接收它；如果不是，就不接收它。自動機的狀態(tài)轉(zhuǎn)換圖就是進程演變的數(shù)學(xué)結(jié)構(gòu)，因此我們用自動機來刻畫信息系統(tǒng)的更新。我們將不同的信息系統(tǒng)作為自動機的不同狀態(tài)，用原子信息作為自動機的字母表，建立信息系統(tǒng)更新的自動機，得到該自動機語言和信息更新的聯(lián)系：該自動機的任何可接受的語言都是從初始信息系統(tǒng)到終結(jié)信息系統(tǒng)的更新過程。

1 預(yù)備知識

定義1([12])一個信息系統(tǒng)（IS）S是一個四元組S=(W,A,V,f)，其中

(1)W是對象的非空有限集合，稱為論域；

(2)A是屬性的非空有限集合；

(4)f:W×A-→V是一個映射，即對每一個對象的任意屬性都賦予了一個屬性值。

不含未知屬性值符號的信息系統(tǒng)，稱為完全信息系統(tǒng)。

注記1我們在本文中限定A是屬性的非空有限集合。有這樣的限制，我們就可以研究信息系統(tǒng)模型檢測的復(fù)雜性；再者，計算機處理的信息系統(tǒng)知識庫都是有限屬性集合，所以這樣的限制是可行的。

下面敘述本文要用到的粗糙集理論中的一些定義。

定義2([12,13])S=(W,A,V,f)是一個完全信息系統(tǒng)，對于任意的B?A，定義W上的二元關(guān)系IND(B)為：(x,y)∈IND(B)當(dāng)且僅當(dāng)，對任意的a∈B都有f(x,a)=f(y,a)；S=(W,A,V∪{?},f)是一個信息系統(tǒng)，對于任意的B?A定義W上的二元關(guān)系SIM(B)為：(x,y)∈SIM(B)當(dāng)且僅當(dāng)，對任意的a∈B都有f(x,a)=f(y,a)或者f(x,a)=?或者f(y,a)=?。

注記2下文的二元關(guān)系R的元素(x,y)∈R，我們有時候也用xRy來表示。下文中用xR1yR2z來表示xR1y并且yR2z。定義3([12,13])任給二元關(guān)系R?W×W，對于任意的x∈W記xR={y| xRy}，對于任意的X?W定義W的兩個子集合及X={x∈W|xR∩X?}，分別稱它們?yōu)閄的R下近似集合和上近似集合。

“完全信息系統(tǒng)”與“信息系統(tǒng)”的本質(zhì)區(qū)別在于是否存在未知屬性值。在完全信息系統(tǒng)的粗糙集理論中的關(guān)系是等價關(guān)系，而在信息系統(tǒng)的粗糙集理論中的關(guān)系是相似關(guān)系。

接下來按Stanley Burris（[2]）給出關(guān)于信息系統(tǒng)S一類泛代數(shù)AS的定義。

定義4設(shè)S=(W,A,V∪{?},f)，代數(shù)的語言（型）,其中?是二元函數(shù)符號，～，是一元函數(shù)符號，(a,v)是零元函數(shù)符號。

關(guān)于S的一類泛代數(shù)AS是一個結(jié)構(gòu)AS=〈2W,F〉。

2 信息系統(tǒng)的邏輯系統(tǒng)（LIS）

LIS的語言L采用Pawlak在文[14]及Khan在文[7]中給出的方式定義。

2.1 LIS的語法

定義5LIS語言L的字母表包括以下部分：

(1)一個有窮非空集合A，其元素稱為屬性常元，用符號a或加數(shù)字下標(biāo)表示；

(2)集合A的子集合符號，用B或加數(shù)字下標(biāo)表示；

(3)特殊屬性值（空值）符號?，及對每一個a∈A有一個有窮非空集合Va，其元素是屬性值常元，用符號v或va或加數(shù)字下標(biāo)表示；

(4)邏輯聯(lián)結(jié)符號?，∧，[IND(B)]，[SIM(B)]；

(5)兩個常元符號?，⊥；

(6)變元符號，用α，β，γ或加數(shù)字下標(biāo)表示；

(7)命題變元符號集合PV，其元素用符號p或加數(shù)字下標(biāo)表示；

(8)技術(shù)性符號：(，)，,，[，]。

定義6LIS的合式公式的形成規(guī)則：

(1)常元符號?，⊥，命題變元符號，變元符號是合式公式；

(2)(a,v)是合式公式，也簡記為av，稱為描述子；

(3)若α，β是合式公式，則?α，α∧β，[IND(B)]α，[SIM(B)]α是合式公式；

(4)僅由以上三條形成合式公式。全體描述子的集合記為D，全體合式公式的集合記為P。

2.2 LIS的語義

LIS語言L的語義是基于模態(tài)邏輯（[1]）模型的框架語義。

定義7([7])一個模型是一個組M=(W,{IND(B)}B?A,{SIM(B)}B?A,m,P)，其中

(1)W是一個非空集合；

(2)IND(B)，SIM(B)是W上的二元關(guān)系；

(3)m:D-→2W；

(4)P:PV-→2W。

下面我們敘述合式公式在模型中的可滿足性的定義：

定義8([7])任給語言L中的合式公式α如下歸納定義模型M在w∈W上

可滿足，記為M,w|=α:

(1)M,w|=?；

(2)非M,w|=⊥；

(3)M,w|=(a,v)當(dāng)且僅當(dāng)，w∈m(av)；

(4)M,w|=p當(dāng)且僅當(dāng)，w∈P(p)；

(5)M,w|=?α當(dāng)且僅當(dāng)，非M,w|=α；

(6)M,w|=α∧β當(dāng)且僅當(dāng)，M,w|=α并且M,w|=β；

(7)對于任意的R∈{IND(B)}B?A∪{SIM(B)}B?A，M,w|=[R]α當(dāng)且僅當(dāng)，對任意的wRw′的w′都有M,w′|=α。

定義9([7])給定S=(W,A,V∪{?},f)，它的標(biāo)準(zhǔn)模型為

MS=(W,{IND(B)}B?A,{SIM(B)}B?A,mS,P)，其中

(1)mS(a,v):={x∈W|f(x,a)=v}；

(2)P:PV-→2W。

在不混淆時候用S表示它的標(biāo)準(zhǔn)模型MS。在S的標(biāo)準(zhǔn)模型MS中，[R]α在模型解釋下集合和粗糙集有著緊密的聯(lián)系，具體如下：

定理1m([R]α)=m(α)。

證明.設(shè)x∈m([R]α)，由定義8(7)得，對任意的xRy的y都有y∈m(α)。這也即是，對任意的y∈xR都有y∈m(α)。由定義3中下近似集合定義得，x∈)。這些都是當(dāng)且僅當(dāng)?shù)?，于是反過來也成立。故m([R□

Khan在文[6,7]給出了LIS的公理和推理規(guī)則，并且給出了可靠性和完全性定理。本文的主要目標(biāo)是給出信息系統(tǒng)的更新的自動機表示，下面就要先給出信息系統(tǒng)更新的邏輯系統(tǒng)。

3 信息系統(tǒng)更新的邏輯系統(tǒng)(DLIS)

DLIS語言LD采用Khan在文[7]中給出的方式定義。

3.1 DLIS的語法

定義10DLIS語言LD的字母表包括以下部分：

(1)L的字母表；

(2)兩個信息更新算子符號：∨（選擇）和;（合成）。

信息上的運算已經(jīng)有兩個二元運算，在一般的動態(tài)邏輯中都有二元算符(合成和選擇)及一元算符(星)。我們本來打算按照動態(tài)邏輯（[4]）的模式在這個信息系統(tǒng)更新的邏輯系統(tǒng)中加上一個新的更新算子符號星算子?，因而就引入更新的自動機，但是利用自動機理論發(fā)現(xiàn)這個星算子的引入是平凡的。文章的第4部分將給出證明。

定義11信息的形成規(guī)則：

(1)原子信息(α,a,v)是信息，這里α∈P，a∈A，v∈Va；

(2)若σ，σ′是信息，則σ;σ′，σ∨σ′是信息；

(3)僅由以上兩條形成信息。

全體原子信息的集合記為AInf，全體信息的集合記為Inf。

我們設(shè)定合成算子的結(jié)合的緊密性比選擇算子的結(jié)合的緊密性高，即是說σ1;σ2∨σ3表示(σ1;σ2)∨σ3。

定義12DLIS的合式公式的形成規(guī)則：

(1)常元符號?，⊥，命題變元符號是合式公式；

(2)(a,v)是合式公式，也簡記為av，稱為描述子；

(3)若α，β是合式公式，則?α，α∧β，[IND(B)]α，[SIM(B)]α是合式公式；

(4)若α是合式公式，σ是信息，則[σ]α是合式公式；

(5)僅由以上四條形成合式公式。

3.2 DLIS的語義

定義13([7])設(shè)M=(W,{IND(B)}B?A,{SIM(B)}B?A,m,P)是一個模型，定義由原子信息σ0=(α,a,v)更新模型M所得模型，或稱為M的σ0更新模型，記為

其中Pσ0:=P；另外，mσ0如下給出：

R(B)σ0,R∈{IND,SIM},B?A如下給出：

這個定義可以推廣到原子信息的合成上的更新信息系統(tǒng)M(σ1;σ2;...;σk):= ((((Mσ1)σ2)...)σk)，這對定理3的證明起著非常重要的作用。

下面定義關(guān)于信息σ的模型間的二元關(guān)系Rσ，我們用花體R來區(qū)別W上的二元關(guān)系R，但都是集合論中的二元關(guān)系。

定義14([7])MRσM′歸納于σ的結(jié)構(gòu)如下：

(1)MR(α,a,v)M′當(dāng)且僅當(dāng)，M′=M(α,a,v)；

(2)MRσ;σ′M′當(dāng)且僅當(dāng)，存在模型M′使得MRσM′且M′Rσ′M′；

(3)MRσ∨σ′M′當(dāng)且僅當(dāng)，MRσM′或者MRσ′M′。

定義15若MRσM′則稱模型M′是模型M由信息σ更新而得到的模型，也稱σ是從M′到M的信息更新。

引理1對于原子信息的合成信息σ和M來說，僅存在一個模型M′使得MRσM′。

這個引理根據(jù)Rσ的定義容易得證，故略去證明過程，它將在下節(jié)的定理5的證明中被用到。接下來給出由更新算子所得合式公式的可滿足性的定義：

定義16([7])M,w|=[σ]α當(dāng)且僅當(dāng)，對任意的MRσM′的M′都有M′,w|= α。

為了引入信息系統(tǒng)更新的自動機，我們需要兩個重要的概念，即：信息的等價和信息的范式。下面我們就來給出它們的定義。

定義17(信息的等價)如果MRσM′當(dāng)且僅當(dāng)MRσ′M′，則稱信息σ與σ′等價，記為σ≡σ′。

注記3信息的等價是個等價關(guān)系。

定義18(信息的范式)有窮多個原子信息的合成稱為合成信息；有窮多個原子信息的選擇稱為選擇信息。有窮多個合成信息的選擇稱為選擇范式信息，這里的合成信息也稱為析取支；有窮多個選擇信息的合成稱為合成范式信息，這里的選擇信息也稱為合取支。

注記4原子信息既是一個選擇范式，也是合成范式。

有了這兩個概念，我們得到下面的一個基礎(chǔ)型的定理：

定理2(信息的范式表示)(1)每個信息σ都有一個選擇范式與它等價。

(2)每個信息σ都有一個合成范式與它等價。

為了證明這個定理，先給出關(guān)于等價的分配性的引理：

引理2(1)σ1;(σ2∨σ3)≡σ1;σ2∨σ1;σ3。

(2)σ1;σ2∨σ3≡(σ1∨σ3);(σ2∨σ3)。

證明.(1)設(shè)MRσ1;(σ2∨σ3)M′，由R定義知存在M′使得MRσ1M′R(σ2∨σ3)M′即是MRσ1M′并且（M′Rσ2M′或者M′Rσ3M′），當(dāng)且僅當(dāng)，（MRσ1M′并且M′Rσ2M′）或者（MRσ1M′并且M′Rσ3M′），于是MRσ1;σ2∨σ1;σ3M′。

故σ1;(σ2∨σ3)≡σ1;σ2∨σ1;σ3。

邏輯對偶地可類似證明(2)成立。 □

注記5這個引理還能推廣到更一般的有窮個的分配律上，如σ1;(σ2∨σ3∨···∨σk)≡σ1;σ2∨σ1;σ3∨···∨σ1;σk。;和∨在等價意義下都具有結(jié)合律。

定理2的證明.歸納于σ的結(jié)構(gòu)，同時證明(1)和(2)。

基礎(chǔ)部分：當(dāng)σ是原子信息，則它本身已是一個選擇范式，也是合成范式。歸納部分：當(dāng)σ是σ1;σ2形式，(1)由歸納假設(shè)有（這里σ;表示σ的合成范式），已是合成范式。(2)由歸納假設(shè)有（這里σ∨表示σ的選擇范式），由引理2(1)可知它能等價為一個選擇范式。

當(dāng)σ是σ1∨σ2形式，(1)由歸納假設(shè)有（這里 σ;表示σ的合成范式），由引理2(2)可知它能等價為一個合成范式。(2)由歸納假設(shè)有（這里σ∨表示σ的選擇范式），已是一個選擇范式。

綜上所述，定理2得證。 □

有了這個定理，我們把信息等價的選擇范式的析取支簡稱為信息的的析取支。

4 信息系統(tǒng)更新的自動機

由信息的范式定理，任給的信息可以轉(zhuǎn)化成范式形式，于是我們將信息系統(tǒng)更新的自動機的輸入字母表定義為全體原子信息。本節(jié)中我們討論IS上的更新，即是討論從一個IS通過怎么的信息更新過程得到新的IS。從模型的角度上說，我們只局限于討論由IS對應(yīng)的標(biāo)準(zhǔn)模型。我們研究的IS中的屬性集合是有窮的，而Khan在文[7]命題5.6中指出僅包含有窮個屬性的語言下的一般模型和這種由IS對應(yīng)的標(biāo)準(zhǔn)模型是等價的，所以這樣的限制是合理的。

給定S及信息集合Inf，利用這些信息對S進行信息更新可以得到新的信息系統(tǒng)。記與S具有相同的對象集合，相同的屬性集合，相同的屬性值集合的全體信息系統(tǒng)為QS。記信息集合的原子信息的全體為ΣS，簡記為Σ。

下面我們來給出由原子信息σ0=(α,a,v)更新S得到Sσ0定義。

定義19由原子信息σ0=(α,a,v)更新S所得Sσ0，或稱為S的σ0更新信息系統(tǒng)，記為Sσ0=(W,A,V,fσ0)：

(1)W、A、V=∪a∈AVa和?是更新前的信息系統(tǒng)中的定義。

(2)fσ0如下給出：

(2.1)當(dāng)x∈[[α]]MS時，fσ0(x,a):=v；

(2.2)當(dāng)x∈[[α]]MS且a′a時，fσ0(x,a′):=f(x,a′)；

任給S，給定原子信息集合AInf，歸納定義一類信息系統(tǒng)的集合QS，簡記為Q。

定義20Q中的元素歸納定義如下：

(1)S是Q的元素；

(2)若S′是Q的元素，則對于任意的σ∈AInf，(S′)σ是Q中的元素；

(3)僅由以上兩條形成Q中的元素。

有了上面的準(zhǔn)備工作，接下來我們給出信息系統(tǒng)更新的自動機表示。

定義21給定初始信息系統(tǒng)S0，在原子信息集合AInf上進行更新的自動機是一組結(jié)構(gòu)T=(Q,Σ,δ,S0)，其中：

(1)Q是有限的非空的狀態(tài)集合，也即是信息系統(tǒng)的集合；

(2)Σ是有限的字母表，也即是原子信息集合AInf；

(3)δ:Q×Σ-→Q是狀態(tài)轉(zhuǎn)換函數(shù)，δ(S,σ):=Sσ；

(4)S0是初始狀態(tài)。

定義22在原子信息集合AInf上進行更新的帶有終結(jié)狀態(tài)的自動機是一組結(jié)構(gòu)T=(Q,Σ,δ,S0,Sfin)，其中：

(1)Q是有限的非空的狀態(tài)集合，也即是信息系統(tǒng)的集合；

(2)Σ是有限的字母表，也即是原子信息集合AInf；

(3)δ:Q×Σ-→Q是狀態(tài)轉(zhuǎn)換函數(shù)，δ(S,σ):=Sσ；

(4)S0是初始狀態(tài)，Sfin是終結(jié)狀態(tài)。

由自動機理論知δ能唯一擴充為Q×Σ?到Q上的映射：δ(S,σ)= δ(S,σ0;σ′):=δ(Sσ0,σ′)。

注記6由引理1可得信息系統(tǒng)更新的自動機是確定性有限自動機。

定理3任意給定原子信息集合AInf，則對于任意的原子信息的合成信息σ都有σ;σ≡σ。

證明.由信息等價的定義知，要證σ;σ≡σ，只要證明出Rσ;σ=Rσ即可。先證Rσ;σ?Rσ。若MRσ;σM′，由R的定義得，存在M′使得MRσM′RσM′，即有M′=Mσ，M′=M′σ。由定義13知，(Mσ)σ=Mσ，故M′=M′σ= (Mσ)σ=Mσ。于是MRσM′，故Rσ;σ?Rσ。再證Rσ;σ?Rσ。若MRσM′，由R的定義有，M′=Mσ。由定義13知，(Mσ)σ=Mσ，故M′=(Mσ)σ=Mσ。□于是MRσ;σM′，故Rσ;σ?Rσ。

這即表明：在信息系統(tǒng)中，如果獲得一個信息，反復(fù)按這個信息對系統(tǒng)進行更新，和僅用這個信息更新一次達到的效果是相同的。因此在信息系統(tǒng)更新的邏輯系統(tǒng)中沒必要引入如動態(tài)邏輯系統(tǒng)（[4]）中的那個星算子。下面舉個例子來加以說明。

例1 設(shè)S=(W,A,V,f)，其中W={A1,...,A7}，A={size,animality,colour}，f如表1所示。

表1 :S的信息表

經(jīng)信息σ=((size,s)∧(animality,cat),colour,brown)更新S所得Sσ，則由定義13可計算出更新系統(tǒng)Sσ=(W,A,V,fσ)，fσ如表2所示，同理可得Sσ;σ=Sσ。

注記7Khan M A.和Banerjee M.在文[7]沒有提出重復(fù)更新的描述，本文的定理3給出重復(fù)更新算子（星算子）的意義。這也符合經(jīng)過同一信息更新若干次和更新一次的效果是相同的這一事實。因此沒有必要引入星算子。

定理4MS,x|=[σ]α當(dāng)且僅當(dāng)對σ的每一個析取支τ，都有Mδ(S,τ),x|=α。

證明.先證“=?”，假設(shè)當(dāng)且僅當(dāng)?shù)淖筮叧闪?。任給σ的一個析取支τ，由Rτ的定義有MSRτMδ(S,τ)。再設(shè)σ∨是σ的選擇范式，由Rσ∨定義，因τ是σ∨的一個析取支，故有MSRσ∨Mδ(S,τ)。由定理2有MSRσMδ(S,τ)。于是由假設(shè)當(dāng)且僅當(dāng)?shù)淖筮叧闪⒑投x16有Mδ(S,τ),x|=α。

表2 :Sσ的信息表

在原子信息集合AInf上進行更新的自動機是T=(Q,Σ,δ,S0)，若信息系統(tǒng)S是自動機T的終結(jié)狀態(tài)(終結(jié)信息系統(tǒng))，記在原子信息集合AInf上進行更新的自動機中的所有從S0到S的道路的集合為InfS。

定理5給定初始信息系統(tǒng)S0，給定終結(jié)信息系統(tǒng)S，則等價于InfS任意子集合的全體元素所形成的選擇范式的信息都是從S0到S的信息更新。

證明.任選道路τ∈InfS，由定義22的擴充可得δ(S0,τ)=S，因而MS0RτMδ(S0,τ)，即MS0RτMS。任取等價于InfS任意子集合的全體元素所形成的選擇范式的信息σ，由定理2和R的定義有MS0RσMS。故由定義15有信息σ是從S0到S的信息更新。 □

由定理3和定理5馬上得到：

定理6 給定初始信息系統(tǒng)S0，給定終結(jié)信息系統(tǒng)S，則T=(Q,Σ,δ,S0,S)可接受的語言LT都是從S0到S的信息更新。

5 信息系統(tǒng)及其更新的邏輯系統(tǒng)的模型檢測的復(fù)雜性：多項式時間

文[1]中給出了結(jié)論：模態(tài)邏輯模型檢測復(fù)雜性是多項式時間的。仿照這個結(jié)論的證明方法（論域個體標(biāo)記算法（[1]））得到下面的定理。

下面介紹自原子公式逐層而上給論域個體標(biāo)記算法。為了對合式公式φ進行模型檢測，我們對論域個體x標(biāo)記上由那些在論域個體x處為真的φ的子公式形成的集合。即對x標(biāo)記上{ψ|M,x|=ψ且ψ是φ的子公式}，記為label(x)={ψ|M,x|=ψ且ψ是φ的子公式}。我們從命題公式p開始：p∈label(x)當(dāng)且僅當(dāng)x∈[[p]]，(a,v)∈label(x)當(dāng)且僅當(dāng)f(x,a)=v。對于更復(fù)雜的合式公式，布爾型的合式公式如下標(biāo)記:如果ψlabel(x)，則?ψ∈label(x)；如果ψ1,ψ2∈label(x)，則ψ1∧ψ2∈label(x)。模態(tài)型的合式公式[R(B)]α（對于任意的R(B)∈{IND(B)}B?A∪{SIM(B)}B?A），如果對任意的xR(B)x′的x′都有α∈label(x′)則[R(B)]α∈label(x)。下文邏輯連接詞符號〈〉是[]的對偶符號，即是?[]?。

定理7信息系統(tǒng)的邏輯系統(tǒng)的模型檢測的復(fù)雜性是多項式時間的。

證明.模型檢測M,x|=φ（當(dāng)φ:=〈R(B)〉α?xí)r）的算法如下：

算法運行時間是：O(con(φ)×nodes(M)×nodes(M))。其中con(φ)是φ中的聯(lián)結(jié)詞的個數(shù)，nodes(M)是模型的論域個體數(shù)。con(φ)×nodes(M)× nodes(M)也是其他類型的合式公式模型檢測運行時間的上界。

最后一步以布爾方式聯(lián)結(jié)而成的公式φ的模型檢測的復(fù)雜性也是多項式時間的。因此，信息系統(tǒng)的邏輯系統(tǒng)的模型檢測的復(fù)雜性是多項式時間的。 □

為了給出信息更新邏輯系統(tǒng)的模型檢測的復(fù)雜性，我們給出由信息系統(tǒng)S0、論域個體xS0（加上標(biāo)為了區(qū)分來自不同信息系統(tǒng)的個體，在不引起混淆時也簡記為x）及合式公式φ而確定的有向圖GS0,x,φ=(Vφ,Eφ)的定義。

定義23 給定初始信息系統(tǒng)S0及論域個體xS0，歸納于合式公式φ的結(jié)構(gòu)定義一個由它們而確定的有向圖GS0,x,φ=(Vφ,Eφ)，Vφ和Eφ分別是頂點集合和有向邊集，不引起混淆時候簡記為Gφ或G：

注記8定義23通過原子信息合成的更新給不同模型中論域個體建立有向邊，通過R(B)后繼給相同模型中論域個體建立有向邊，從而給定初始信息系統(tǒng)S0及論域個體xS0，給定合式公式φ就形成一個有向圖。

自原子公式逐層而上給論域個體標(biāo)記，若MS,xS|=φ，則對xS標(biāo)記一個φ。為了對公式φ進行模型檢測，對xS標(biāo)記上{ψ|MS,xS|=ψ且ψ是φ的子公式}，記為label(xS)={ψ|MS,xS|=ψ且ψ是φ的子公式}。對于更新型的合式公式〈σ〉α，如果存在某個的的xSτ有α∈label(xSτ)則〈σ〉α∈label(xS)。其他公式標(biāo)記方法如定理7前面給出的標(biāo)記方式。

定理8信息更新邏輯系統(tǒng)的模型檢測的復(fù)雜性是多項式時間的。

證明.模型檢測MS,x|=〈σ〉α的算法如下

算法運行時間是：O(disjun(σ)×con(φ)×nodes(M)×nodes(M))。其中disjun(σ)是σ的析取支數(shù)，con(φ)是φ中的聯(lián)結(jié)詞的個數(shù)，nodes(M)是模型的論域個體數(shù)。這個運行時間有上界O(con(φ)×con(φ)×nodes(M)× nodes(M))，它也是其他類型的合式公式模型檢測運行時間的上界。因此，信息系統(tǒng)的更新的邏輯系統(tǒng)的模型檢測的復(fù)雜性是多項式時間的。

6 結(jié)束語

M.A.Khan和M.Banerjee在文[7]給出信息系統(tǒng)更新的邏輯系統(tǒng)。我們對信息系統(tǒng)的更新過程進一步研究，通過引入信息等價和將信息范式化，從范式中拆分出的原子信息而得到自動機的文字，從而建立了信息更新的自動機。然后利用自動機給出信息系統(tǒng)更新的刻畫，證明了帶有終結(jié)狀態(tài)的自動機T=(Q,Σ,δ,S0,Sf)的語言都是從S0到Sf的信息更新。我們本來還打算在這個信息系統(tǒng)更新的邏輯系統(tǒng)中加上信息更新的星算子，但是利用自動機理論發(fā)現(xiàn)這個星算子的引入是平凡的。接下來進一步的工作可以利用信息更新的自動機的語言對更新過程作形式推演，具體可以表現(xiàn)為建立類似于Hoare邏輯（[5]）的形式系統(tǒng)。在這個形式系統(tǒng)中，可以對{S0}σ{Sf}做形式推演。這正是我們提出信息系統(tǒng)更新的自動機的初衷和動力。最后利用自動機理論得到了信息系統(tǒng)及其更新邏輯系統(tǒng)的模型檢測的復(fù)雜性都是多項式時間的。

[1] P.Blackburn,J.F.van Benthem and F.Wolter(eds),2006,Handbook of Modal Logic, Amsterdam:Elsevier.

[2] S.Burris and H.P.Sankappanavar,1981,A Course in Universal Algebra,New York: Springer-Verlag.

[3] I.Duntsch,1997,“A logic for rough sets”,Theoretical Computer Science,179:427-436.

[4] D.Harel,J.TiurynandD.Kozen,2000,Dynamiclogic,Massachusetts:TheMITpress.

[5] C.A.R.Hoare,1985,Communicating Sequential Processes,New York:Springer.

[6] M.A.Khan and M.Banerjee,2009,“A logic for complete information systems”,in C. Sossai and G.Chemello(eds.),Symbolic and Quantitative Approaches to Reasoning with Uncertainty,Vol.5590,pp.829-840,Berlin:Springer Berlin Heidelberg.

[7] M.A.KhanandM.Banerjee,2011,“Logicsforinformationsystemsandtheirdynamic extensions”,ACM Transactions on Computational Logic(TOCL),12(4):29:1-29:36.

[8] M.Kondo,2005,“Algebraic approach to generalized rough sets”,Lecture Notes in Artificial Intelligence,3641:132-140.

[9] T.Y.Lin and Q.Liu,1994,“Rough approximate operators:Axiomatic rough set theory”,in W.Ziarko(ed.),Rough Sets,Fuzzy sets and Knowledge Discovery,pp.256-260,Berlin:Springer.

[10] G.L.Liu,2013,“Using one axiom to characterize rough set and fuzzy rough set approximations”,Information Sciences,223:285-296.

[11] G.L.LiuandW.Zhu,2008,“Thealgebraicstructuresofgeneralizedroughsettheory”, Information Sciences,178(21):4105-4113.

[12] Z.Pawlak,1981,“Information systems theoretical foundations”,Information systems, 6(3):205-218.

[13] Z.Pawlak,1982,“Rough sets”,International Journal of Computer and Information Sciences,11:341-356.

[14] Z.Pawlak,1991,RoughSets:TheoreticalAspectsofReasoningaboutData,TheNetherlands:Kluwer Academic Publishers.

[15] Y.Y.Yao,1998,“Constructive and algebraic methods of the theory of rough sets”, Information Sciences,109:21-47.

[16] 陶仁驥，自動機引論，1986年，北京：科學(xué)出版社。

[17] 祝峰，何華燦，“粗集的公理化”，計算機學(xué)報，2000年第23卷第3期，第330-333頁。

（責(zé)任編輯：何健坤）

Automata of Update for Information Systems

Fasheng Cao
Institute of Logic and Cognition,Sun Yat-sen University
caofasheng@163.com

By defining the concepts of information equivalence and normal form,automata of update for information systems is presented.The model of update for information systems is characterized by automata theory.It is proved that it is not necessary to add the iteration operator to the logic system of update for information systems.Then,we obtain the connection with update for information systems and its automata.Finally, the model checking complexities of update for information systems are studied by the automata theory of information system and update logic system.

B81

A

1674-3202(2015)-01-0079-16

2014-12-05