有關時間自動機重置的若干問題的計算復雜性*

朱 凱, 毋國慶, 吳理華, 袁夢霆

1(武漢大學 計算機學院,湖北 武漢 430072)

2(華南農業大學 數學與信息學院,廣東 廣州 510642)

1 引 言

有限自動機的重置(或同步)問題[1],最早由?erny在1964年提出,重置的概念從此逐漸受到關注和不間斷的研究,形成了許多成果,吸引了來自計算機、數學、控制和生物領域的研究人員,這些成果已應用在離散事件系統控制、軟件測試、生物信息計算[2-4]和機器人[5]等領域.重置有限自動機的關鍵是構造重置字(或序列):有限自動機通過運行重置字w,將從任意一個未知的或無法觀測到的狀態到達某個特定狀態qw.這僅依賴于w自身,而與w開始運行時有限自動機所處的狀態q0無關.比如,Stojanovic等人[4]2003年發表在《Nature Biotechnology》上的研究成果提出了一種稱為MAYA的分子自動機,可與人對弈TIC-TAC-TOE游戲.這種自動機經過一輪對弈后需要運行重置字,將自動機帶到“新一輪游戲”狀態.再比如,Huffman編碼作為主流的數據壓縮方法之一,當壓縮的文本出現錯誤時,僅僅一個小錯誤就會毀掉整個編碼串.為確保數據的可靠性,可采用特殊的編碼方式,向壓縮數據中插入重置字,使得不論出現什么錯誤,解碼器都可以通過運行重置字恢復.于是在一定程度上得到了抗錯誤的數據壓縮方法[6].近年來,關于重置這一經典概念又激起了新的研究興趣,這得益于重置字已被泛化到變遷系統的博弈和無限狀態系統[7]上,對諸如分布式數據網絡和嵌入式實時系統這一類的復雜系統建模有著更大的意義.它還引發對時序邏輯的擴展,以規約系統的可重置性.比如Chatterjee等人[8]提出一種新的可判定的邏輯,比經典的計算樹邏輯(CTL)有更強的表達能力,為針對可重置性的模型檢測方法與工具的實現奠定了理論基礎.

在理論計算機科學(形式化理論基礎)中,對某一問題,比如某種邏輯的可滿足性、某種自動機的可達性等,首先考慮它的可判定性(常轉化為對應的判定問題),接著考慮它的計算復雜性.在具體實踐中,對不可判定的和計算復雜度高的問題,考慮若干可判定的子類或使計算復雜性得以顯著降低的子類,或考慮對應有高效近似算法的問題.這是對復雜性研究的真正意義所在.在形式化驗證領域中,要為復雜系統開發自動化的驗證工具,所涉及問題的計算復雜性是無法回避的重要研究課題之一.具體到本文關注的自動機的可重置性的研究,主要面臨如下5類問題.(1) 基本問題:給定自動機A,判定它是否為可重置的,即判斷它是否存在重置序列w.(2) 限界問題:給定自動機A和正整數k,判斷它是否存在滿足|w|≤k的重置序列w.(3) 最優問題:給定自動機A和正整數k,判定它是否存在滿足|w|=k的最短重置序列w.(4) 閾值問題:給定可重置的自動機A,給出其重置序列的最短長度的上界.其中,著名的 ?erny猜想[1]斷言:對于可以重置的含有n個狀態的自動機A,其具有長度不超過(n-1)2的重置字.該猜想至今尚未得到證明(或證偽).(5) 近似問題:針對最優問題(3),在給定的常數因子下,判定是否存在多項式時間算法近似重置序列的最小長度.在證明對應問題是可判定的情況下,給出問題(1)～問題(3)的計算復雜性,給出問題(4)的閾值和問題(5)的存在性證明.目前,針對這 5類問題,僅在有限自動機上進行了較為全面和系統的研究,其他類型的自動機上的對應研究較少,甚至沒有.

時間自動機模型是由Alur等人在20世紀90年代提出的,它在有限自動機的基礎上引入了時鐘,可測量和約束系統中的時間因素.它自從誕生以來受到廣泛關注,文獻[9]迄今成為《Theorectical Computer Science》期刊上引用最多的文章(根據GoogleScholar數據引用超過7 700次).實際上,時間自動機已成為業界有關時間系統的事實標準.20多年來,在時間自動機上展開了建模、測試、模型檢測等深入的研究和實用化工作[10-17],出現了以UPPAAL[10,11]為代表的在工業界廣泛使用的工具.在此期間,我國的林惠民院士[18,19]、王義教授[11,18,19]和趙建華教授[16,17]分別在時間自動機的公理化、UPPAAL檢測工具的研發和模型檢測優化方面取得高水平的成果.但對時間自動機重置問題的研究才剛剛起步,目前僅有的工作是Doyen及其博士生Shirmohammadi在2014年給出的結論[20,21].一般情況下,完全的確定的時間自動機的重置問題是 PSPACE-完全的,而對完全的非確定的時間自動機,它是不可判定的.這個結論回答了上述第(1)類問題中的兩個子問題,而時間自動機的其他4類問題以及第(1)類問題中的其他情況,如非完全的(即部分規約的)時間自動機的重置問題、限界條件下的重置問題等的答案尚處空缺狀態.其實,對時間自動機的第(1)類重置問題的深入討論,可以通過判斷自動機的語法或在語法上增加限制條件得到不同子類,通過研究不同子類問題的復雜性,判斷它們是否存在高效算法,比如可以限制時鐘的個數、字母表的大小,還可以約定變遷函數是否為完全函數(劃分完全的時間自動機和部分歸約的時間自動機的標準)和變遷函數是否為單值函數(劃分為確定的時間自動機和非確定的時間自動機的標準).

