直覺主義計(jì)算樹邏輯中的安全性和活性*

鮑秋霜，張晉津

1.南京航空航天大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，南京 210016

2.南京審計(jì)學(xué)院 計(jì)算機(jī)科學(xué)與技術(shù)系，南京 211815

直覺主義計(jì)算樹邏輯中的安全性和活性*

鮑秋霜1+，張晉津2

1.南京航空航天大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，南京 210016

2.南京審計(jì)學(xué)院 計(jì)算機(jī)科學(xué)與技術(shù)系，南京 211815

BAO Qiushuang,ZHANG Jinjin.Safety and liveness in intuitionistic computing tree logic.Journal of Frontiers of Computer Science and Technology,2016,10(2)：163-172.

將Patrick Maier關(guān)于直覺主義線性時(shí)序邏輯的研究擴(kuò)展到計(jì)算樹邏輯中，基于完全樹和非完全樹構(gòu)成的集合提出了一種直覺主義解釋的計(jì)算樹邏輯，并在此邏輯框架中研究了安全性和活性及其相關(guān)性質(zhì)。比較了經(jīng)典計(jì)算樹邏輯與直覺主義計(jì)算樹邏輯的表達(dá)能力，探究了直覺主義計(jì)算樹邏輯中安全性和活性在并、交等操作下的封閉性以及與經(jīng)典計(jì)算樹邏輯中安全性和活性的關(guān)系，并為直覺主義計(jì)算樹邏輯公式建立了分解定理。

直覺主義；計(jì)算樹邏輯；安全性；活性；分解定理

1　引言

反應(yīng)式系統(tǒng)（reactive system）是能對(duì)外界事件做出反應(yīng)的系統(tǒng)，其特點(diǎn)是系統(tǒng)持續(xù)與所在環(huán)境進(jìn)行交互。理論上，反應(yīng)式系統(tǒng)中的有限行為都可以轉(zhuǎn)換成無限行為[1]，并使用時(shí)序邏輯描述相關(guān)性質(zhì)。運(yùn)行時(shí)驗(yàn)證是一種輕量級(jí)程序驗(yàn)證技術(shù)，運(yùn)行時(shí)驗(yàn)證需要根據(jù)系統(tǒng)當(dāng)前運(yùn)行軌跡判定系統(tǒng)是否滿足給定性質(zhì)，因此需要研究系統(tǒng)的有限行為[1]。

為了使用時(shí)序邏輯規(guī)范系統(tǒng)的有限行為，學(xué)術(shù)界提出了多種不同方法。例如，Pnueli等人在時(shí)序邏輯中加入強(qiáng)next操作符和弱next操作符，并在有限行為和無限行為上對(duì)其給予不同解釋[2]。Eisner等人通過強(qiáng)、弱兩種語義解釋時(shí)序公式，其在有限行為和無限行為上的解釋也是不同的[3]。Maier基于有限和無限行為的前綴封閉集合解釋時(shí)序公式，并統(tǒng)一處理有限和無限行為[4]。

在時(shí)序驗(yàn)證中，很多驗(yàn)證方法只適用于安全性（safety）或活性（liveness），而分解定理表明每一個(gè)性質(zhì)都可以分解成安全性和活性的交，這極大地拓展了這些驗(yàn)證方法的適用范圍[4]。學(xué)術(shù)界在不同系統(tǒng)中就安全性、活性及分解定理進(jìn)行了深入研究。其中，Lamport最早非形式化地提出安全性和活性的概念[5]，Alpern和Schneider對(duì)安全性和活性進(jìn)行了嚴(yán)格的形式化定義且建立了分解定理[6]，并將工作擴(kuò)展到Buchi自動(dòng)機(jī)定義的ω正則語言上[7]。Manolios和Trefler則將安全性和活性概念引入到分叉時(shí)序框架中[8]，通過兩個(gè)閉包操作符定義了4種類型的性質(zhì)：存在型安全性、全局安全性、存在型活性和全局活性，基于模格給出了安全性和活性的抽象定義并建立了分解定理[9-10]。除經(jīng)典框架下的研究外，Maier將安全性和活性的概念擴(kuò)展到直覺主義線性時(shí)序邏輯（intuitionistic linear time logic，ILTL）中[4]，張文輝等人在此基礎(chǔ)上進(jìn)一步對(duì)直覺主義線性 μ演算（intuitionistic linear time μ-calculus,IμTL）開展了相關(guān)研究[11]。

