張晉津，張 嚴，朱朝暉

(1.南京審計學院工學院，江蘇 南京 211815;2.南京航空航天大學計算機科學與技術學院，江蘇 南京 210016)

(η,α)-互模擬的分層及判定算法*

張晉津1，張 嚴2，朱朝暉2

(1.南京審計學院工學院，江蘇 南京 211815;2.南京航空航天大學計算機科學與技術學院，江蘇 南京 210016)

分層刻畫是傳統(tǒng)的互模擬概念研究中的一個重要內容，它為一些互模擬判定算法提供了理論基石。(η,α)-互模擬是一種帶折扣的近似互模擬概念，其定義蘊涵著一種折扣思想：在比較系統(tǒng)差異時，越晚出現(xiàn)的差異越不重要。為(η,α)-互模擬建立分層刻畫，將清晰地揭示這種折扣思想。此外，由于(η,α)-互模擬一般不是等價關系，所以傳統(tǒng)的互模擬判定算法中常用的最粗劃分方法不適用于(η,α)-互模擬的判定，基于(η,α)-互模擬的分層刻畫給出一種該互模擬的判定算法。還提供一個簡單的例子用于說明(η,α)-互模擬及其判定算法在描述實現(xiàn)與規(guī)范之間關系時的應用。

(η,α)-互模擬；分層；判定算法；折扣

1 引言

近年來，狀態(tài)或動作上附加定量信息的標記轉換系統(tǒng)LTS(Labelled Transition Systems)廣泛應用于描述通信系統(tǒng)[1]、控制系統(tǒng)[2,3]及實時系統(tǒng)[4]等。為了刻畫此類系統(tǒng)間的等價關系，學術界提出了許多近似等價概念，例如λ-互模擬[4]、δ-互模擬[3]、(η,α)-互模擬[5]等。這些概念在描述通信或軟件的可靠性[1,6]及控制系統(tǒng)形式化驗證與設計[2]方面發(fā)揮了重要作用。

眾所周知，互模擬概念可以通過多種不同方式加以刻畫，例如，可以通過模態(tài)邏輯、不動點、余代數(shù)及分層方式等給出等價的定義。其中，分層刻畫是一些傳統(tǒng)互模擬判定算法的理論基石[7]，是互模擬的一種重要刻畫方式。文獻[3,4]分別給出了δ-互模擬和λ-互模擬的分層刻畫方式。特別地，文獻[3]還基于δ-互模擬的分層刻畫給出了該互模擬的判定算法。

本文將建立(η,α)-互模擬的分層刻畫，并在此基礎上給出該互模擬的判定算法。(η,α)-互模擬中的α∈[0,1]是一個折扣因子，其定義帶有折扣思想。粗略地說，兩個狀態(tài)是(η,α)-互模擬的，當且僅當它們之間的差異不大于η并且它們下一刻到達的狀態(tài)是(η/α,α)-互模擬的。因此，當α小于1時，(η,α)-互模擬的兩個系統(tǒng)的狀態(tài)之間允許出現(xiàn)的差異隨著系統(tǒng)運行時間的增加而增大。換言之，越晚出現(xiàn)的差異越不重要。本文建立的(η,α)-互模擬分層刻畫將更為清晰地展示這種折扣思想。

2 (η,α)-互模擬

本節(jié)將回顧(η,α)-互模擬的若干相關定義和性質，這些定義與性質均出自文獻[5]。該互模擬概念的提出背景、有關性質及與相關概念的討論參見文獻[5]。在給出(η,α)-互模擬概念的定義之前，需要引入下面這個記號。

定義1 一個量化的轉換系統(tǒng)是一個四元組R=(S,P,→,[·])，其中S是一個狀態(tài)集合，P是一個有限命題集合，→?S×S是一個轉換關系，[·]:S→(P→[0,1])是一個賦值函數(shù)。

一個量化的轉換系統(tǒng)R=(S,P,→,[·])被稱為非死鎖的，當且僅當對于任意q∈S，{q′∈S:q→q′}是非空集合。一個量化的轉換系統(tǒng)R=(S,P,→,[·])被稱為有限分岔的，當且僅當對于任意q∈S,{q′∈S:q→q′}是一個有限集合。一個量化的轉換系統(tǒng)R=(S,P,→,[·])被稱為有限的，當且僅當集合S是有限的。

定義2 令α∈(0,1]并且D?[0,1]。我們稱集合D是α-封閉的，當且僅當對于任意的x∈D，都有fα(x)∈D。

定義3 令R=(S,P,→,[·])是一個量化的轉換系統(tǒng)并且α∈(0,1]。假設D(?[0,1])是α-封閉的。稱一個關系序列{Rλ?S×S:λ∈D}是一個α-折扣互模擬序列,當且僅當對于任意的λ∈D和q，q′∈S,如果(q,q′)∈Rλ，則:

(1λ) 對于任意的r∈P，都有|[q](r)-[q′](r)|≤λ；

下文將{Rλ?S×S:λ∈D}簡記為{Rλ}λ∈D。

定義4((η,α)-互模擬) 令R=(S,P,→,[·])是一個量化的轉換系統(tǒng)，α∈(0,1]并且η∈[0,1]。一個二元關系R?S×S被稱為是一個(η,α)-互模擬關系，當且僅當存在一個α-折扣互模擬序列{Rλ}λ∈D,使得η∈D并且Rη=R。定義(η,α)-互模擬～η,α如下：

我們稱兩個狀態(tài)q和q′是(η,α)-互模擬的,當且僅當q～η,αq′。

定理1 令R=(S,P,→,[·])是一個量化轉換系統(tǒng)，α∈(0,1]并且η∈[0,1]。對于任意的q，q′∈S,q～η,αq′，當且僅當q和q′滿足下列條件：

(iη) 對于任意的r∈P，|[q](r)-[q′](r)|≤η；

(1)對于任意的r∈P，都有|[q](r)-[q′](r)|≤η；

易見函數(shù)#η是一個單調函數(shù)。即，對于任意R?R′，#η(R)?#η(R′)成立。

命題1 對于任意量化轉換系統(tǒng)R，α∈(0,1]和η∈[0,1]，～η,α=#η(～fα(η),a)。

定義6 函數(shù)σ:(0,1]×[0,1]→w-{0}定義如下：

3 (η,α)-互模擬的分層

3.1 (η,α)-互模擬分層：任意框架情形

本小節(jié)將在任意量化的轉換系統(tǒng)框架下討論(η,α)-互模擬的分層。為此，定義如下關系序列：

假設κ=ζ+1并且η∈[0,1]。根據(jù)定義7、歸納假設和#η的單調性可得:

□

下面這個結果表明定義7可以為(η,α)-互模擬提供一種分層刻畫方式。

因此，由定義4可知，只需證明下面這個結論就可完成證明:

{Rλ}λ∈[0,1]是一個α-折扣互模擬序列。

□

3.2 (η,α)-互模擬分層：有限分岔或非死鎖情形

我們已經為任意量化的轉換系統(tǒng)框架下的(η,α)-互模擬給出了分層的刻畫方式。當量化轉換系統(tǒng)是有限分岔或者非死鎖時，可以得到更有趣的結果。下面將在此假設下討論(η,α)-互模擬的分層。首先，與經典互模擬相關結果類似，當量化的轉換系統(tǒng)是有限分岔時，(η,α)-互模擬的分層只需考慮ω層即可。

這個定理的證明類似于定理2，有興趣的讀者可以證明之。文獻[3,8]分別為δ-近似互模擬和λ-互模擬給出了類似的分層結果。

引理2 令R是一個非死鎖的量化轉換系統(tǒng)并且α∈(0, 1]，則～1,α=S×S。

證明 因為～1,α?S×S顯然成立，所以只需證明～1,α?S×S。令D={1}并且R1=S×S。顯然地，D是α-封閉的。進而，容易驗證{Rλ}λ∈D是一個α-折扣互模擬序列。因此，由定義4可知，S×S是一個(1,α)-互模擬關系并且～1,α?S×S。

□

定理4 令R是一個非死鎖的量化轉換系統(tǒng)并且α∈(0, 1)。對于任意的η∈[0,1]，都有:

□

4 折扣與(η,α)-互模擬判定算法

互模擬的判定算法是行為等價理論的一個重要研究內容[9,10]。由于(η,α)-互模擬一般不是等價關系，其判定問題不能歸結為最粗劃分問題(Coarsest Partition Problem)，所以不能采取傳統(tǒng)的互模擬判定方法[11]。本文將基于定理4提出判定算法。

Figure 1 Stratification of (η,α)-bisimilarity (Case of non-block QTS and α<1)

由上述論斷可知，對于非死鎖的量化轉換系統(tǒng)，當α<1時，判斷兩個狀態(tài)是否(η,α)-互模擬只需驗證這兩個狀態(tài)的σ(α,η)步以內的后繼狀態(tài)是否匹配。因此，如果該量化轉換系統(tǒng)同時也滿足有限分岔性質，則兩個狀態(tài)是否(η,α)-互模擬是可判定的。特別地，當該量化轉換系統(tǒng)是有限的，可以在有限步內計算得到(η,α)-互模擬的所有狀態(tài)。

針對有限非死鎖的量化轉換系統(tǒng)，下面給出(η,α)-互模擬判定算法：

算法1 (η,α)-互模擬判定算法

(1)InputR=(S,P,→,[·])、η、α