目前,對時間自動機的重置問題的研究只是初現端倪,很多問題尚未提出并解決,本文將完全和部分規約的概念從有限自動機延伸到時間自動機,將最早在有限自動機上討論的有關可重置性的若干問題轉移到時間自動機上,得到該問題在時間自動機上的新的復雜性結論.這些復雜性結論指出了時間自動機的重置問題本身的固有難度,它們大都是難解的.通過歸約技術說明了該問題與其他經典問題(如可達性問題)的復雜性之間的聯系.這些研究工作一方面為時間系統的可重置性的檢測和求解奠定了比較堅實的理論基礎,另一方面為將來尋找具有高效算法的特殊結構的時間系統(即具有高效算法的問題子類)給予理論指導.

本文研究工作取得的新結論具體是:

(1) 對于完全的確定的時間自動機:當時鐘個數為1即單時鐘時,它的重置問題是NLOGSPACE-完全的;當時鐘個數大于等于2時,它是PSPACE-完全的.另外,在輸入字母表的大小減少至2時,問題仍是PSPACE-完全的.

(2) 對于部分規約的確定的時間自動機:通過不同的證明方法,得到與(1)同樣的結論.

(3) 對于非確定的時間自動機:證明了Di-可重置問題(i=1,2,3)的不可判定性.此外,找到兩個可判定的子類:在單時鐘情況下,它是Ackermann-完全的;當重置序列的長度被限制在k(k∈?)時,它是NEXPTIME-完全的.

本文第2節介紹有關時間自動機及其重置序列的概念.第 3節討論完全的確定的時間自動機的重置問題,完善已有結論.第 4節討論關于部分規約的確定的時間自動機重置的若干問題的復雜性和它們之間的關系,主要是簡單的CAR-RESET問題和2-CAR-RESET問題.第5節討論完全的非確定的時間自動機重置的若干問題,比如Di-重置問題(i=1,2,3)、限界的重置問題和單時鐘的重置問題.第6節主要從有限自動機和其他自動機的重置問題、時間自動機的可達性兩方面討論相關的研究及其進展.最后給出結論以及下一步的研究方向.

2 基礎知識

符號約定.設?、?、?分別是自然數集、有理數集和實數集,?≥0是非負實數集.對有限集X,|X|和 2X分別是它的基數和冪集(即X所有子集構成的集合).若|X|=1,則稱X是單元集.XY表示由屬于X同時不屬于Y的元素構成的集合,即X-Y的差.定義在字母表Γ上的變遷系統是二元組〈Q,R〉,其中,Q是狀態集,R?Q×Γ×Q是變遷關系.用A≤pB(或A≤EB)表示問題A可多項式時間(或指數時間)歸約到問題B.

本文中出現的引理、命題和推論將在附錄中加以證明,定理直接在正文中證明.

2.1 時間自動機

時間自動機在有限自動機上擴充了時鐘,以便對系統記時.時鐘是非負實數的變量,它們的初值為 0,均以相同速率(時間增長的變化率)增加.設C是時鐘變量的有限集,在C上定義時鐘約束φ,其語法如下.

φ:=true|x#c|φ?φ

定義1(時間自動機,timed automata).時間自動機A定義為六元組〈L,l0,C,∑,E,F〉,其中,

·L是位置的有限集,l0∈L是初始位置.

·C是時鐘(變量)的有限集.

·∑是動作的有限集(即字母表).

·E?L×Guard×∑×2C×L是變遷(邊)集,Guard∈Φ(C).

·F?L是最終(接受)位置集.

注意,本文定義的時間自動機未給出位置上的不變式,實際上可將它歸入變遷的衛士;也未給出形如x-y#c的對角線約束,實際上可通過增加時鐘和約束來度量這類時鐘差.因此,不影響時間自動機的表達能力.

定義2 (時間自動機的語義,semantics of TA).時間自動機的語義解釋在變遷系統〈Q,R〉上.其中,

·Q=L×C.

·R?Q×Γ×Q,其中,Γ=∑∪?≥0.

給定q=(l,v),γ∈∑∪?≥0,loc(q)=l是狀態q對應的位置,post(q,γ)={q′|(q,γ,q′)∈R}是應用γ后狀態q的后繼.對于P?Q,loc(P)={loc{q}|q∈P},post(P,γ)= ∪q∈Ppost(q,γ).對于序列,可遞歸定義post(q,γw)=post(post(q,γ),w).

方便起見,本文對變遷函數post的使用并不嚴格規范,出現post((l,v),(t,a))和post((l,v),a)的用法,post((l,v),(t,a))=post(post(l,v),t),a),有時將post((l,v),(t,a))稱為(t,a)-變遷,其中,t∈?≥0,a∈∑.

