曹發(fā)生

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

caofasheng@163.com

信息系統(tǒng)更新的自動(dòng)機(jī)

曹發(fā)生

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

caofasheng@163.com

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

信息系統(tǒng)；動(dòng)態(tài)；自動(dòng)機(jī)；模型檢測(cè)

粗糙集理論中的知識(shí)表達(dá)方式（[12,13]）一般采用信息表或稱為信息系統(tǒng)的形式，對(duì)于粗糙集理論的邏輯推理系統(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)的可靠性和完全性。

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

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

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

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

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

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

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

注記1我們?cè)诒疚闹邢薅ˋ是屬性的非空有限集合。有這樣的限制，我們就可以研究信息系統(tǒng)模型檢測(cè)的復(fù)雜性；再者，計(jì)算機(jī)處理的信息系統(tǒng)知識(shí)庫都是有限屬性集合，所以這樣的限制是可行的。

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

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

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

“完全信息系統(tǒng)”與“信息系統(tǒng)”的本質(zhì)區(qū)別在于是否存在未知屬性值。在完全信息系統(tǒng)的粗糙集理論中的關(guān)系是等價(jià)關(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ù)符號(hào)，～，是一元函數(shù)符號(hào)，(a,v)是零元函數(shù)符號(hào)。

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

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

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

2.1 LIS的語法

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

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

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

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

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

(5)兩個(gè)常元符號(hào)?，⊥；

(6)變?cè)?hào)，用α，β，γ或加數(shù)字下標(biāo)表示；

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

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

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

(1)常元符號(hào)?，⊥，命題變?cè)?hào)，變?cè)?hào)是合式公式；

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

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

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

2.2 LIS的語義

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

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

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

(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)對(duì)于任意的R∈{IND(B)}B?A∪{SIM(B)}B?A，M,w|=[R]α當(dāng)且僅當(dāng)，對(duì)任意的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。

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

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

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

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

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

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

3.1 DLIS的語法

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

(1)L的字母表；

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

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

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

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

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

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

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

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

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

(1)常元符號(hào)?，⊥，命題變?cè)?hào)是合式公式；

(2)(a,v)是合式公式，也簡(jiǎn)記為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)是一個(gè)模型，定義由原子信息σ0=(α,a,v)更新模型M所得模型，或稱為M的σ0更新模型，記為

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

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

這個(gè)定義可以推廣到原子信息的合成上的更新信息系統(tǒng)M(σ1;σ2;...;σk):= ((((Mσ1)σ2)...)σk)，這對(duì)定理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′或者M(jìn)Rσ′M′。

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

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

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

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

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

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

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

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

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

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

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

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

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

引理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(jìn)′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。

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

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

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

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

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

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

有了這個(gè)定理，我們把信息等價(jià)的選擇范式的析取支簡(jiǎn)稱為信息的的析取支。

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

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

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

下面我們來給出由原子信息σ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時(shí)，fσ0(x,a):=v；

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

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

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

(1)S是Q的元素；

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

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

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

定義21給定初始信息系統(tǒng)S0，在原子信息集合AInf上進(jìn)行更新的自動(dòng)機(jī)是一組結(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上進(jìn)行更新的帶有終結(jié)狀態(tài)的自動(dòng)機(jī)是一組結(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)。

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

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

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

證明.由信息等價(jià)的定義知，要證σ;σ≡σ，只要證明出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σ?！跤谑荕Rσ;σM′，故Rσ;σ?Rσ。

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

例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可計(jì)算出更新系統(tǒng)Sσ=(W,A,V,fσ)，fσ如表2所示，同理可得Sσ;σ=Sσ。

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

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

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

表2 :Sσ的信息表

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

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

證明.任選道路τ∈InfS，由定義22的擴(kuò)充可得δ(S0,τ)=S，因而MS0RτMδ(S0,τ)，即MS0RτMS。任取等價(jià)于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)的模型檢測(cè)的復(fù)雜性：多項(xiàng)式時(shí)間

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

下面介紹自原子公式逐層而上給論域個(gè)體標(biāo)記算法。為了對(duì)合式公式φ進(jìn)行模型檢測(cè)，我們對(duì)論域個(gè)體x標(biāo)記上由那些在論域個(gè)體x處為真的φ的子公式形成的集合。即對(duì)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。對(duì)于更復(fù)雜的合式公式，布爾型的合式公式如下標(biāo)記:如果ψlabel(x)，則?ψ∈label(x)；如果ψ1,ψ2∈label(x)，則ψ1∧ψ2∈label(x)。模態(tài)型的合式公式[R(B)]α（對(duì)于任意的R(B)∈{IND(B)}B?A∪{SIM(B)}B?A），如果對(duì)任意的xR(B)x′的x′都有α∈label(x′)則[R(B)]α∈label(x)。下文邏輯連接詞符號(hào)〈〉是[]的對(duì)偶符號(hào)，即是?[]?。

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

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

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

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

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

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

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

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

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

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

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

6 結(jié)束語

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

[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] 陶仁驥，自動(dòng)機(jī)引論，1986年，北京：科學(xué)出版社。

[17] 祝峰，何華燦，“粗集的公理化”，計(jì)算機(jī)學(xué)報(bào)，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