有关时间自动机重置的若干问题的计算复杂性*

朱 凯, 毋国庆, 吴理华, 袁梦霆

1(武汉大学 计算机学院,湖北 武汉 430072)

2(华南农业大学 数学与信息学院,广东 广州 510642)

1 引 言

有限自动机的重置(或同步)问题[1],最早由Černý在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,给出其重置序列的最短长度的上界.其中,著名的 Černý猜想[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],显然,它相对指数时间归约是封闭的.