在時間自動機中,如果∑中的每個字母在某個位置l上都有定義,且這些變遷不會離開l,那么,稱l為0位置(Zero)(或吸收位置).形式化定義為:對于l∈L,如果對?a∈∑.loc(post(l,a))=l,那么,稱l為 0 位置.

定義3(完全規約的時間自動機,completely specified TA).對于時間自動機A=〈L,l0,C,Σ,E,F〉,如果對于可達狀態(l,v)和所有a∈∑,post((l,v),a)有定義且post((l,v),a)≠?(此時,a-變遷可行),那么,它是完全規約的,簡稱完全的,否則,是部分規約的(partially specified TA).

定義4(確定的時間自動機,deterministic TA).對于時間自動機A=〈L,l0,C,Σ,E,F〉,如果對于可達狀態(l,v)和所有的a∈∑,|loc(post((l,v),a))|≤1,那么,它是確定的,否則,它是非確定的時間自動機(nondeterminsitic TA).

注意,與某些文獻不同,本文對完全的時間自動機和部分規約的時間自動機的劃分要將字母表和時間延遲當作輸入考慮進來.這一點在第3節和第4節通過構造對應自動機進行歸約來證明復雜性時有所體現.

時間自動機的(有限的)運行ρ是指序列對(S(ρ),?(ρ)),使得狀態((li,vi))0≤i≤n的序列S(ρ)和變遷(li-1,ai,gi,ri,li)的序列?(ρ),滿足如下要求:

· 對每個i=1,…,n,狀態對((li-1,vi-1),(li,vi))有邊(li-1,ai,gi,ri,li)是變遷;

· 運行ρ的軌跡是時間字(d0,a0),…,(dn-1,an-1).當忽略變遷時,運行可用((li,vi))0≤i≤n表示;

對時間字w,如果它是A的一條接受的運行軌跡,那么,它被自動機A識別(或接受).時間自動機A識別的語言用L(A)表示.用|w|表示其長度.設i,j∈{1,…,|w|},字的第i個字母用w[i]表示,假設i＜j,字w[i]w[i+1]…w[j]用w[i,j]表示.如果n是正整數,∑是字母表,則用∑n和∑*分別表示∑上所有長度為n的字的集合和長度大于等于0的字的集合.

時間自動機的可達性(reachability)問題(或時間語言的非空(nonemptiness)問題)一般情況下是 PSPACE-完全的;它的普遍性(universality)問題是不可判定的.具體證明細節見文獻[9].

2.2 重置序列

定義 5(重置序列,reset sequences).對于時間自動機A,若存在某個序列w∈((?≥0,∑))*,使得不論A處于哪個狀態,運行w上都會達到某個統一的狀態,稱w為重置(或同步(synchronizing))序列,稱A是可重置的(或可同步的).

約定重置序列的形式為由(d0,a0),…,(dn-1,an-1)的時延-動作構成的序列,例如圖 1所示引用文獻[20]中的例子展示了一個完全的確定的 1-字母單時鐘的時間自動機,它具有一條重置序列是(3,a)(0,a)(0,a)(1,a)(0,a)(0,a).有時,將時延為 0的變遷省略,并將重復動作變遷寫成指數形式,得到d(3)?a3?d(1)?a3,其中,d(m),m∈?表示時間延遲.

時間自動機的重置問題(RESET)可形式化定義為:

問題:RESET

輸入:時間自動機A.

詢問:A是否是可重置的(即A是否存在一個重置序列w)?

3 完全的時間自動機的重置問題

本節研究完全的確定的時間自動機的重置問題,考慮時鐘個數對復雜性的影響,利用當時鐘個數不同時時間自動機的可達性問題的復雜性結論完善Doyen等人的結論.

3.1 一般情況

一般情況下的結論是由Doyen等人給出的,其復雜性是PSPACE-完全的,它是這一節的研究基礎.具體細節見文獻[20,21].主要思想是分兩階段構造重置序列:第 1階段利用了完全的確定的時間自動機的結構特點,搜索某個一定存在的序列,將起初的無限狀態空間壓縮到有限的狀態空間.第 2階段采用有限自動機的重置序列的求解方法[22],對第1階段得到的狀態集,兩兩成對搜索重置序列以判斷它的存在性.這種算法將消耗多項式空間的存儲資源,因此屬于PSPACE.對于PSPACE-難的證明使用從時間自動機的可達性問題到重置問題的歸約.

3.2 考慮時鐘個數時的復雜性

定理 1.對于單時鐘的完全的確定的時間自動機,它的重置問題是 NLOGSPACE-完全的;對于含 2個或 2個以上時鐘的完全的確定的時間自動機,它的重置問題是PSPACE-完全的.

證明思路.根據Doyen[20]的結論,一般情況的重置問題是PSPACE-完全的.這里只需要考慮時鐘個數的情況.

證明:PSPACE成員性(即問題屬于 PSPACE)的證明與 Doyen等人的證明相同.PSPACE-難的證明不同于Doyen等人的證明,這里,將語言的非空問題歸約到重置問題,而Doyen等人是從可達性問題歸約的.自動機的可達性問題和語言的非空問題本質上等價的,這樣歸約的目的是為了與第4節定理2的證明中的歸約保持一致.