本文借鑒Manolios和Trefler在分叉框架中的工作，將Maier關(guān)于ILTL的研究擴(kuò)展到計(jì)算樹邏輯（computing tree logic，CTL）中，在樹的前綴封閉集合形成的Heyting代數(shù)中解釋CTL操作符，提出了一種基于直覺主義解釋的計(jì)算樹邏輯（intuitionistic computing tree logic，ICTL）。本文將比較CTL和ICTL的表達(dá)能力，并在ICTL語義框架下定義安全性和活性，并證明相應(yīng)的分解定理。

本文組織結(jié)構(gòu)如下：第2章介紹樹的鏈接操作、前綴子樹的定義以及CTL公式的經(jīng)典語義；第3章引入CTL的直覺主義語義，并比較CTL和ICTL的表達(dá)能力；第4章在直覺主義語義下定義安全性和活性，建立分解定理，并比較經(jīng)典安全性和活性與直覺主義安全性和活性的關(guān)系；第5章總結(jié)全文。

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

本文采用如下一些記號(hào)：N表示自然數(shù)集合；P(S)表示集合S的冪集；R|S被稱為二元關(guān)系R左限制于集合S，即；S*和Sω分別表示集合S中的元素組成的有限和無限序列的集合，令S∞=S*?Sω。對(duì)u,v∈S∞，按通常方法定義u是v的前綴（記作u≤v）以及真前綴（記作u＜v）概念，并用u(i)表示序列u的第i+1個(gè)元素。若U?S∞且對(duì)所有u∈U，v≤u蘊(yùn)涵v∈U，則稱U為一個(gè)前綴封閉集合。

無標(biāo)記樹是N*的一個(gè)前綴封閉子集。帶標(biāo)記樹t是一個(gè)二元組＜T,τ＞，其中T是無標(biāo)記樹，τ:T→Σ，此處 Σ表示一個(gè)非空字符集合。如果T≠?，并且對(duì)所有u∈T，都存在v∈T使得u＜v，那么樹t被稱為完全樹。本文用Atot和Ant分別表示完全樹和非完全樹的集合。對(duì)任意樹t=＜T,τ＞，如果存在一個(gè)自然數(shù)n∈N，使得對(duì)所有u∈T，有#u≤n，那么該樹被稱為有限深度樹。有限深度樹的集合用Af表示，易見Af?Ant。Aall表示所有樹的集合，即Aall=Atot?Ant。下面回顧樹的葉子節(jié)點(diǎn)、鏈接操作、前綴樹以及閉包函數(shù)等概念。

定義1[7]（樹的葉子節(jié)點(diǎn)、鏈接操作以及前綴子樹）給定樹t1=＜T1,τ1＞和t2=＜T2,τ2＞，樹的葉子節(jié)點(diǎn)、鏈接操作以及前綴子樹定義如下：

（1）如果u∈T1并且不存在v∈T1使得u＜v，那么稱u是t1的一個(gè)葉子節(jié)點(diǎn)，記作leaf(u,t1)。

（2）樹t1和t2的鏈接t1t2定義為，其中τ′=τ2|T′，T′={v∈T2|v∈T1或存在u∈T1,leaf(u,t1)且u＜v}。

（3）如果存在一棵樹t=＜T,τ＞使得t1t=t2，那么稱樹t1為t2的一個(gè)前綴子樹，記作。

例1圖1、圖2給出兩棵樹t1、t2及其鏈接t1t2，易知t1是t1t2的前綴子樹。為方便起見，圖中只給出樹的節(jié)點(diǎn)，未給出節(jié)點(diǎn)上的標(biāo)記。

定義2[10]（閉包函數(shù)、拓?fù)溟]包函數(shù)）如果函數(shù)C:P(Aall)→P(Aall)滿足如下3個(gè)條件，那么該函數(shù)被稱為Aall上的一個(gè)閉包函數(shù)，對(duì)所有p,q∈P(Aall)：

（1）p?C(p)；

（2）C(p)=C(C(p))；

（3）如果p?q，那么C(p)?C(q)。

