LTL 性質(zhì)的可監(jiān)視性

王偉芳，樊麗麗，李寶鳳，趙光峰

（唐山師范學(xué)院 數(shù)學(xué)與計(jì)算科學(xué)學(xué)院，河北 唐山 063000）

可監(jiān)視性質(zhì)的形式定義由Pnuel 和Zaks 首次提出[1]，是指通過(guò)對(duì)系統(tǒng)動(dòng)作的觀察，就可以判斷它的任何繼續(xù)是否屬于一個(gè)形式化準(zhǔn)述的語(yǔ)言。在過(guò)去幾年里，一些作者也研究了 正則語(yǔ)言的可監(jiān)視性并給出了幾種構(gòu)造監(jiān)視器的方法，還有一些學(xué)者用LTL3來(lái)研究LTL的可監(jiān)視性[2-5]。本文從LTL的語(yǔ)義和可監(jiān)視的定義出發(fā)，證明LTL性質(zhì)的可監(jiān)視性。

1 符號(hào)說(shuō)明

∑ω的子集稱為性質(zhì)（語(yǔ)言）。如果L是無(wú)限單詞的語(yǔ)言，則Lc表示它的補(bǔ)集，即Lc=∑ωL。

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

由拓?fù)鋵W(xué)知識(shí)，很容易給出∑ω上的一個(gè)拓?fù)浠缦拢?/p>

可以證明這個(gè)子集族生成拓?fù)?/p>

在這個(gè)拓?fù)淇臻g，L是安全性質(zhì)[7-9]當(dāng)且僅當(dāng)L是閉集，L是余安全性質(zhì)當(dāng)且僅當(dāng)L是開集。

定義1令L是拓?fù)淇臻g∑ω的子集。

——若集合L是閉集，則稱L是安全集；

——若集合L是開集，則稱L是余安全集。

定義2令L是拓?fù)淇臻g∑ω的子集。若?x∈∑ω，?p＜x，都存在非空開集V?p∑ω，使得V?L或V?Lc，則稱L可監(jiān)視。

因?yàn)榇嬖贐V={p∑ω|p∈∑*}，非空開集所以，V可以由基本開集B=q∑ω,p≤q來(lái)代替。

由文獻(xiàn)[2]不難得到以下命題：

命題1可監(jiān)視性質(zhì)在有限交，有限并和補(bǔ)下封閉。

命題2開集和閉集可監(jiān)視。

命題3L可監(jiān)視當(dāng)且L的邊界有空的內(nèi)部。

定義3（LTL的語(yǔ)法[10]）原子命題集合AP上的LTL公式根據(jù)下述語(yǔ)法形成：

其中a∈AP。

定義LTL經(jīng)常使用的公式如下：

在本文中，令∑=2AP表示AP的冪集，并且把看做AP的任一包含的子集。

定義4（LTL的語(yǔ)義[10]）令φ是AP上的LTL公式，由φ誘導(dǎo)的性質(zhì)為：

其中，滿足關(guān)系|=?∑ω×LTL是具有表1 所示性質(zhì)的最小關(guān)系。由LTL公式誘導(dǎo)的性質(zhì)（語(yǔ)言）稱為L(zhǎng)TL性質(zhì)（語(yǔ)言）。

表1 無(wú)限單詞的LTL 語(yǔ)義

定義5（安全/余安全公式）[7]公式φ∈LTL稱為一個(gè)安全（余安全）公式，若L（φ）是一個(gè)安全（余安全）性質(zhì)。

3 LTL 性質(zhì)的可監(jiān)視性

定理1L（ture）可監(jiān)視。

證明由于L（ture）=∑ω是拓?fù)淇臻g中的既開又閉的集合，因此可監(jiān)視。

定理2若a∈AP，則L（a）可監(jiān)視。

證明由于，因此L（a）可監(jiān)視。

由于L（﹁φ）=L（φ）c，并且可監(jiān)視性在補(bǔ)下封閉，因此有：

定理 3對(duì)于φ∈LTL,L（φ）可監(jiān)視當(dāng)且僅當(dāng)L（﹁φ）可監(jiān)視。

由于L（φ1∨φ2）=L（φ1）∪L（φ2），并且可監(jiān)視性在有限并下封閉，可得：