從A可以構造一個完全的確定的時間自動機A′,將L(A)的非空問題歸約到重置問題.

給定A=〈L,li,C,Σ,E,F〉,可以在多項式時間內構造A′=〈L′,l0′,C′,∑′,E′,F′〉,其構造過程如下.

·C′=C;

·∑′=∑∪{α};

·對于表示變遷函數定義的邊集E′,按以下次序構造,如圖2所示.

(a)E′=E;

(b)E′=E′-{(lp,g,a,r,l)|lp∈F,a∈Σ},即刪除F中的每個位置上的出邊;

(c)E′=E′∪{(lp,true,Σ,C,lf)|lp∈F},即為F中的每個位置增加到lf的變遷,圖2中用綠色標注的變遷;

(d)E′=E′∪{(lf,true,∑∪{α},C,lf)},即為lf增加到自身的環,圖2中用藍色標注的變遷,此時,lf成為A′的零位置;

(e)E′=E′∪{(l0,true,Σ∪{α},C,li)},即為l0增加到li的變遷,圖2中用藍色標注的變遷;

(f)E′=E′∪{(l,true,α,C′,l0′)|l∈L′{l0,lf}},即為A′中除l0和lf之外的位置增加到l0的變遷,圖2中用紅色標注的變遷.

從圖2所示的構造方案容易看出:w∈((?≥0,∑))*是lp的接受字,即w∈L(A) 當且僅當u=(t1,α)?w?(t2,c)是A′的重置序列,其中,t1,t2∈?≥0,c∈∑.

接著考慮時鐘因素:由于 Laroussinie等人證明了單時鐘和雙時鐘的時間自動機的可達性問題分別是NLOGSPACE-完全的和NP-難的(細節見文獻[23]中的命題5.1和命題 6.1),Fearnley等人進一步確定了雙時鐘的自動機的可達性問題是PSPACE-完全的(細節見文獻[24]末尾部分的推論12).Courcoubetis等人證明了含3個時鐘的時間自動機的可達性是 PSPACE-完全的(細節見文獻[25]中的定理 2).對含k(k>3)個時鐘的時間自動機,Haase等人[26,27]證明了它與受限的2-計數器自動機是對數空間內相互歸約的,利用受限的2-計數器自動機的可達性問題是PSPACE-完全的結論證明了它是PSPACE-完全的.

4 部分規約的時間自動機的重置問題

本節研究部分規約的確定的時間自動機在一般情況下和輸入字母表大小為 2時的計算復雜性.將Martyugin[28,29]在部分規約的有限自動機上的研究擴展到時間自動機,證明的技術路線與其大致相同,由于加入了時鐘,因此情況要復雜得多.為方便起見,本節若無特殊說明,均將省略“確定的”字樣.

4.1 一般情況

比較常見的是部分歸約的時間自動機.對于這類時間自動機,如果存在序列w∈((?≥0,∑))*,使得post(L×C,w)有定義且|post(L×C,w)|=1|,那么,稱w是仔細重置序列(carefully reset sequence),稱該時間自動機是可仔細重置的.仔細重置序列沒有使用自動機上未定義的變遷(區別有定義但不可行的變遷),是一般重置序列的泛化.

仔細重置問題(CARE-RESET),即部分規約的時間自動機的重置問題,可形式化為:

問題:CARE-RESET(ZERO CARE-RESET)

輸入:(含一個零位置的)部分規約的時間自動機A;

詢問：A是否是可仔細重置的(A是否存在一個仔細重置序列)?

定理2.ZERO CARE-RESET問題是PSPACE-完全的.

證明思路.首先證明有非確定的多項式空間的算法判斷重置序列的存在性,即證明PSPACE的成員性(利用薩維奇定理 NPSPACE=PSPACE的結論).然后證明是 PSPACE-難的,從k(k∈?,k≥2)個時間自動機交問題歸約.

證明:Doyen[20]通過舉出反例證實:由于區域圖抽象掉了具體時間信息,它的重置序列不一定是原自動機的重置序列.若能在自動機的區域圖[9]上找到一條長度不超過區域大小的 3次方的序列作為候選重置序列(因為可重置的完全的有限自動機的重置序列閾值是(n3-n)/6,其中,n是區域圖的狀態個數,可參考文獻[28],而可重置的部分規約的有限自動機的重置序列也滿足該閾值),則自動機有可能是可重置的,否則,一定是不可重置的.猜測時按需展開(on-the-fly)產生區域圖,每次猜一個字母,總次數不超過閾值,如果存在候選序列,就接著對候選序列編碼形成線性的實數算術公式,再輸入 SMT求解器檢查:(1) 任意兩個區域狀態;(2) 區域中任意兩個狀態執行候選序列后時鐘賦值(自最后一次重置以來)是否相等(即同步).因為猜測候選重置序列這一步需要多項式空間的存儲資源,采用SMT求解屬于PSPACE.那么,這個“猜測-檢驗”算法屬于PSPACE,即算法需要多項式空間的存儲資源.

