朱維軍，周清雷

(鄭州大學(xué) 信息工程學(xué)院 河南 鄭州 450052)

一種時(shí)間自動(dòng)機(jī)時(shí)鐘離散化算法

朱維軍，周清雷

(鄭州大學(xué) 信息工程學(xué)院 河南 鄭州 450052)

稠密時(shí)間自動(dòng)機(jī)被廣泛應(yīng)用于實(shí)時(shí)系統(tǒng)自動(dòng)驗(yàn)證.然而其在補(bǔ)操作下不封閉，因而導(dǎo)致多種線性實(shí)時(shí)性質(zhì)不可驗(yàn)證.離散時(shí)間自動(dòng)機(jī)雖不存在此問(wèn)題，但該模型表達(dá)能力偏弱.因此，提出了一種時(shí)間自動(dòng)機(jī)時(shí)鐘離散化算法，結(jié)合時(shí)鐘物理約束因素，證明了新方法可有效解決上述問(wèn)題.

時(shí)間自動(dòng)機(jī)； 模型檢測(cè)； 物理時(shí)鐘； 離散化

0 引言

模型檢測(cè)的形式化理論、計(jì)算模型與驗(yàn)證算法是近年來(lái)計(jì)算機(jī)科學(xué)的研究熱點(diǎn)之一.基于模型檢測(cè)算法的驗(yàn)證工具已經(jīng)在硬件設(shè)計(jì)、網(wǎng)絡(luò)協(xié)議、網(wǎng)絡(luò)安全協(xié)議、實(shí)時(shí)系統(tǒng)、軟件規(guī)范等領(lǐng)域取得了廣泛應(yīng)用.在實(shí)時(shí)計(jì)算系統(tǒng)模型檢測(cè)中，時(shí)間自動(dòng)機(jī)[1]已成為建立模型的事實(shí)標(biāo)準(zhǔn)，各種實(shí)時(shí)邏輯[2-7]則被提出并用來(lái)描述系統(tǒng)需滿足的性質(zhì).然而，在實(shí)數(shù)時(shí)間域上取值的線性實(shí)時(shí)邏輯與時(shí)間自動(dòng)機(jī)通常是不可模型檢測(cè)的.解決的方法有：對(duì)線性實(shí)時(shí)邏輯的語(yǔ)法做某種約束[2，4]；約束時(shí)鐘語(yǔ)義到離散域[8].現(xiàn)有的研究從數(shù)學(xué)層面上證明了離散時(shí)間自動(dòng)機(jī)的模型描述能力低于稠密時(shí)間自動(dòng)機(jī)[4,9]，繼而導(dǎo)致了尋找既能保持稠密時(shí)間自動(dòng)機(jī)的描述能力(特別是描述異步時(shí)鐘能力)，同時(shí)又能保持離散時(shí)間自動(dòng)機(jī)由于補(bǔ)操作封閉因而正則實(shí)時(shí)性質(zhì)完全可模型檢測(cè)能力的途徑[9-13].對(duì)此問(wèn)題，我們的研究從實(shí)用角度揭示了一些有益的結(jié)論.

1 時(shí)間自動(dòng)機(jī)

定義1對(duì)時(shí)鐘集合x(chóng)，時(shí)鐘約束集合Φ(X)={δ|δ=xc|x≤c|x≥c|δ1∧δ2}，其中δ1,δ2是時(shí)鐘約束且x∈X,c∈Q.

定義2對(duì)τ∈R+,v表示時(shí)鐘賦值，對(duì)任意x∈X,v(x)+τ表示對(duì)時(shí)鐘x，時(shí)鐘流逝τ后的時(shí)鐘賦值.對(duì)Y?X,[Y→0]v表示對(duì)任意x,x∈Y,v(x)∶=0;對(duì)任意x,x?Y,x∈X,v(x)不變.

2)進(jìn)展性：對(duì)任意t∈R+，存在i≥1使得τi>t，

是時(shí)間序列.

定義4時(shí)間轉(zhuǎn)換表是一個(gè)五元組(Σ,S,S0,X,E).其中，Σ是有限輸入字母表.S是有限狀態(tài)集.S0?S是開(kāi)始狀態(tài)集，X是有限時(shí)鐘集.E?S×S×Σ×2X×Φ(X)是轉(zhuǎn)換規(guī)則集.一條轉(zhuǎn)換規(guī)則具有形式(s,s′，a,λ,δ)，表示對(duì)輸入字母a，如果滿足時(shí)鐘約束δ，那么從狀態(tài)s轉(zhuǎn)換到狀態(tài)s′，并對(duì)任意x∈λ,v(x)∶=0.

定義6時(shí)間自動(dòng)機(jī)是一個(gè)六元組A=(Σ,S,S0,X,E,F)，其中,(Σ,S,S0,X,E)是一個(gè)時(shí)間轉(zhuǎn)換表,F?S是接受狀態(tài)集.

2 基于真實(shí)物理時(shí)鐘的時(shí)間自動(dòng)機(jī)表達(dá)能力