進(jìn)而，如果C:P(Aall)→P(Aall)滿足如下兩個(gè)條件，那么該函數(shù)被稱為一個(gè)拓?fù)溟]包函數(shù)：

（4）C(?)=?；

（5）對(duì)于所有p∈P(Aall)和q∈P(Aall)，有C(p?q)= C(p)?C(q)。

計(jì)算樹邏輯CTL有兩種類型的公式：狀態(tài)公式φ和路徑公式θ。CTL公式是所有狀態(tài)公式φ的集合，其定義如下：

其中p是原子命題公式。

對(duì)于CTL公式φ和ψ，公式φ?ψ是公式(φ→ψ)∧(ψ→φ)的縮寫。CTL公式中操作符的結(jié)合能力從強(qiáng)到弱依次為：最強(qiáng)為一元操作符、X、F、G，其次為二元操作符U、W，最弱為∧、∨、→、?。如果一個(gè)公式不含蘊(yùn)含詞和等值詞，并且否定詞只作用于原子命題公式上，那么該公式稱為具有否定范式（negation normal form,NNF）形式。

定義3（函數(shù)tot） L為P(Aall)中任意元素，函數(shù)tot:P(Aall)→P(Atot)定義為：

將函數(shù) tot的值域記作 TOT，易知 TOT= P(Atot)。且是一個(gè)完備的布爾代數(shù)，其中一元運(yùn)算表示補(bǔ)，即。

函數(shù)Modc:Φ→TOT把CTL公式解釋到布爾代數(shù)上[10]，Modc(φ)表示滿足公式φ的完全樹的集合。Modc歸納定義見圖3。該定義使用了如下幾個(gè)函數(shù)：

Fig.1　Treet1andt2圖1　樹t1和t2

Fig.2　Concatnation oft1andt2圖2　樹t1和t2的鏈接t1t2

Fig.3　Classical semantic of CTL圖3　CTL公式的經(jīng)典語義解釋

其中tσ表示以節(jié)點(diǎn)σ為根節(jié)點(diǎn)的t的子樹；#σ表示節(jié)點(diǎn)σ的長(zhǎng)度，#σ=1表明σ是根節(jié)點(diǎn)的直接子節(jié)點(diǎn)；S,S1,S2∈TOT。

3　CTL的直覺主義語義

下面參照LTL公式的直覺主義語義給出CTL公式的直覺主義語義，不同的是，該語義定義在樹的前綴封閉集合形成的Heyting代數(shù)上。

定義4（函數(shù) pref） L為P(Aall)中任意元素，函數(shù)pref:P(Aall)→P(Aall)定義如下：

將函數(shù)pref的值域記作PREF，易知該函數(shù)是Aall上的閉包函數(shù)，且PREF是所有前綴封閉的樹的集合。易知 PREF=＜PREF,?,?,?pc,Aall,?＞是一個(gè)完備的Heyting代數(shù)[12]，即＜PREF,?,?,Aall,?＞構(gòu)成有界格，并且對(duì)任意L1,L2∈PREF，存在一個(gè)最大的L∈PREF使得L1?L?L2。L稱為L(zhǎng)1相對(duì)于L2的偽補(bǔ)元，記作 L1?pcL2。易證 L={t∈Aall|pref(t)?L1?L2}。

和經(jīng)典語義類似，本文將通過函數(shù)Modi:Φ→PREF把CTL公式解釋到Heyting代數(shù) PREF=上，見圖4。CTL的直覺主義語義定義使用如下幾個(gè)函數(shù)：

其中S,S1,S2∈PREF。

Fig.4　Intuitionistic semantic of CTL圖4　CTL公式的直覺主義解釋

根據(jù)圖4中公式的直覺主義解釋，可得到如下關(guān)于|=i性質(zhì)的命題。

命題1（|=i的性質(zhì)）對(duì)于任意CTL公式φ和ψ，φ|=iψ當(dāng)且僅當(dāng)|=iφ→ψ。

上述命題容易證明。下文將比較CTL和ICTL的表達(dá)能力，即比較能夠由CTL中的公式和ICTL中的公式描述的樹的集合。由于CTL和ICTL公式分別在不同的代數(shù)上進(jìn)行解釋，不能直接比較其表達(dá)能力。本文將通過上面定義的映射tot:P(Aall)→TOT和 pref:P(Aall)→PREF進(jìn)行轉(zhuǎn)換，從而比較CTL和ICTL的表達(dá)能力。