以下給出PSPACE-難的證明.

B的構造過程如下,如圖3所示.圖中綠色和紅色的虛線方框分別標識自動機iA和它的最終位置集Fi.

由命題1(k(k≥2)個時間自動機交),可得ZERO CARE-RESET是PSPACE-完全的.

如果采用定理2證明中的構造方法,從若干個時間自動機構造出B,則稱B是簡單的.

說明:對于完全的確定的時間自動機,構造的新的時間自動機也是完全的確定的,在定理1的證明中使用的構造是對F中的每個狀態刪除了它的所有出邊,并增加分別指向l0和lf的邊,同時將lf改造為零位置,而對于部分規約的自動機,構造思路大致相同但要更加復雜,都增加了零位置.對于完全時間自動機,Doyen等人給出一種較暴力的算法[20],對于部分規約的時間自動機,本文沒有給出相應的算法細節是基于兩點原因:首先,時間自動機的狀態空間是無窮的,而基于時間互模擬等價的區域自動機[9]來計算序列是不可靠的,需要進一步的檢驗.其次,由于變遷函數不是完全函數,所以Doyen算法第1階段的構造在部分規約的時間自動機上可能無法實現.但這并不影響問題具有PSPACE成員性的結論以及對問題復雜性的討論.

至于可重置的部分規約的有限自動機的重置序列可以復用完全的有限自動機的重置序列閾值,原因在于,前者的可重置序列一定是對應的擴展(結構(狀態和變遷)保持不變,只飽和化變遷上的字母表和時鐘衛士)后的完全的有限自動機的重置序列,顯然滿足其閾值.

選取的簡單的CAR-RESET問題實際上是CAR-RESET問題的子類,復雜性是PSPACE-完全的,而且ZERO CAR-RESET≤pCAR-RESET,那么,對于CAR-RESET問題仍是PSPACE-完全的.

4.2 考慮輸入字母表大小時的復雜性

有時還會將問題限制在最多有k(k∈? )個輸入字母的自動機上,這類問題的命名一般采用前綴k-的方式,比如2-CARE-RESET是指將CARE-RESET問題限制到最多含有2個輸入字母的時間自動機上.

用簡單的CAR-RESET表示對問題CAR-RESET的限制,將在以下定理的證明中加以使用.

定理3.2-ZERO CAR-RESET問題是PSPACE-完全的.

證明思路.問題的 PSPACE成員性證明與定理 2相同.關鍵是證明它是 PSPACE-難的,可從 ZERO CARRESET問題歸約到2-ZERO CAR-RESET問題.

證明:這個問題的 PSPACE成員性的證明與定理 2相同.以下將簡單的 ZERO CAR-RESET問題歸約到2-ZERO CAR-RESET問題來證明它是PSPACE-難的.

圖 4通過一個簡單的例子展示了上述構造方法.首先將給定的時間自動機A1和A2轉換為簡單的部分歸約的時間自動機B,然后將B轉換為一個 2-字母的部分規約的時間自動機 .C B中用紅色標注的變遷是構造時增加的,它們在C中也對應標注為紅色,變遷上的字母變為b;B中用黑色標注的變遷源自A1和A2中的變遷,它們在C中保持黑色不變,標注的字母變為b;C中藍色標注的變遷對應步驟(a)和步驟(b)的構造,標注的字母是a.另外,c0=b,c1=ab,c2=a2b,c3=a3b.

設k∈{0,…,m+1}和i∈{1,…,n},Rowk={lk,1,…,lk,n}是LC的第k行,Coli={l0,i,…,lm+1,i}是集合LC的第i列(在對自動機C的引用是清楚的情況下,可省略位置的上標),其中,第n列退化為z,顯然,z屬于每一行,即?k∈{0,…,m+1}有lk,n=z.

引理2.

(1) 對于i∈{1,…,n},loc(post(Coli×CC,a))?Coli;

(2) 對于k∈{0,…,m},loc(post(Rowk×CC,a))?Rowk+1,特別地,loc(post(Rowm+1×CC,a))?Rowm+1;

(3)loc(post(LC×CC,b))?Row0.

引理3.如果u∈((?≥0,{a,b}))*((?≥0,{a}))*且post(LC×CC,u)有定義,那么,

(1) 對每個i∈{1,…,n},|Coli∩loc(post(LC×CC,u))|≤1;

(2) |loc(post(LC×CC,u?(t,a)))|=|loc(post(LC×CC,u))|,其中,t∈?≥0;

(3)loc(post(LC×CC,u?(t,b)))?Row0,其中,t∈?≥0.

定義映射f:(?≥0,{a,b}*b)→(?≥0,Σ),其中,Σ=｛c0,...,cm+1｝:

對每個k(k≥2,k∈?),k-字母的重置問題是對應的無約束版本的特例.對于每個無約束版本的問題,其k-字母的重置問題的實例自動機可以轉化為同類問題的(k+1)-字母版本的實例,通過增加一個額外的字母即可得到新的自動機,對原自動機的每個位置增加到其自身的變遷,以這個額外字母為標記.于是,k-RESET≤p(k+1)-RESET.

