LTL 性質的可監視性

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

（唐山師范學院 數學與計算科學學院，河北 唐山 063000）

可監視性質的形式定義由Pnuel 和Zaks 首次提出[1]，是指通過對系統動作的觀察，就可以判斷它的任何繼續是否屬于一個形式化準述的語言。在過去幾年里，一些作者也研究了 正則語言的可監視性并給出了幾種構造監視器的方法，還有一些學者用LTL3來研究LTL的可監視性[2-5]。本文從LTL的語義和可監視的定義出發，證明LTL性質的可監視性。

1 符號說明

∑ω的子集稱為性質（語言）。如果L是無限單詞的語言，則Lc表示它的補集，即Lc=∑ωL。

2 預備知識

由拓撲學知識，很容易給出∑ω上的一個拓撲基如下：

可以證明這個子集族生成拓撲

在這個拓撲空間，L是安全性質[7-9]當且僅當L是閉集，L是余安全性質當且僅當L是開集。

定義1令L是拓撲空間∑ω的子集。

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

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

定義2令L是拓撲空間∑ω的子集。若?x∈∑ω，?p＜x，都存在非空開集V?p∑ω，使得V?L或V?Lc，則稱L可監視。

因為存在BV={p∑ω|p∈∑*}，非空開集所以，V可以由基本開集B=q∑ω,p≤q來代替。

由文獻[2]不難得到以下命題：

命題1可監視性質在有限交，有限并和補下封閉。

命題2開集和閉集可監視。

命題3L可監視當且L的邊界有空的內部。

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

其中a∈AP。

定義LTL經常使用的公式如下：

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

定義4（LTL的語義[10]）令φ是AP上的LTL公式，由φ誘導的性質為：

其中，滿足關系|=?∑ω×LTL是具有表1 所示性質的最小關系。由LTL公式誘導的性質（語言）稱為LTL性質（語言）。

表1 無限單詞的LTL 語義

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

3 LTL 性質的可監視性

定理1L（ture）可監視。

證明由于L（ture）=∑ω是拓撲空間中的既開又閉的集合，因此可監視。

定理2若a∈AP，則L（a）可監視。

證明由于，因此L（a）可監視。

由于L（﹁φ）=L（φ）c，并且可監視性在補下封閉，因此有：

定理 3對于φ∈LTL,L（φ）可監視當且僅當L（﹁φ）可監視。

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

定理4對于φ1,φ2∈LTL，若L（φ1）和L（φ2）可監視，則L（φ1∨φ2）可監視。

由于

所以有：

定理5對于φ∈LTL，L（φ）可監視當且僅當L（○φ）可監視。

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

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

" ? "反證法。假 設L（φ）不可監 視，則?y∈∑ω,?p＜y，對任意非空開集V?p∑ω，都有V∩L（φ）≠?并且V∩L（φ）c≠?。對任意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（○φ）不可監視。矛盾。

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

推論1對給定的i∈N+和φ∈LTL，L（φ）可監視當且僅當L（○iφ）可監視。

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

例1設AP={a},∑=2AP=｛｛a｝,?｝。

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

由于

下面說明φ1∪φ2不可監視。注意到

令ψ=□ ◇a（無限次出現a）。由于

并且

因此L（ψ）不可監視，從而L（φ1∪φ2）不可監視。

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

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

證明由于

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

定理7對φ1,φ2∈LTL，如果L（φ1）,L（φ2）可監視，則L（φ1∪kφ2）可監視。

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

證明注意到

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

推論2對φ1,φ2∈LTL，如果L（φ1）,L（φ2）可監視，則L（φ1∪≤kφ2）可監視。

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

證明由可得。

4 結論

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