(2) Computeσ(α,η)

(3) leti=1,R1=S×S

(4) whilei≤σ(α,η) do{

(4) setS1to be the domain of the relationRi

(5) for allq1∈S1do{

(6) add (q1,q1) to relationRi+1;

(7) for allq2∈S1withq1≠q2do

(8) if for anyr∈P, |[q1](r)-[q2](r)|≤η/ασ(α,η)-i+1&Match(Ri,ReachSet(q1),ReachSet(q2)) &Match(Ri,ReachSet(q2),ReachSet(q1)) /*見算法2 */

(9) add (q1,q2) to relationRi+1}

(10)i=i+1}

(11) returnRi-1

在上述算法中涉及兩個函數(shù)：Match和ReachSet。ReachSet函數(shù)用于求得給定狀態(tài)的后續(xù)狀態(tài)集合，例如ReachSet(q)是狀態(tài)q所有一步可達狀態(tài)組成的集合。這個函數(shù)根據(jù)量化的轉換系統(tǒng)直接可得，在此不再贅述。Match函數(shù)用于判斷集合S1與S2中元素是否保持R關系，具體而言，如果對于S1中任意元素，均存在q2∈S2使得(q1,q2)∈R，則Match函數(shù)返回值true，否則返回false。Match函數(shù)算法如下：

算法2Match函數(shù)

Match(R,S1,S2)

(1)for allq1∈S1do{

(2) try to find an elementq2∈S2so that (q1,q2)∈R

(3) if suchq2does not exist

(4) return false}

(5)return true

根據(jù)定理4，可以驗證該算法是正確的。此外，容易驗證給定量化的轉換系統(tǒng)R=(S,P,→,[·])，該算法的時間復雜度為O(|S|4)。

5 (η,α)-互模擬的應用

下面將給出一個簡單的例子說明(η,α)-互模擬在實際應用中的作用。給定一個控制系統(tǒng)，其輸入電壓每100 ms可變化一次。圖2a給出了一個規(guī)范，要求該控制系統(tǒng)的輸入電壓滿足該規(guī)范。即，輸入電壓最初要求為0，在100 ms時可變化為1或0.5。若變化為1，則其后時間100*n(n>1)ms時刻保持為1或者變化為0.8，一旦變化為0.8，則之后都應保持為0.8。若100 ms時變化為0.5，則其后時間100*n(n>1)ms時刻保持為0.5或者變化為0.8或0.3，一旦變化為0.8或0.3，則之后都應保持為0.8或0.3。

由于物理設備本身存在誤差，所以實際實現(xiàn)的系統(tǒng)一般不能嚴格滿足該規(guī)范，進而需要允許一定誤差存在，設定允許誤差η=0.03。此外，由于系統(tǒng)運行初期可能不穩(wěn)定，因此嚴格要求輸入電壓的誤差不得超過規(guī)定值。隨著系統(tǒng)運行時間的增加，系統(tǒng)逐漸穩(wěn)定和適應環(huán)境，對輸入電壓的誤差限定逐漸放寬，即誤差限定可以打折扣。為此，設定折扣因子α=0.9。

Figure 2 Specification and its implementation

假設根據(jù)上述規(guī)范設計實現(xiàn)的一個輸入電壓變化系統(tǒng)如圖2b所示。顯然，當采用傳統(tǒng)互模擬概念刻畫實現(xiàn)與規(guī)范間滿足關系時，由于圖2b所示的實現(xiàn)與圖2a所示的規(guī)范不具有互模擬關系，因此視為該實現(xiàn)不滿足規(guī)范。事實上，由于物理設備誤差的存在，實現(xiàn)與規(guī)范都不能保持互模擬關系。所以，當采用傳統(tǒng)互模擬概念時，實現(xiàn)一般都不滿足規(guī)范。因此，采用傳統(tǒng)互模擬概念刻畫實現(xiàn)與規(guī)范間滿足關系是不恰當?shù)摹?/p>

根據(jù)上述關于規(guī)范滿足條件的描述，如果實現(xiàn)與規(guī)范是(η,α)-互模擬的，則可認為該實現(xiàn)滿足規(guī)范。由第4節(jié)提供的算法，容易驗證圖2b所示的實現(xiàn)與圖2a所示的規(guī)范是(η,α)-互模擬的。因此，可以認為該實現(xiàn)滿足給定規(guī)范。

6 結束語

(η,α)-互模擬是一種帶折扣的近似互模擬概念。本文為其建立了分層刻畫方式，清晰地展示了折扣的思想。這種分層刻畫又為(η,α)-互模擬的判定算法提供了理論基石。由于(η,α)-互模擬一般不是等價關系，無法采用傳統(tǒng)的最粗劃分方法，本文基于(η,α)-互模擬的分層刻畫為其提供了一種可用的判定算法。但是，該算法不是線性時間的，今后我們將進一步研究在哪些量化轉換系統(tǒng)框架下，可以給出線性時間的(η,α)-互模擬判定算法。