時鐘個數對該問題的影響,在第 3節已有討論,有關的結論是一致的.字母表大小對完全的確定的時間自動機的重置問題的復雜性影響也可以用類似定理3的歸約的方法來加以探討,于是得到以下兩個推論.

推論1.對于單時鐘的部分規約的確定的時間自動機,它的重置問題是NLOGSPACE-完全的;對含有2個或2個以上時鐘的部分規約的確定的時間自動機,它的重置問題是PSPACE-完全的.

推論2.對于完全的確定的時間自動機,即使它的字母表大小減少到2,其重置問題仍是PSPACE-完全的.

5 非確定的時間自動機的重置問題

本節主要討論完全的非確定的時間自動機的重置問題的兩個可判定子類——限界問題和單時鐘問題,直接利用了完全的非確定的寄存器自動機的限界重置問題的結論[30]和結構相同的時間自動機與寄存器自動機之間可指數時間內相互可歸約的結論[31].比如,在文獻[31]中,從安全的單路交錯的單寄存器自動機的非空問題是EXPSPACE-難的,直接得出對應的交錯的安全的單時鐘自動機的非空問題是EXPSPACE-難的.

5.1 一般情況

一般情況下的結論是由Doyen等人給出的,它是不可判定的.證明的具體細節見文獻[20,21].主要思想是利用時間語言普遍性問題的不可判定性[9],得到非普遍性問題的不可判定性.然后從時間語言的非普遍性問題歸約到它的重置問題.

5.2 Di-可重置問題

類似非確定的有限自動機[28,29,32],考慮對應的非確定的時間自動機的Di-可重置問題(i=1,2,3).

對于時間自動機A=〈L,l0,C,∑,E,F〉,序列w∈((?≥0,∑))*被稱為是:

·D1-可重置的,如果對所有(l,v)∈L×C,滿足post((l,v),w)有定義且|post(L×C,w)|=1;

·D2-可重置的,如果對所有(l,v)∈L×C,滿足post((l,v),w)有定義且post((l,v),w)=post(L×C,w);

·D3-可重置的,如果∩(l,v)∈L×Cpost((l,v),w))≠?.

Di-可重置問題(Di-RESET)可形式化為:

問題:D1-RESET(D2-RESET,D3-RESET).

輸入:非確定的時間自動機;A

詢問:非確定的時間自動機是否是D1-可重置的(或D2-可重置的,或D3-可重置的)?

定理4.非確定的時間自動機的Di-可重置問題是不可判定的(i=1,2,3).

證明:因為 Doyen等人證明了完全的非確定的時間自動機的重置問題在一般情況下是不可判定的[20,21],所以,非確定的時間自動機是否是D1-可重置的是不可判定的.

引理5.每個D1-重置序列也是D2-重置序列,每個D2-重置序列也是D3-重置序列.

根據引理5,D2-可重置和D3-可重置問題均是不可判定的.

5.3 限界的重置問題的復雜性

定理 5.完全的非確定時間自動機的限界的非普遍性問題(BOUNDED-NONUNIVERSALITY)是NEXPTIME-完全的.

證明:首先證明該問題屬于NEXPTIME.可以猜測一個長度小于k的序列w,能在指數時間內檢查w是不是它接受的字.然后證明它是NEXPTIME-難的.Babari和Quaas等人[30]證明了完全的非確定的寄存器自動機的限界的普遍性問題(BOUNDED-UNIVERSALITY)是 co-NEXPTIME-完全的,即非確定的寄存器自動機的限界的非普遍性問題是NEXPTIME-完全的.

命題2.NEXPTIME和ACK在指數時間歸約下封閉.

Figueira給出的時間自動機和寄存器自動機之間的歸約是指數時間的,根據命題 2,指數時間歸約對于NEXPTIME是封閉的.Figueira等人[31]證明非確定的寄存器自動機的普遍性問題可以在指數時間內歸約到非確定的時間自動機的普遍性問題上.那么,非確定的時間自動機的限界的非普遍性問題是NEXPTIME-難的.

定理6.完全的非確定時間自動機的限界重置問題(BOUNDED-RESET)是NEXPTIME-完全的.

證明:首先證明該問題是NEXPTIME的成員.可以猜測一個長度小于k的序列w,可以在指數時間內檢查w是否為重置序列.接下來證明這個問題是NEXPTIME-難的.Doyen等人[20,21]證明非確定的時間自動機的非普遍性問題可以在多項式時間內歸約到非確定的時間自動機的重置問題,于是非確定的時間自動機的限界的非普遍性問題也可以在多項式時間內歸約到非確定的時間自動機的限界重置問題.再根據定理 5可知,非確定的時間自動機的限界重置問題(BOUNDED-RESET)是NEXPTIME-難的.

5.4 單時鐘的重置問題的復雜性

定理7.完全的非確定的單時鐘時間自動機的重置問題是Ackermann-完全的.

