有關(guān)時(shí)間自動(dòng)機(jī)重置的若干問題的計(jì)算復(fù)雜性*

朱 凱, 毋國慶, 吳理華, 袁夢(mèng)霆

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

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

1 引 言

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

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

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

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

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

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

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

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

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

2 基礎(chǔ)知識(shí)

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

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

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

時(shí)間自動(dòng)機(jī)在有限自動(dòng)機(jī)上擴(kuò)充了時(shí)鐘,以便對(duì)系統(tǒng)記時(shí).時(shí)鐘是非負(fù)實(shí)數(shù)的變量,它們的初值為 0,均以相同速率(時(shí)間增長的變化率)增加.設(shè)C是時(shí)鐘變量的有限集,在C上定義時(shí)鐘約束φ,其語法如下.

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

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

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

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

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

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

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

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

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

·Q=L×C.

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

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

方便起見,本文對(duì)變遷函數(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),有時(shí)將post((l,v),(t,a))稱為(t,a)-變遷,其中,t∈?≥0,a∈∑.

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

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

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

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

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

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

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

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

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

2.2 重置序列

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

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

時(shí)間自動(dòng)機(jī)的重置問題(RESET)可形式化定義為:

問題:RESET

輸入:時(shí)間自動(dòng)機(jī)A.

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

3 完全的時(shí)間自動(dòng)機(jī)的重置問題

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

3.1 一般情況

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

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

定理 1.對(duì)于單時(shí)鐘的完全的確定的時(shí)間自動(dòng)機(jī),它的重置問題是 NLOGSPACE-完全的;對(duì)于含 2個(gè)或 2個(gè)以上時(shí)鐘的完全的確定的時(shí)間自動(dòng)機(jī),它的重置問題是PSPACE-完全的.

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

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

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

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

·C′=C;

·∑′=∑∪{α};

·對(duì)于表示變遷函數(shù)定義的邊集E′,按以下次序構(gòu)造,如圖2所示.

(a)E′=E;

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

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

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

(e)E′=E′∪{(l0,true,Σ∪{α},C,li)},即為l0增加到li的變遷,圖2中用藍(lán)色標(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∈∑.

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

4 部分規(guī)約的時(shí)間自動(dòng)機(jī)的重置問題

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

4.1 一般情況

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

仔細(xì)重置問題(CARE-RESET),即部分規(guī)約的時(shí)間自動(dòng)機(jī)的重置問題,可形式化為:

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

輸入:(含一個(gè)零位置的)部分規(guī)約的時(shí)間自動(dòng)機(jī)A;

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

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

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

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

以下給出PSPACE-難的證明.

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

由命題1(k(k≥2)個(gè)時(shí)間自動(dòng)機(jī)交),可得ZERO CARE-RESET是PSPACE-完全的.

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

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

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

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

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

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

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

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

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

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

圖 4通過一個(gè)簡單的例子展示了上述構(gòu)造方法.首先將給定的時(shí)間自動(dòng)機(jī)A1和A2轉(zhuǎn)換為簡單的部分歸約的時(shí)間自動(dòng)機(jī)B,然后將B轉(zhuǎn)換為一個(gè) 2-字母的部分規(guī)約的時(shí)間自動(dòng)機(jī) .C B中用紅色標(biāo)注的變遷是構(gòu)造時(shí)增加的,它們?cè)贑中也對(duì)應(yīng)標(biāo)注為紅色,變遷上的字母變?yōu)閎;B中用黑色標(biāo)注的變遷源自A1和A2中的變遷,它們?cè)贑中保持黑色不變,標(biāo)注的字母變?yōu)閎;C中藍(lán)色標(biāo)注的變遷對(duì)應(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列(在對(duì)自動(dòng)機(jī)C的引用是清楚的情況下,可省略位置的上標(biāo)),其中,第n列退化為z,顯然,z屬于每一行,即?k∈{0,…,m+1}有l(wèi)k,n=z.

引理2.

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

(2) 對(duì)于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) 對(duì)每個(gè)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｝:

對(duì)每個(gè)k(k≥2,k∈?),k-字母的重置問題是對(duì)應(yīng)的無約束版本的特例.對(duì)于每個(gè)無約束版本的問題,其k-字母的重置問題的實(shí)例自動(dòng)機(jī)可以轉(zhuǎn)化為同類問題的(k+1)-字母版本的實(shí)例,通過增加一個(gè)額外的字母即可得到新的自動(dòng)機(jī),對(duì)原自動(dòng)機(jī)的每個(gè)位置增加到其自身的變遷,以這個(gè)額外字母為標(biāo)記.于是,k-RESET≤p(k+1)-RESET.

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

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

推論2.對(duì)于完全的確定的時(shí)間自動(dòng)機(jī),即使它的字母表大小減少到2,其重置問題仍是PSPACE-完全的.

5 非確定的時(shí)間自動(dòng)機(jī)的重置問題

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

5.1 一般情況

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

5.2 Di-可重置問題

類似非確定的有限自動(dòng)機(jī)[28,29,32],考慮對(duì)應(yīng)的非確定的時(shí)間自動(dòng)機(jī)的Di-可重置問題(i=1,2,3).

對(duì)于時(shí)間自動(dòng)機(jī)A=〈L,l0,C,∑,E,F〉,序列w∈((?≥0,∑))*被稱為是:

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

·D2-可重置的,如果對(duì)所有(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).

輸入:非確定的時(shí)間自動(dòng)機(jī);A

詢問:非確定的時(shí)間自動(dòng)機(jī)是否是D1-可重置的(或D2-可重置的,或D3-可重置的)?

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

證明:因?yàn)?Doyen等人證明了完全的非確定的時(shí)間自動(dòng)機(jī)的重置問題在一般情況下是不可判定的[20,21],所以,非確定的時(shí)間自動(dòng)機(jī)是否是D1-可重置的是不可判定的.

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

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

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

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

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

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

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

定理6.完全的非確定時(shí)間自動(dòng)機(jī)的限界重置問題(BOUNDED-RESET)是NEXPTIME-完全的.

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

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

定理7.完全的非確定的單時(shí)鐘時(shí)間自動(dòng)機(jī)的重置問題是Ackermann-完全的.

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

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

6 相關(guān)工作

6.1 有限自動(dòng)機(jī)和其他自動(dòng)機(jī)的重置問題

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

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

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

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

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

6.2 時(shí)間自動(dòng)機(jī)的可達(dá)性問題

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

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

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

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

7 結(jié) 論

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

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

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

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

附錄

引理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),它是單元集.如果對(duì)于n≤|u|,u[n]=(t2,*),那么,u的前綴u[1,n]也是B的一個(gè)仔細(xì)重置序列.由于假設(shè)u是最短的仔細(xì)重置序列,那么,n=|u|且(t2,*)在u中僅出現(xiàn)1次,它位于u的末端.

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

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

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

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

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

引理3的證明:

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

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

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

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

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

N=“對(duì)于輸入w:

(1) 計(jì)算f(w);

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