一種時間自動機時鐘離散化算法

朱維軍，周清雷

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

一種時間自動機時鐘離散化算法

朱維軍，周清雷

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

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

時間自動機； 模型檢測； 物理時鐘； 離散化

0 引言

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

1 時間自動機

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

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

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

是時間序列.

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

定義6時間自動機是一個六元組A=(Σ,S,S0,X,E,F)，其中,(Σ,S,S0,X,E)是一個時間轉換表,F?S是接受狀態(tài)集.

2 基于真實物理時鐘的時間自動機表達能力

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

定理1TAN與TAΔ等價

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

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

3 離散時間自動機構造算法

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ù)，證明略)

G∶=G∪{c′};

End for

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

Σ′∶=Σ;S′∶=S;S0′∶=S0;X′∶=X;//構造離散時間自動機字母表狀態(tài)集時鐘集

E′∶=φ; //離散時間自動機轉換規(guī)則集初始化

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

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

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

End for

End begin //離散時間自動機構造完成

Function con(δ) //定義函數(shù)，求離散時間自動機時鐘步長最優(yōu)化

For allx#cinδ

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

End for

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

End function

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

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

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

定理3[9]離散時間自動機TAN可模型檢測.

4 結論

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

由于時間自動機已被應用于航天控制軟硬件計算系統(tǒng)、實時通信網(wǎng)絡等領域的實時計算模型檢測，因此，新算法有著良好應用前景，我們下一步準備在新算法基礎上開發(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] 朱維軍, 張海賓, 周清雷. 離散時間區(qū)間時序邏輯可滿足性的判定[J]. 電子學報，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] 晏榮杰,李廣元,徐雨波,等. 有限精度時間自動機的可達性檢測[J]. 軟件學報,2006,17(1): 1-10.

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

[12] 姚興華，鄧培民，易忠.弱可逆有限自動機分解的一個結果[J]. 廣西師范大學學報：自然科學版，2008，52(1)：31-33.

[13] 宋煌, 鄭麗萍, 莊雷, 等. 時間自動機與自動驗證[J]. 鄭州大學學報：理學版，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

國家(863)高技術研究發(fā)展計劃項目，編號2007AA010408；國家自然科學基金青年基金資助項目，編號61003079，60901078；河南省重大科技攻關計劃項目，編號092101210104.

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