證明:首先證明它屬于ACK.參照文獻[30](它的引理6和引理7),可知存在兩類完全的非確定的單寄存器自動機,使得在重置時需要讀取Ackermann(n)多的不同數據字和為了到達重置狀態需要讀取2n次輸入數據字,其中,位置個數為O(n).時間自動機重置時,重置序列的長度也存在類似的兩種情況.然后再證明它是 Ackermann-難的.Figueira等人[31]證明完全的非確定的寄存器自動機的普遍性問題可以在指數時間內歸約到非確定的時間自動機的普遍性問題,并且保持寄存器的數目與時鐘數目相等.Babari和 Quaas[30]證明單寄存器的非確定的寄存器自動機的重置問題是Ackermann-完全的.根據命題2,指數時間歸約對于ACK是封閉的,所以單時鐘的非確定的時間自動機的重置問題是Ackermann-難的.

注意,指數時間歸約不同于多項式時間歸約,相對低復雜性類是不封閉的,對它的使用需具體問題具體分析.

6 相關工作

6.1 有限自動機和其他自動機的重置問題

關于重置問題較早、較全面的研究是在完全的確定的有限自動機上進行的.確定的有限自動機的結論見表1的第2列和第3列.表1的第1行第4列和第1行第5列分別對應本文第3節和第4節的工作.鑒于時間自動機結構上比有限自動機更加復雜,本文考慮了第(1)類問題中的若干子類,比如時鐘個數、字母表大小的情況.對于完全的確定的時間自動機,完善了 Doyen等人的工作,得到若干更精細的結論;對于部分規約的時間自動機,本文對它的重置問題的研究工作是最早的,更具體的結論總結見第 7節的表 2.對于第(2)類問題,本文的一個后繼工作已獲知其限界問題的復雜性也是PSPACE-完全的,限于篇幅,對它的證明將另文給出探討.表1和表2中復雜性類后的-C符號表示該復雜性類是完全的,Open表示對應位置上的問題還未得到研究.

Table 1 Main results of the problems for resetting deterministic finite automata and timed automata表1 關于確定的有限自動機和時間自動機重置問題的主要結論

對非確定的有限自動機,傳統上研究它的Di-可重置問題(i=1,2,3).Imreh和 Steinby[32]給出它們是可判定的,Martyugin[28,29]證明這3個問題都是PSPACE-完全的.對非確定的有限自動機的重置序列的長度d1(n),Gazdag和Iván給出d1(n)=Θ(2n)的結論(見文獻[36]中的定理1).本文在第5節針對完全的非確定的時間自動機進行了研究,Doyen等人指出一般情況下它是不可判定的,在此基礎上,本文證明了它的Di-可重置問題是不可判定的,還找到了它在限界和單時鐘條件下的兩個可判定的子類,其復雜度分別是NEXPTIME-完全的和Ackermann-完全的.這些結論也是本文首次給出.

從有限自動機的重置問題的研究路線和方法上,大致可以得到時間自動機研究的方向、方法和待解決的問題.因為加入了時鐘的要素,問題變得更加復雜,可將在有限自動機上證明的思想和方法擴展到時間自動機上來,如本文第4節的工作采用類似的思想但卻是不同的歸約過程,將Martyugin[28,29]在部分規約的有限自動機上的工作移植到部分規約的時間自動機上.我們還發現:尋找求解時間自動機重置問題的多項式時間的高效算法不應盲目和樂觀,其存在性需要計算復雜性的理論結果作為支撐,首先研究重置問題的計算復雜性意義更重大.

對其他種類自動機的研究有:Doyen等人還討論了概率有限自動機[37]和權重自動機的重置問題[20,21].Caucal[38]和 Chistikov等人[39]還分別研究了下推自動機和嵌入字自動機的重置問題.對于 Babari和 Quaas等人[30]在寄存器自動機的數據重置字問題上的工作,本文第 5節在研究非確定的時間自動機的重置問題時,采用寄存器自動機到時間自動機的指數時間可歸約[31],利用他們的結論直接證明了新的結論.

6.2 時間自動機的可達性問題

對時間自動機,它的可達性問題[9,40]與時間自動機機對應的時間正則語言的非空問題是等價的,很多問題都與它們有聯系.比如,針對Fq和Gp等性質的LTL模型檢測問題和本文討論的時間自動機的重置問題都可以從它歸約,因此這兩個問題是基本問題.本文的定理 1是從完全的確定的時間自動機的可達性問題歸約的,定理2是從多個部分規約的確定的時間自動機語言的交的非空問題(即多個時間自動機積的可達性問題)歸約的.這說明,重置問題至少與可達性問題是一樣難的,如果有實用的方法求解可達性,那么,同樣也可以求解可重置性.

近年來,對時間自動機的可達性問題的研究進展主要體現在理論和算法優化兩個方面:(1) 弄清時間自動機模型與其他自動機模型間的相互模擬關系[26,27,31],比如就時鐘這個關鍵影響因素,得到單時鐘和k-時鐘(k≥2)的自動機的可達性問題的復雜性[23,24],時間自動機與計數器自動機[26,27]、寄存器自動機之間的關系[31],還弄清時間自動機與某些時序邏輯之間的關系,比如CLTLoc邏輯[41]、MTL和MITL邏輯[42,43].這些理論在討論與之相關的復雜性證明時經常用到,本文第3節定理1的證明使用的結論就是通過時間自動機與計數器自動機之間的相互模擬得到的復雜性結論.另外,本文第5節定理5～定理7的證明也使用了寄存器自動機與時間自動機的相互歸約關系.(2) 在可達性分析算法優化方面的進展,主要是在抽象-精化的框架下集成插值[15]、對于zone結構引入了保可達性的上近似抽象[13,14].另外,是由 SMT求解器的進步帶來的限界模型檢測性能的提升[12],這些算法實現的原型在某些情況下的性能是優于UPPAAL的.如果采用定理1和定理2中證明PSPACE成員性時提出的基于“猜測-檢驗”的非確定性算法計算(或檢驗)重置序列,那么,可達性分析和SAT/SMT求解顯然是算法實現的重要組成部分,復雜性的結論還揭示出,只有在時間自動機規模不大時,基于“猜測-檢驗”思想的算法才是可以實現的.