我們注意到，時(shí)間自動(dòng)機(jī)作為實(shí)時(shí)計(jì)算模型，它被廣泛應(yīng)用于工程實(shí)時(shí)系統(tǒng)的形式化驗(yàn)證.在任何這樣的實(shí)際系統(tǒng)中，所有的時(shí)鐘都需要滿足它的物理規(guī)律.任何真實(shí)的物理時(shí)鐘都不可能像數(shù)學(xué)時(shí)鐘一樣以無(wú)窮小的逼近步長(zhǎng)來(lái)計(jì)時(shí)，必然存在足夠小的純小數(shù)Δ，使得所有物理時(shí)鐘的最小計(jì)時(shí)單元都大于等于Δ.當(dāng)這樣的Δ取最大值Δmax時(shí)，我們就可以得到一個(gè)以Δmax為時(shí)間單元的時(shí)鐘(集)，使得以它(們)為時(shí)鐘(集)的離散時(shí)間自動(dòng)機(jī)TAN足以描述稠密時(shí)間自動(dòng)機(jī)TAΔ所能描述的真實(shí)實(shí)時(shí)系統(tǒng).定理1證明了這一點(diǎn).

定理1TAN與TAΔ等價(jià)

證明1)令TAΔ時(shí)間域?yàn)門(mén)IME，它的時(shí)間單元為足夠小的有理數(shù)Δ，做映射f：TIME→N，令1N=m·1TIME，m∈N，其中1N=1表示時(shí)間域N中的一個(gè)單元，1TIME=Δ∈Q,?k,Δ=1/k表示時(shí)間域TIME中的一個(gè)時(shí)間單元.令m=k，則m·1TIME=m·Δ=k·1/k=1=1N，因此，k·TIME=N，即通過(guò)乘系數(shù)k，TA在TIME上的解釋轉(zhuǎn)化為在N上的解釋.

2)同理可證TA在N上的解釋可通過(guò)乘系數(shù)1/k轉(zhuǎn)化為在TIME上的解釋.

3 離散時(shí)間自動(dòng)機(jī)構(gòu)造算法

Procedure construct_TAN

Input:TAΔ=(Σ,S,S0,X,E); Output:TAN=(Σ′,S′,S0′,X′,E′)

Begin

G∶=φ;

For allδ=x#c∈Φ(X) //#∈{<,=,>,≤,≥}

c′∶=c/Δ; //時(shí)鐘約束所有常量映射為正整數(shù)(顯然為正整數(shù)，證明略)

G∶=G∪{c′};

End for

m∶=mcd(G); //求G中元素的最大公約數(shù)

Σ′∶=Σ;S′∶=S;S0′∶=S0;X′∶=X;//構(gòu)造離散時(shí)間自動(dòng)機(jī)字母表狀態(tài)集時(shí)鐘集

E′∶=φ; //離散時(shí)間自動(dòng)機(jī)轉(zhuǎn)換規(guī)則集初始化

For alle=(s×s′×a×λ×δ)∈E

δ′∶=con(δ) //調(diào)用自定義函數(shù)求最優(yōu)化時(shí)鐘約束

e′=s×s′×a×λ×δ′;E′∶=E′∪{e′} //構(gòu)造轉(zhuǎn)換規(guī)則集

End for

End begin //離散時(shí)間自動(dòng)機(jī)構(gòu)造完成

Function con(δ) //定義函數(shù)，求離散時(shí)間自動(dòng)機(jī)時(shí)鐘步長(zhǎng)最優(yōu)化

For allx#cinδ

