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

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

2(華南農(nóng)業(yè)大學(xué) 數(shù)學(xué)與信息學(xué)院,廣東 廣州 510642)

1 引 言

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

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

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

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

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

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

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

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

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

2 基礎(chǔ)知識

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

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

2.1 時間自動機

時間自動機在有限自動機上擴充了時鐘,以便對系統(tǒng)記時.時鐘是非負實數(shù)的變量,它們的初值為 0,均以相同速率(時間增長的變化率)增加.設(shè)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是最終(接受)位置集.

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

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

·Q=L×C.

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

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

方便起見,本文對變遷函數(shù)post的使用并不嚴(yán)格規(guī)范,出現(xiàn)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(完全規(guī)約的時間自動機,completely specified TA).對于時間自動機A=〈L,l0,C,Σ,E,F〉,如果對于可達狀態(tài)(l,v)和所有a∈∑,post((l,v),a)有定義且post((l,v),a)≠?(此時,a-變遷可行),那么,它是完全規(guī)約的,簡稱完全的,否則,是部分規(guī)約的(partially specified TA).

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

注意,與某些文獻不同,本文對完全的時間自動機和部分規(guī)約的時間自動機的劃分要將字母表和時間延遲當(dāng)作輸入考慮進來.這一點在第3節(jié)和第4節(jié)通過構(gòu)造對應(yīng)自動機進行歸約來證明復(fù)雜性時有所體現(xiàn).

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

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

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

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

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

2.2 重置序列

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

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

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

問題:RESET

輸入:時間自動機A.

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

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

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

3.1 一般情況

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

3.2 考慮時鐘個數(shù)時的復(fù)雜性

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

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

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

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

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

·C′=C;

·∑′=∑∪{α};

·對于表示變遷函數(shù)定義的邊集E′,按以下次序構(gòu)造,如圖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中用綠色標(biāo)注的變遷;

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

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

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

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

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

4 部分規(guī)約的時間自動機的重置問題

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

4.1 一般情況

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

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

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

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

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

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

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

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

以下給出PSPACE-難的證明.

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

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

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

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

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

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

4.2 考慮輸入字母表大小時的復(fù)雜性

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

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

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

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

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

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

設(shè)k∈{0,…,m+1}和i∈{1,…,n},Rowk={lk,1,…,lk,n}是LC的第k行,Coli={l0,i,…,lm+1,i}是集合LC的第i列(在對自動機C的引用是清楚的情況下,可省略位置的上標(biāo)),其中,第n列退化為z,顯然,z屬于每一行,即?k∈{0,…,m+1}有l(wèi)k,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-字母的重置問題是對應(yīng)的無約束版本的特例.對于每個無約束版本的問題,其k-字母的重置問題的實例自動機可以轉(zhuǎn)化為同類問題的(k+1)-字母版本的實例,通過增加一個額外的字母即可得到新的自動機,對原自動機的每個位置增加到其自身的變遷,以這個額外字母為標(biāo)記.于是,k-RESET≤p(k+1)-RESET.

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

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

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

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

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

5.1 一般情況

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

5.2 Di-可重置問題

類似非確定的有限自動機[28,29,32],考慮對應(yīng)的非確定的時間自動機的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-重置序列.

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

5.3 限界的重置問題的復(fù)雜性

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

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

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

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

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

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

5.4 單時鐘的重置問題的復(fù)雜性

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

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

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

6 相關(guān)工作

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

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

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

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

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

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

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

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

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

6.3 涉及的多個問題間的關(guān)系

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

7 結(jié) 論

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

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

Table 2 Results of the problems for resetting timed automata表2 關(guān)于時間自動機重置問題的結(jié)論

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

附錄

引理1的證明:只有經(jīng)過*-變遷才能將A1,…,Ak中的狀態(tài)最終融合到end位置→.因此,(t2,*)應(yīng)出現(xiàn)在u中.簡單起見,可令t2=0.顯然,如果post(LB×CB,(0,*))有定義,則post(LB×CB,(0,*))=(end,0),它是單元集.如果對于n≤|u|,u[n]=(t2,*),那么,u的前綴u[1,n]也是B的一個仔細重置序列.由于假設(shè)u是最短的仔細重置序列,那么,n=|u|且(t2,*)在u中僅出現(xiàn)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的一個仔細重置序列.由于已假設(shè)u是最短的仔細重置序列,所以,(0,#)變遷在u中只會出現(xiàn)1次,因此,(0,#)不會出現(xiàn)在w中.

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

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

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

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

引理3的證明:

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

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

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

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

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

N=“對于輸入w:

(1) 計算f(w);

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