6.3 涉及的多個問題間的關系

不可判定性和復雜性的證明均使用歸約,此外,復雜性證明還需進行算法分析,主要分析對資源(時間和空間)的消耗,算法大多是非確定的,與非確定的計算模型相對應.歸約分為高效的多項式時間歸約和指數時間歸約兩類,本文所涉及的各問題間的歸約關系在圖 5中給出總結,其中,歸約符號右上方所標注的定理旨在說明在定理的證明中使用了這種歸約.

7 結 論

本文最先研究了時間自動機在若干種約束條件下的重置問題的復雜性,具體結論見表 2,表中標注了對應定理和推論的結論都屬于本文的新結論,特別是部分規約的確定的時間自動機的重置問題的若干結論.

下一步的研究方向是時間自動機的閾值問題和可描述時間系統的可重置性的邏輯.另一個研究方向是利用已有的開源模型檢測框架[15]和SMT求解器開發計算重置序列的原型.

Table 2 Results of the problems for resetting timed automata表2 關于時間自動機重置問題的結論

致謝感謝華南農業大學數學與信息學院黃瓊教授為本文復雜性證明提供了很好的建議.感謝各位匿名評審專家為本文研究工作的進一步完善提出了寶貴意見.

附錄

引理1的證明:只有經過*-變遷才能將A1,…,Ak中的狀態最終融合到end位置→.因此,(t2,*)應出現在u中.簡單起見,可令t2=0.顯然,如果post(LB×CB,(0,*))有定義,則post(LB×CB,(0,*))=(end,0),它是單元集.如果對于n≤|u|,u[n]=(t2,*),那么,u的前綴u[1,n]也是B的一個仔細重置序列.由于假設u是最短的仔細重置序列,那么,n=|u|且(t2,*)在u中僅出現1次,它位于u的末端.

因為u必須從begin位置開始,∑中的字母和符號*在begin位置上均沒有定義,所以u[1]=(t1,#),簡單起見,可令t1=0,于是對于某個w∈((?≥0,∑∪{→#}))*,u可以被表示為u=(0,#)?w?(t2,*)的形式.因為對每個i∈{1,…,k},滿足post(LB×CB,(0,#))∩(Li×CB)={(li,0)},所以|post(LB×CB,(0,#))∩(Li×CB)|=1.∑中的字母和符號#都定義在集合Li×CB上,并且這些變遷將Li×CB映射到Li×CB自身.因此,對?m∈{1,...,|u|-1},有|loc(post(LB×CB,u[1,m]))∩Li)|=1.于是,對于某個m,如果u[m]=(0,#),那么,loc(post(LB×CB,u[1,m]))={l1,...,lk}=loc(post(LB×CB,(0,#))),這樣,(0,#)?u[m+1,|u|]也是B的一個仔細重置序列.由于已假設u是最短的仔細重置序列,所以,(0,#)變遷在u中只會出現1次,因此,(0,#)不會出現在w中.

再由時間正則語言L(A)非空的判定問題是PSPACE-完全的(具體細節參考文獻[9]中的定理4.17的證明)可證.

注意,該命題PSPACE成員性可以看成是“PSPACE對交運算封閉”[44]的具體表現形式.

引理2的證明:(1)～(3)均可由變遷函數的定義直接得出.

注意,(1)和(2)意味著a-變遷不改變位置所在列號,但會使位置的行號加1,如果位置已在最后一行,那么該位置形成自環.(3)意味著b-變遷會使位置進入第0行.

引理3的證明:

引理的第2句可類似地歸納證明.

推論1的證明:由定理1的證明中提到的:時鐘個數不同時,時間自動機的可達性問題的復雜性結論和定理2的證明中提到的:一般情況下部分規約的時間自動機的重置問題的復雜性結論可證.

推論2的證明:采用定理3的證明中使用的多字母表到2-字母表的映射方法可證.

引理5的證明:可由Di-重置序列(i=1,2,3)的定義直接得到.

命題2的證明:首先證明,對于問題A和問題B,如果A≤EB且A∈NEXPTIME,那么B∈NEXPTIME.設M是判定B的算法,f是從A到B的指數時間歸約.判定A的算法N可以描述為

N=“對于輸入w:

(1) 計算f(w);

然后證明:對于問題A和問題B,如果A≤EB且A∈ACK,則B∈ACK.由于ACK是超過ELEMENTARY的快速增長的復雜性類[45],顯然,它相對指數時間歸約是封閉的.