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

• 作者: 吴理华 朱凯 毋国庆 袁梦霆
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 时间自动机 重置序列 归约 计算复杂性
• 年，卷（期）: 2019,（7）
• 所属期刊栏目: 软件形式化验证专题
• 页码范围: 2033-2051
• 页数: 19页
• 分类号: TP301
• 字数: 18755字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.005757

摘要

自动机的重置序列也称为同步序列,具有以下特性:有限自动机通过运行重置序列w,可从任意一个未知的或无法观测到的状态q0到达某个特定状态qw.这仅依赖于w,而与开始运行w时的状态q0无关.这一特性可用于部分可观察的复杂系统的自动恢复,而无需重启,甚至有时不能重启.基于此,重置问题自出现以来便得到关注和持续研究.最近几年,它被扩展到可以描述诸如分布式、嵌入式实时系统等复杂系统的无限状态模型上,比如时间自动机和寄存器自动机等.以时间自动机的重置问题的计算复杂性为研究对象,发现重置问题与可达性问题有着紧密的联系.主要贡献是:(1)利用时间自动机可达性问题的最新成果,完善完全的确定的时间自动机重置问题的计算复杂性结论;(2)对部分规约的确定的时间自动机,研究得出,即使在输入字母表大小减至2的情况下,其复杂性仍是PSPACE-完全的;特别地,在单时钟情况下是NLOGSPACE-完全的;(3)对完全的非确定的时间自动机,研究得出其Di=可重置问题(i=1,2,3)是不可判定的,其重置问题与非确定的寄存器自动机重置问题在指数时间可以相互归约,通过证明指数时间归约相对高复杂性类具有封闭性,利用非确定的寄存器自动机的结论得出单时钟的时间自动机的重置问题是Ackermann-完全的、限界的重置问题是NEXPTIME-完全的.这些复杂性结论,说明关于时间自动机的重置问题大都是难解的,一方面,为时间系统的可重置性的检测和求解奠定坚实的理论基础,另一方面,为以后寻找具有高效算法的特殊结构的时间系统(即具有高效算法的问题子类)给予理论指导.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	毋国庆	武汉大学计算机学院	72	470	12.0	17.0
2	袁梦霆	武汉大学计算机学院	13	39	3.0	6.0
3	朱凯	武汉大学计算机学院	11	9	2.0	2.0
7	吴理华	华南农业大学数学与信息学院	4	3	1.0	1.0