首先通過函數(shù)tot把直覺主義語義投影到完全樹集合上，在完全樹集合所形成的布爾代數(shù)TOT中比較CTL和ICTL的表達(dá)能力。命題2是關(guān)于和 untilnext操作符的性質(zhì)。

命題2如果φ、ψ是兩個(gè)否定范式，n為任意自然數(shù)，則：

證明關(guān)于自然數(shù)n歸納易證。□

命題3如果φ是一個(gè)否定范式，則Modc(φ)= tot(Modi(φ))。

證明 按照公式φ的結(jié)構(gòu)復(fù)雜度歸納證明，當(dāng)φ形如T、⊥、p或φ1∨φ2時(shí)，容易證明。下面考慮?φ以及公式中含有模態(tài)詞的情形。

4　安全性和活性

本文將在直覺主義語義下引入安全性和活性的概念，建立分解定理，并探究經(jīng)典安全性和活性與直覺主義語義下安全性和活性的關(guān)系。與Manolios和Trefler在完全樹集合所形成的布爾代數(shù)中定義安全性和活性不同[7]，本文將在樹的前綴封閉集合所形成的Heyting代數(shù)中定義安全性和活性。

5　總結(jié)

本文提出了計(jì)算樹邏輯的一個(gè)直覺主義變種ICTL，該邏輯定義在樹的前綴封閉集合所形成的Heyting代數(shù)上，可用來描述和研究運(yùn)行時(shí)驗(yàn)證中的有限行為及其相關(guān)性質(zhì)。本文比較了CTL和ICTL的表達(dá)能力，在ICTL中引入了安全性和活性的概念，探究了安全性和活性在邏輯操作下的封閉性，并建立了分解定理。與Manolios和Trefler在完全樹集合形成的布爾代數(shù)上定義安全性和活性不同[8]，本文在樹的前綴封閉集合形成的Heyting代數(shù)上探究相關(guān)性質(zhì)。張文輝等人將Maier關(guān)于直覺主義線性時(shí)序邏輯的研究擴(kuò)展到了線性μ-演算框架下，但他們并沒有研究分解定理，也沒有探究經(jīng)典性質(zhì)和直覺主義性質(zhì)的關(guān)系[10-11]。

由本文、文獻(xiàn)[10]以及文獻(xiàn)[13]結(jié)果可知，在ICTL、ILTL以及LTL中，每個(gè)公式表達(dá)的性質(zhì)都滿足安全性-活性分解定理，并且這些安全性和活性也可由相應(yīng)公式表示，這一性質(zhì)將在時(shí)序驗(yàn)證中發(fā)揮重要作用。但CTL是否同樣具有這種性質(zhì)有待進(jìn)一步研究。此外，經(jīng)典時(shí)序邏輯作為一種便于描述反應(yīng)式系統(tǒng)的形式體系，也常應(yīng)用于博弈論中，例如使用時(shí)序邏輯公式刻畫玩家目標(biāo)[14-15]，但目前直覺主義時(shí)序邏輯在博弈論中的應(yīng)用仍有待探究。

References:

[1]Colin S,Mariani L.Run-time verification[C]//LNCS 3472: Model-Based Testing of Reactive Systems.Berlin,Heidelberg:Springer,2005:525-555.

[2]Lichtenstein O,Pnueli A,Zuck L.The glory of the past[C]// LNCS 193:Proceedings of the Workshop on Logic of Programs,Brooklyn,Jun 17-19,1985.Berlin,Heidelberg:Springer,1985:196-218.

[3]Eisner C,Fisman D,Havlicak J,et al.Reasoning with temporal logic on truncated paths[C]//LNCS 2725:Proceedings of the 15th International Conference on Computer Aided Verification,Boulder,USA,Jul 8-12,2003.Berlin,Heidelberg:Springer,2003:27-39.

[4]Maier P.Intuitionistic LTL and a new characterization of safety and liveness[C]//LNCS 3210:Proceedings of the 13th Annual Conference of the Computer Science Logic,Karpacz,Poland,Sep 20-24,2004.Berlin,Heidelberg:Springer, 2004:295-309.

[5]Lamport L.Proving the correctness of multiprocess programs[J].IEEE Transactions on Software Engineering, 1977,SE-3(2):125-143.