[1] Ying Ming-sheng. π-calculus with noisy channels [J]. Acta Informatica, 2005, 41(9):525-593.

[2] Girard A, Pappas G. Approximate bisimulation:A bridge between computer science and control theory [J]. European Journal of Control, 2011, 17(5):568-578.

[3] Girard A, Pappas G. Approximation metrics for discrete and continuous systems [J]. IEEE Transactions on Automatic Control, 2007, 52(5):782-798.

[4] Ying Ming-sheng. Bisimulation indexes and their applications [J]. Theoretical Computer Science, 2002, 275(1-2):1-68.

[5] Zhang Jin-jin, Zhu Zhao-hui. Characterize branching distance in terms of (η,α)-bisimilarity [J]. Information and Computation, 2008, 206(8):953-965.

[6] Cao Yong-zhi.Reliability of mobile processes with noisy channels [J]. IEEE Transaction on Computers, 2012, 61(9):1217-1230.

[8] Milner R.Communication and concurrency[M]. New York:Prentice Hall, 1989.

[9] Li Zhou-jun,Chen Huo-wang.Bisimulation checking algorithms based on symbolic transition graphs [J]. Computer Engineering & Science, 2002, 24(2):34-41.(in Chinese)

[10] Xu Wen,Fang Hai, Lin Hui-min. Optimization and implementation of a bisimulation checking algorithm for the π-calculus [J]. Journal of Software, 2001, 12(2):159-166. (in Chinese)

[11] Paige R,Tarjan R E, Bonic R. A linear time solution to the single function coarsest partition problem [J]. Theoretical Computer Science, 1985, 40(1):67-84.

附中文參考文獻：

[9] 李舟軍，陳火旺. 基于符號遷移圖的互模擬驗證算法 [J]. 計算機工程與科學, 2002, 24(2):34-41.

[10] 許文，方海，林慧民. π-演算互模擬判定算法的優(yōu)化和實現(xiàn) [J]. 軟件學報, 2001, 12(2):159-166.

ZHANG Jin-jin,born in 1981,PhD,lecturer，his research interests include formal methods, and logics in computer science.

張嚴(1983-),男，江蘇南通人，博士生，研究方向為形式化方法和計算機科學中的邏輯學。E-mail:yanzhang_nuaa@nuaa.edu.cn

ZHANG Yan,born in 1983,PhD candidate,his research interests include formal methods, and logics in computer science.

朱朝暉(1970-),男，江蘇南通人，博士，教授，研究方向為形式化方法和計算機科學中的邏輯學。E-mail:zhaohui.nuaa@gmail.com

ZHU Zhao-hui,born in 1970,PhD,professor,his research interests include formal methods, and logics in computer science.

Stratification and checking algorithm of (η,α)-bisimilarity

ZHANG Jin-jin1，ZHANG Yan2,ZHU Zhao-hui2

(1.School of Technology,Nanjing Audit University,Nanjing 211815;2.College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016,China)

The stratification of bisimilarity is an important issue in the classical research on bisimilarity. It provides a theoretical basis for some checking algorithms of bisimilarity. We establish the stratification of (η,α)-bisimilarity in this paper.(η,α)-bisimilarity is a notion of approximate bisimilarity with discount factor. It is defined with a discounted setting, which means that the difference occurring in the far away future is not as important as the difference occurring in the near future, which will be revealed in the stratification established in this paper. Moreover, since (η,α)-bisimilarity is not always an equivalence relation, the coarsest partition method used in classical checking algorithms of bisimilarity cannot be adopted to offer a checking algorithm of (η,α)-bisimilarity.Based on the stratification of (η,α)-bisimilarity, we provide a checking algorithm of this bisimilarity.We also offer a simple example to illustrate how to apply (η,α)-bisimilarity and its checking algorithm to capture the satisfaction relation between implementations and specifications.

(η,α)-bisimilarity;stratification;checking algorithm;discount

1007-130X(2015)03-0547-06

2013-11-08;

2014-01-08基金項目：國家自然科學基金資助項目(60973045,11426136);江蘇省高校自然科學基金資助項目(13KJB520012)

TP302

A

10.3969/j.issn.1007-130X.2015.03.023

張晉津(1981-),男，山西曲沃人，博士，講師，研究方向為形式化方法和計算機科學中的邏輯學。E-mail:jinjinzhang@nau.edu.cn

通信地址：211815 江蘇省南京市南京審計學院工學院

Address:School of Technology,Nanjing Audit University,Nanjing 211815,Jiangsu,P.R.China