c′∶=c/Δ;c″∶=c′/m,replace(x#c″,x#c,δ) //所有約束被最優(yōu)化之后的約束所替換

End for

returnδ//返回最優(yōu)化之后的時(shí)鐘約束集

End function

定理2算法1的時(shí)間復(fù)雜度為O(n)

證明對(duì)TAΔ中轉(zhuǎn)換規(guī)則集E，構(gòu)造TAN轉(zhuǎn)換規(guī)則E′需時(shí)間O(|E|)；構(gòu)造TAN的輸入字母集需時(shí)O(|Σ|)；構(gòu)造TAN狀態(tài)集需時(shí)O(|S|+|S0|)，構(gòu)造TAN時(shí)鐘集需時(shí)O(|X|)；而求時(shí)鐘約束集正整數(shù)常量的最大公約數(shù)需時(shí)O(|Φ(X)|)，因此算法時(shí)間復(fù)雜度為O(|E|+|Σ|+|S|+|S0|+|X|+|Φ(X)|)，而輸入時(shí)間自動(dòng)機(jī)TAΔ的長(zhǎng)度n=|E|+|Σ|+|S|+|S0|+|X|+|Φ(X)|，因此算法1為線性時(shí)間算法.

定理1保證算法1的有效性與正確性，定理2則證明了算法具很高的效率.

定理3[9]離散時(shí)間自動(dòng)機(jī)TAN可模型檢測(cè).

4 結(jié)論

算法1的優(yōu)勢(shì)在于可以驗(yàn)證真實(shí)物理世界中實(shí)時(shí)計(jì)算系統(tǒng)的各種實(shí)時(shí)性質(zhì)(包含安全性與可靠性)，并可以開(kāi)發(fā)工具進(jìn)行全自動(dòng)驗(yàn)證，而且無(wú)需受到現(xiàn)有各種方法的約束.新方法僅僅損失了數(shù)學(xué)理論上的時(shí)間自動(dòng)機(jī)驗(yàn)證能力，而對(duì)真實(shí)物理世界中實(shí)時(shí)計(jì)算系統(tǒng)的自動(dòng)機(jī)模型表達(dá)能力并無(wú)降低，換來(lái)的是對(duì)所有時(shí)間正則性質(zhì)的可(自動(dòng))驗(yàn)證能力(定理3)，這是現(xiàn)有方法所不具備的.

由于時(shí)間自動(dòng)機(jī)已被應(yīng)用于航天控制軟硬件計(jì)算系統(tǒng)、實(shí)時(shí)通信網(wǎng)絡(luò)等領(lǐng)域的實(shí)時(shí)計(jì)算模型檢測(cè)，因此，新算法有著良好應(yīng)用前景，我們下一步準(zhǔn)備在新算法基礎(chǔ)上開(kāi)發(fā)工具.

[1] Alur R, Dill D L. A theory of timed automata[J].Theoretical Computer Science, 1994, 126(2): 183-235.

[2] Alur R, Feder T, Henzinger T A. The benefits of relaxing punctuality[J].Journal of the ACM, 1996, 43(1): 116-146.

[3] Alur R, Henzinger T A. A really temporal logic[J]. Journal of the ACM, 1994, 41(1): 181-204.

[4] Alur R, Henzinger T A. Logics and models of real time: A survey[C]//Proceedings of the Real-Time: Theory in Practice, REX Workshop, LNCS600.Berlin, 1992: 74-106.

[5] Duan Zhenhua. Modeling of hybrid systems[M]. Beijing: Science Press, 2004: 1-43.

[6] Zhou C, Hoare C A, Ravn A P. A calculus of duration[J]. Information Processing Letters, 1991, 40(5): 269-276.

[7] Li Guangyuan, Tang Zhisong. Translating a continuous-time temporal logic into timed automata[C]// Proceedings of the First Asian Symposium on Programming Languages and Systems (APLAS 2003), LNCS2895. Berlin, 2003: 322-338.

[8] 朱維軍, 張海賓, 周清雷. 離散時(shí)間區(qū)間時(shí)序邏輯可滿足性的判定[J]. 電子學(xué)報(bào)，2010，38(5)：1039-1045.

[9] Wilke T. Specifying timed state sequences in powerful decidable logics and timed automata[C]//Proceedings of the Third International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS863. Berlin, 1994：694-715.

[10] 晏榮杰,李廣元,徐雨波,等. 有限精度時(shí)間自動(dòng)機(jī)的可達(dá)性檢測(cè)[J]. 軟件學(xué)報(bào),2006,17(1): 1-10.

[11] Hanson M R. Model-checking discrete duration calculus[J]. Formal Aspects of Computing, 1994, 6A: 826-845.

[12] 姚興華，鄧培民，易忠.弱可逆有限自動(dòng)機(jī)分解的一個(gè)結(jié)果[J]. 廣西師范大學(xué)學(xué)報(bào)：自然科學(xué)版，2008，52(1)：31-33.

[13] 宋煌, 鄭麗萍, 莊雷, 等. 時(shí)間自動(dòng)機(jī)與自動(dòng)驗(yàn)證[J]. 鄭州大學(xué)學(xué)報(bào)：理學(xué)版，2001，33(2)：30-34.

NovelAlgorithmforDiscretizationofClocksofTimedAutomata

ZHU Wei-jun, ZHOU Qing-lei

(SchoolofInformationEngineering,ZhengzhouUniversity,Zhengzhou450052,China)

Some linear real-time properties can not be verified automatically because dense timed automata are not closed under complement operation. Discrete timed automata can be used to model checking discrete regular properties, but the express power of them is weak. A novel procedure was given to construct discrete timed automata from their dense time version. For physical factors of clock constrain, the new algorithm was used to solve the problem above efficiently.

timed automata; model checking; physical clocks; discretization

TP 301

A

1671-6841(2011)03-0070-03

2010-06-03

國(guó)家(863)高技術(shù)研究發(fā)展計(jì)劃項(xiàng)目，編號(hào)2007AA010408；國(guó)家自然科學(xué)基金青年基金資助項(xiàng)目，編號(hào)61003079，60901078；河南省重大科技攻關(guān)計(jì)劃項(xiàng)目，編號(hào)092101210104.

朱維軍(1976-)，男，講師，博士，主要從事計(jì)算機(jī)形式化方法、高可信軟件、實(shí)時(shí)計(jì)算等研究，E-mail:zhuweijun76@163.com.