定理4對(duì)于φ1,φ2∈LTL，若L（φ1）和L（φ2）可監(jiān)視，則L（φ1∨φ2）可監(jiān)視。

由于

所以有：

定理5對(duì)于φ∈LTL，L（φ）可監(jiān)視當(dāng)且僅當(dāng)L（○φ）可監(jiān)視。

證明" ?"?x∈∑ω，x=A0A1A2...=A0.z，其中A0∈∑,z=A1A2...∈∑ω，由于L（φ）可監(jiān)視，對(duì)z∈∑ω，?q=A1A2…Ak＜z（k≥1），（則p=A0.q可以是x的長(zhǎng)度≥ 2的任意前綴），存在非空開集

（則A0.V?p∑ω）使得V?L（φ）或V?L（φ）c。因此，非空開 集A0.V?∑.L（φ）或A0.V?∑.L（φ）c即A0.V?L（○φ）或A0.V?L（○φ）c。

" ? "反證法。假 設(shè)L（φ）不可監(jiān) 視，則?y∈∑ω,?p＜y，對(duì)任意非空開集V?p∑ω，都有V∩L（φ）≠?并且V∩L（φ）c≠?。對(duì)任意A∈∑，令x=A.y，則A.p＜A.y,?A.V?A.p∑ω，有A.V∩∑.L（φ）≠?并 且A.V∩∑.L（φ）c≠?，即A.V∩L（○φ）≠?并 且A.V∩L（○φ）c≠?，從而，L（○φ）不可監(jiān)視。矛盾。

從上述定理，易得如下推論：

推論1對(duì)給定的i∈N+和φ∈LTL，L（φ）可監(jiān)視當(dāng)且僅當(dāng)L（○iφ）可監(jiān)視。

前面已證，LTL公式的可監(jiān)視性在取非、有限析取、有限合取和下一步算子下封閉。但是，在直到算子下不封閉，反例如下：

例1設(shè)AP={a},∑=2AP=｛｛a｝,?｝。

φ1=true,φ2=﹁(ture∪a)，則L（φ1）,L（φ2）可監(jiān)視，然而L（φ1∪φ2）不可監(jiān)視。

由于

下面說(shuō)明φ1∪φ2不可監(jiān)視。注意到

令ψ=□ ◇a（無(wú)限次出現(xiàn)a）。由于

并且

因此L（ψ）不可監(jiān)視，從而L（φ1∪φ2）不可監(jiān)視。

上例中，φ1,φ2都是安全公式，即便如此，也不能保證φ1∪φ2可監(jiān)視。如果它們都是余安全的，有：

定理6對(duì)φ1,φ2∈LTL，如果φ1,φ2都是余安全的，則L（φ1∪φ2）可監(jiān)視。

證明由于

而φ1,φ2都是余安全的，L（φ1）,L（φ2）都是開集，從而L（○iφ1）,L（○jφ2）是開集，進(jìn)一步L（φ1∪φ2）是開集從而可監(jiān)視。

定理7對(duì)φ1,φ2∈LTL，如果L（φ1）,L（φ2）可監(jiān)視，則L（φ1∪kφ2）可監(jiān)視。

其中φ1∪kφ2是φ1∪φ2的有界變體，它表示恰好在第k步φ2成立，在此之前φ1一直成立。

證明注意到

由于L（φ1）和L（φ2）可監(jiān)視，由推論 1，可知L（○iφ1）和L（○kφ2），因此L（φ1∪kφ2）可監(jiān)視。

推論2對(duì)φ1,φ2∈LTL，如果L（φ1）,L（φ2）可監(jiān)視，則L（φ1∪≤kφ2）可監(jiān)視。

其中φ1∪≤kφ2表示在k步之內(nèi)φ2成立，在此之前φ1一直成立。

證明由可得。

4 結(jié)論

利用LTL公式的語(yǔ)義和可監(jiān)視的定義證明了LTL性質(zhì)的可監(jiān)視性，進(jìn)一步證明了可監(jiān)視性在布爾連接詞析取∨、取非﹁和下一步○下封閉，在合取∧和○i下封閉，在直到∪算子下不封閉，在∪≤k下封閉。對(duì)時(shí)序算子∪，得到了保證φ1∪φ2可監(jiān)視的幾個(gè)充分條件，φ1∪φ2可監(jiān)視的充要條件有待進(jìn)一步研究。