[6]Alpern B,Schneider F B.Defining liveness[J].Information Processing Letters,1985,21(4):181-185.

[7]Alpern B,Schneider F B.Recognizing safety and liveness[J]. Distributed Computing,1987,2(3):117-126.

[8]Manolios P,Trefler R.Safety and liveness in branching time [C]//Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science,Boston,USA,2001.Piscataway,USA:IEEE,2001:366-374.

[9]Manolios P,Trefler R.A lattice-theoretic characterization of safety and livenes[C]//Proceedings of the 22nd ACM Symposium on Principles of Distributed Computing,Boston, USA,Jul 13-16,2003.New York,USA:ACM,2003:325-333.

[10]Gumm H P.Another glance at the Alpern-Schneider characterization of safety and liveness in concurrent executions[J]. Information Processing Letters,1993,47(6):291-294.

[11]Kazmi S A R,Zhang Wenhui.Intuitionistic linear-time μcalculus[J].Journal of Software,2008,19(12):3122-3133.

[12]Rutherford D E.Introduction to lattice theory[M].New York:Hafner Publishing Co,1965.

[13]Maretic G P,Dashti M T,Basin D.LTL is closed under topological closure[J].Information Processing Letters,2014, 114(8):408-413.

[14]Gutierrez J,Harrenstein P,Wooldridge M.Reasoning about equilibria in game-like concurrent systems[C]//Proceedings of the 14th International Conference on Principles of Knowledge Representation and Reasoning.Menlo Park,USA: AAAI,2014:408-417.

[15]Gutierrez J,Harrenstein P,Wooldridge M.Iterated Boolean games[J].Information and Computation,2015,242:53-79.

BAO Qiushuang was born in 1990.She is an M.S.candidate at Nanjing University of Aeronautics and Astronautics.Her research interests include process algebra and logics in computer science,etc.

鮑秋霜（1990—），女，山東菏澤人，南京航空航天大學(xué)碩士研究生，主要研究領(lǐng)域?yàn)檫M(jìn)程代數(shù)，計(jì)算機(jī)科學(xué)中的邏輯學(xué)等。

張晉津（1981—），男，山西曲沃人，2011年于南京航空航天大學(xué)獲得博士學(xué)位，現(xiàn)為南京審計(jì)學(xué)院計(jì)算機(jī)科學(xué)系講師，主要研究領(lǐng)域?yàn)樾问交绞剑?jì)算機(jī)科學(xué)中的邏輯學(xué)等。

Safety and Liveness in Intuitionistic Computing Tree Logic*

BAO Qiushuang1+,ZHANG Jinjin2
1.College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016,China
2.Department of Computer Science and Technology,NanjingAudit University,Nanjing 211815,China
+Corresponding author:E-mail:baoqiushuangnuaa@163.com

This paper makes an extension from the intuitionistic linear time logic of Patrick Maier to computation tree logic,proposes an intuitionistic computation tree logic based on the set constructed by total and non-total tree, and considers safety and livenss in this intuitionistic computation tree logic.This paper also compares the expressive power between classical computation tree logic and intuitionistic computation tree logic,explores some properties of safety and liveness in intuitionistic computation tree logic under disjunction and conjunction,and discusses the relationship between intuitionistic computation tree logic and classical computation tree logic.Besides,this paper builds the decomposition theorem for formulas of intuitionistic computation tree logic.

intuitionistic;computation tree logic;safety;liveness;decompositiontheorem

2015-06,Accepted 2015-09.

ZHANG Jinjin was born in 1981.He the Ph.D.degree from Nanjing University of Aeronautics and Astronautics in 2011.Now he is a lecturer at Nanjing Audit University.His research interests include formal methods and logic in computer science,etc.

10.3778/j.issn.1673-9418.1506009

*The National Natural Science Foundations of China under Grant Nos.11426136,60973045(國(guó)家自然科學(xué)基金);the Natural Science Foundation of Jiangsu Higher Education Institutions under Grant No.13KJB520012(江蘇省高校自然科學(xué)基金).

CNKI網(wǎng)絡(luò)優(yōu)先出版：2015-09-16,http://www.cnki.net/kcms/detail/11.5602.TP.20150916.1059.004.html

A

TP301