有关时间自动机重置的若干问题的计算复杂性
|
摘要
自动机的重置序列也称为同步序列,具有以下特性:有限自动机通过运行重置序列w,可从任意一个未知的或无法观测到的状态q0到达某个特定状态qw.这仅依赖于w,而与开始运行w时的状态q0无关.这一特性可用于部分可观察的复杂系统的自动恢复,而无需重启,甚至有时不能重启.基于此,重置问题自出现以来便得到关注和持续研究.最近几年,它被扩展到可以描述诸如分布式、嵌入式实时系统等复杂系统的无限状态模型上,比如时间自动机和寄存器自动机等.以时间自动机的重置问题的计算复杂性为研究对象,发现重置问题与可达性问题有着紧密的联系.主要贡献是:(1)利用时间自动机可达性问题的最新成果,完善完全的确定的时间自动机重置问题的计算复杂性结论;(2)对部分规约的确定的时间自动机,研究得出,即使在输入字母表大小减至2的情况下,其复杂性仍是PSPACE-完全的;特别地,在单时钟情况下是NLOGSPACE-完全的;(3)对完全的非确定的时间自动机,研究得出其Di-可重置问题(i=1,2,3)是不可判定的,其重置问题与非确定的寄存器自动机重置问题在指数时间可以相互归约,通过证明指数时间归约相对高复杂性类具有封闭性,利用非确定的寄存器自动机的结论得出单时钟的时间自动机的重置问题是Ackermann-完全的、限界的重置问题是NEXPTIME-完全的.这些复杂性结论,说明关于时间自动机的重置问题大都是难解的,一方面,为时间系统的可重置性的检测和求解奠定坚实的理论基础,另一方面,为以后寻找具有高效算法的特殊结构的时间系统(即具有高效算法的问题子类)给予理论指导.
The reset sequences of finite automata, also known as the synchronizing sequences, have a characteristic: a finite automaton can reach a certain state q_w by running a reset sequence from any unknown or unobservable state q_0. This is dependent only on the reset sequence w itself, not on the state q_0 of the finite automaton at the beginning of running the sequence w. It can be used to restore the running partially observable and complex systems automatically that needs no resetting, and sometimes even that cannot reset. Therefore,the reset problem has been paid attention to since it emerged and has been studied continuously. Recently, it has extended to infinite state models that can describe the complex systems, including distributed and embedded real-time systems, such as timed automata, register automata, etc. In this work, the computational complexity of several problems for the resetting timed automata is studied, and the strong connection between resettability problem and reachability problem for timed automata is found. The main contribution includes:(1) the complexity of the problem for resetting the complete and deterministic timed automata is updated more precisely with the recent achievements in reachability problem for timed automata;(2) the complexity of the problem for resetting the partially specified timed automata is studied. Even if the size of input alphabet is decreased to 2, it is still PSPACE-complete, and in the case of single clock, it is NLOGSPACE-complete;(3) for the complete and nondeterministic timed automata, Di-resetting problems(i=1,2,3) are all undecidable.The resetting problem for nondeterministic register automata and nondeterministic timed automata can be inter-reduced in exponential time, and the reduction in exponential time is closed for relatively high computational complexity classes. Therefore, it concludes that the problem for resetting it in single clock case is Ackermann-complete, and that bounded version is NEXPTIME-complete from the results on corresponding nondeterministic register automata. These conclusions show that most of resetting problems for timed automata are intractable. On the one hand, they make a solid theoretical foundation for checking and solving the resettability of the timed systems, on the other hand, they guide to seek for some subclasses of real time system which have particular structure and effective algorithms for solving it.
The reset sequences of finite automata, also known as the synchronizing sequences, have a characteristic: a finite automaton can reach a certain state q_w by running a reset sequence from any unknown or unobservable state q_0. This is dependent only on the reset sequence w itself, not on the state q_0 of the finite automaton at the beginning of running the sequence w. It can be used to restore the running partially observable and complex systems automatically that needs no resetting, and sometimes even that cannot reset. Therefore,the reset problem has been paid attention to since it emerged and has been studied continuously. Recently, it has extended to infinite state models that can describe the complex systems, including distributed and embedded real-time systems, such as timed automata, register automata, etc. In this work, the computational complexity of several problems for the resetting timed automata is studied, and the strong connection between resettability problem and reachability problem for timed automata is found. The main contribution includes:(1) the complexity of the problem for resetting the complete and deterministic timed automata is updated more precisely with the recent achievements in reachability problem for timed automata;(2) the complexity of the problem for resetting the partially specified timed automata is studied. Even if the size of input alphabet is decreased to 2, it is still PSPACE-complete, and in the case of single clock, it is NLOGSPACE-complete;(3) for the complete and nondeterministic timed automata, Di-resetting problems(i=1,2,3) are all undecidable.The resetting problem for nondeterministic register automata and nondeterministic timed automata can be inter-reduced in exponential time, and the reduction in exponential time is closed for relatively high computational complexity classes. Therefore, it concludes that the problem for resetting it in single clock case is Ackermann-complete, and that bounded version is NEXPTIME-complete from the results on corresponding nondeterministic register automata. These conclusions show that most of resetting problems for timed automata are intractable. On the one hand, they make a solid theoretical foundation for checking and solving the resettability of the timed systems, on the other hand, they guide to seek for some subclasses of real time system which have particular structure and effective algorithms for solving it.
引文
[1]?erny J.Poznámka k-homogénnym eksperimentom s kone?nymi automata mi.Mathematicko-fyzikalny ?asopis Slovensk,Akad.Vied,1964,14(3):208-216(in Slovak).
[2]Benenson Y,Adar R,Paz-Elizur T,Livneh Z,Shapiro E.DNA molecule provides a computing machine with both data and fuel.Proc.of the National Academy of Sciences,2003,100(5):2191-2196.[doi:10.1073/pnas.0535624100]
[3]Benenson Y,Paz-Elizur T,Adar R,Keinan E,Livneh Z,Shapiro E.Programmable and autonomous computing machine made of biomolecules.Nature,2001,414(6862):430.[doi:10.1038/35106533]
[4]Stojanovic MN,Stefanovic D.A deoxyribozyme-based molecular automaton.Nature Biotechnology,2003,21(9):1069-1074.[doi:10.1038/nbt862]
[5]Natarajan BK.An algorithmic approach to the automated design of parts orienteers.In:Proc.of the 27th Annual Symp.on Foundations of Computer Science.IEEE,1986.132-142.[doi:10.1109/SFCS.1986.5]
[6]Berlinkov MV,Szykula M.Algebraic synchronization criterion and computing reset words.Information Sciences,2016,718-730.[doi:10.1016/j.ins.2016.07.049]
[7]Song F,Wu ZL.Survey on formal models to reason about infinite data values.Ruan Jian Xue Bao/Journal of Software,2016,27(3):1-9(in Chinese with English abstract).http://www.jos.org.cn/1000-9825/4989.htm[doi:10.13328/j.cnki.jos.004989]
[8]Chatterjee K,Doyen L.Computation tree logic for synchronization properties.In:Proc.of the LIPIcs-Leibniz Int’l in Informatics.Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik,2016.55.[doi:10.4230/LIPIcs.ICALP.2016.98]
[9]Alur R,Dill DL.A theory of timed automata.Theoretical Computer Science,1994,126(2):183-235.[doi:10.1016/0304-3975(94)90010-8]
[10]Behrmann G,David A,Larsen KG,H?kansson J,Petterson P,Yi W,Hendriks M.UPPAAL 4.0.In:Proc.of the 3rd Int’l Conf.on Quantitative Evaluation of Systems,2006(QEST 2006).IEEE,2006.125-126.[doi:10.1109/QEST.2006.59]
[11]Bengtsson J,Yi W.Timed automata:Semantics,algorithms and tools.In:Advanced Course on Petri Nets.Berlin,Heidelberg:Springer-Verlag,2003.87-124.[doi:10.1007/978-3-540-27755-2_3]
[12]Bouyer P,Fahrenberg U,Larsen KG,Markey N,Ouaknine J,Worrell J.Model checking real-time systems.In:Handbook of Model Checking.Cham:Springer-Verlag,2018.1001-1046.[doi:10.1007/978-3-319-10575-8_29]
[13]Herbreteau F,Srivathsan B,Walukiewicz I.Lazy abstractions for timed automata.In:Proc.of the 24th Int’l Conf.on Computer Aded Verification(CAV 2013).Springer-Verlag,2013.990-1005.[doi:10.1007/978-3-642-39799-8_71]
[14]Herbreteau F,Srivathsan B,Walukiewicz I.Better abstractions for timed automata.Information and Computation,2016,251:67-90.[doi:10.1016/j.ic.2016.07.004]
[15]Tóth T,Hajduá,V?r?s A,Micskei Z,Majzik I.Theta:A framework for abstraction refinement-based model checking.In:Proc.of the Formal Methods in Computer Aided Design(FMCAD).IEEE,2017.176-179.[doi:10.23919/FMCAD.2017.8102257]
[16]Zhao J,Li X,Zheng T,Zheng G.Removing irrelevant atomic formulas for checking timed automata efficiently.In:Proc.of the Int’l Conf.on Formal Modeling and Analysis of Timed Systems.Berlin,Heidelberg:Springer-Verlag,2003.34-45.[doi:10.1007/978-3-540-40903-8_4]
[17]Zhao J,Li X,Zheng G.A quadratic-time DBM-based successor algorithm for checking timed automata.Information Processing Letters,2005,96(3):101-105.[doi:10.1016/j.ipl.2005.05.027]
[18]Lin H,Yi W.A proof system for timed automata.In:Proc.of the Int’l Conf.on Foundations of Software Science and Computation Structures.Berlin,Heidelberg:Springer-Verlag,2000.208-222.[doi:10.1007/3-540-46432-8_14]
[19]Lin H,Yi W.Axiomatising timed automata.Acta informatica,2002,38(4):277-305.[doi:10.1007/s236-002-8035-2]
[20]Doyen L,Juhl L,Larsen KG,Markey N,Shirmohammadi M.Synchronizing words for weighted and timed automata.In:Proc.of the Int’l Conf.on Foundation of Software Technology and Theoretical Computer Science.2014.121-132.[doi:10.4230/LIPIcs.FSTTCS.2014.121]
[21]Doyen L,Juhl L,Larsen KG,Markey N,Shirmohammadi M.Synchronizing words for timed and weighted automata.Research Report,LSV-13-15(version 2),Laboratoire Spécification et Vérification,ENS Cachan,France,2014.28.
[22]Eppstein D.Reset sequences for monotonic automata.SIAM Journal on Computing,1990,19(3):500-510.[doi:10.1137/0219033]
[23]Laroussinie F,Markey N,Schnoebelen P.Model checking timed automata with one or two clocks.In:Proc.of the Int’l Conf.on Concurrency Theory.Berlin,Heidelberg:Springer-Verlag,2004.387-401.[doi:10.1007/978-3-540-28644-8_25]
[24]Fearnley J,Jurdziński M.Reachability in two-clock timed automata is PSPACE-complete.Information and Computation,2015,243:26-36.[doi:10.1016/j.ic.2014.12.004]
[25]Courcoubetis C,Yannakakis M.Minimum and maximum delay problems in real-time systems.Formal Methods in System Design,1992,1(4):385-415.[doi:10.1007/BF00709157]
[26]Haase C,Ouaknine J,Worrell J.On the relationship between reachability problems in timed and counter automata.In:Proc.of the Int’l Workshop on Reachability Problems.Berlin,Heidelberg:Springer-Verlag,2012.54-65.[doi:10.1007/978-3-642-33512-9_6]
[27]Haase C,Ouaknine J,Worrell J.Relating reachability problems in timed and counter automata.Fundamenta Informaticae,2016,143(3-4):317-338.[doi:10.3233/FI-2016-1316]
[28]Martyugin P.Complexity of problems concerning carefully synchronizing words for PFA and directing words for NFA.In:Proc.of the Computer Science Symp.in Russia.2010.288-302.[doi:10.1007/978-3-642-13182-0_27]
[29]Martyugin P.Computational complexity of certain problems related to carefully synchronizing words for partial automata and directing words for nondeterministic automata.Theory of Computing Systems,2014,54(2):293-304.[doi:10.1007/s00224-013-9516-6]
[30]Babari P,Quaas K,Shirmohammadi M.Synchronizing data words for register automata.In:Proc.of the LIPIcs-Leibniz Int’l in Informatics.Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik,2016.58.[doi:10.4230/LIPIcs.MFCS.2016.15]
[31]Figueira D,Hofman P,Lasota S.Relating timed and register automata.Mathematical Structures in Computer Science,2016,26(6):993-1021.[doi:10.1017/S0960129514000322]
[32]Imreh B,Steinby M.Directable nondeterministic automata.Acta Cybernetica,1999,14(1):105-115.
[33]Olschewski J,Ummels M.The complexity of finding reset words in finite automata.Mathematical Foundations of Computer Science,2010,568-579.[doi:10.1007/978-3-642-15155-2_50]
[34]Pin J.On two combinatorial problems arising from automata theory.North-holland Mathematics Studies,1983,535-548.[doi:10.1016/S0304-0208(08)73432-7]
[35]Berlinkov MV.Approximating the minimum length of synchronizing words is hard.In:Proc.of the Computer Science Symp.in Russia.2010.37-47.[doi:10.1007/978-3-642-13182-0_4]
[36]Gazdag Z,Iván S,Nagy-Gy?rgy J.Improved upper bounds on synchronizing nondeterministic automata.Information Processing Letters,2009,109(17):986-990.[doi:10.1016/j.ipl.2009.05.007]
[37]Doyen L,Massart T,Shirmohammadi M.Infinite synchronizing words for probabilistic automata.In:Proc.of the Int’l Symp.on Mathematical Foundations of Computer Science.Berlin,Heidelberg:Springer-Verlag,2011.278-289.[doi:10.1007/978-3-642-22993-0_27]
[38]Caucal D.Synchronization of pushdown automata.In:Proc.of the Int’l Conf.on Developments in Language Theory.Berlin,Heidelberg:Springer-Verlag,2006.120-132.[doi:10.1007/11779148_12]
[39]Chistikov D,Martyugin P,Shirmohammadi M.Synchronizing automata over nested words.In:Proc.of the Int’l Conf.on Foundations of Software Science and Computation Structures.Berlin,Heidelberg:Springer-Verlag,2016.252-26.[doi:10.1007/978-3-662-49630-5_15]
[40]Quaas K,Shirmohammadi M,Worrell J.Revisiting reachability in timed automata.In:Proc.of the 32nd Annual ACM/IEEE Symp.on Logic in Computer Science(LICS).IEEE,2017.1-12.[doi:10.1109/LICS.2017.8005098]
[41]Bersani MM,Rossi M,San Pietro P.A logical characterization of timed regular languages.Theoretical Computer Science,2017,658:46-59.[doi:10.1016/j.tcs.2016.07.020]
[42]Maler O,Nickovic D,Pnueli A.From MITL to timed automata.In:Proc.of the Int’l Conf.on Formal Modeling and Analysis of Timed Systems.Berlin,Heidelberg:Springer-Verlag,2006.274-289.[doi:10.1007/11867340_20]
[43]Ni?kovi?D,Piterman N.From MTL to deterministic timed automata.In:Proc.of the Int’l Conf.on Formal Modeling and Analysis of Timed Systems.Berlin,Heidelberg:Springer-Verlag,2010.152-167.[doi:10.1007/978-3-642-15297-9_13]
[44]Papadimitriou CH.Computational Complexity.John Wiley and Sons Ltd.,2003.
[45]Schmitz S.Complexity hierarchies beyond elementary.ACM Trans.on Computation Theory(TOCT),2016,8(1):3:1-3:36.[doi:10.1145/2858784]
[7]宋富,吴志林.面向无穷数据的形式模型综述.软件学报,2016,27(3):1–9. http://www.jos.org.cn/1000-9825/4989.htm[doi:10.13328/j.cnki.jos.004989]
[2]Benenson Y,Adar R,Paz-Elizur T,Livneh Z,Shapiro E.DNA molecule provides a computing machine with both data and fuel.Proc.of the National Academy of Sciences,2003,100(5):2191-2196.[doi:10.1073/pnas.0535624100]
[3]Benenson Y,Paz-Elizur T,Adar R,Keinan E,Livneh Z,Shapiro E.Programmable and autonomous computing machine made of biomolecules.Nature,2001,414(6862):430.[doi:10.1038/35106533]
[4]Stojanovic MN,Stefanovic D.A deoxyribozyme-based molecular automaton.Nature Biotechnology,2003,21(9):1069-1074.[doi:10.1038/nbt862]
[5]Natarajan BK.An algorithmic approach to the automated design of parts orienteers.In:Proc.of the 27th Annual Symp.on Foundations of Computer Science.IEEE,1986.132-142.[doi:10.1109/SFCS.1986.5]
[6]Berlinkov MV,Szykula M.Algebraic synchronization criterion and computing reset words.Information Sciences,2016,718-730.[doi:10.1016/j.ins.2016.07.049]
[7]Song F,Wu ZL.Survey on formal models to reason about infinite data values.Ruan Jian Xue Bao/Journal of Software,2016,27(3):1-9(in Chinese with English abstract).http://www.jos.org.cn/1000-9825/4989.htm[doi:10.13328/j.cnki.jos.004989]
[8]Chatterjee K,Doyen L.Computation tree logic for synchronization properties.In:Proc.of the LIPIcs-Leibniz Int’l in Informatics.Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik,2016.55.[doi:10.4230/LIPIcs.ICALP.2016.98]
[9]Alur R,Dill DL.A theory of timed automata.Theoretical Computer Science,1994,126(2):183-235.[doi:10.1016/0304-3975(94)90010-8]
[10]Behrmann G,David A,Larsen KG,H?kansson J,Petterson P,Yi W,Hendriks M.UPPAAL 4.0.In:Proc.of the 3rd Int’l Conf.on Quantitative Evaluation of Systems,2006(QEST 2006).IEEE,2006.125-126.[doi:10.1109/QEST.2006.59]
[11]Bengtsson J,Yi W.Timed automata:Semantics,algorithms and tools.In:Advanced Course on Petri Nets.Berlin,Heidelberg:Springer-Verlag,2003.87-124.[doi:10.1007/978-3-540-27755-2_3]
[12]Bouyer P,Fahrenberg U,Larsen KG,Markey N,Ouaknine J,Worrell J.Model checking real-time systems.In:Handbook of Model Checking.Cham:Springer-Verlag,2018.1001-1046.[doi:10.1007/978-3-319-10575-8_29]
[13]Herbreteau F,Srivathsan B,Walukiewicz I.Lazy abstractions for timed automata.In:Proc.of the 24th Int’l Conf.on Computer Aded Verification(CAV 2013).Springer-Verlag,2013.990-1005.[doi:10.1007/978-3-642-39799-8_71]
[14]Herbreteau F,Srivathsan B,Walukiewicz I.Better abstractions for timed automata.Information and Computation,2016,251:67-90.[doi:10.1016/j.ic.2016.07.004]
[15]Tóth T,Hajduá,V?r?s A,Micskei Z,Majzik I.Theta:A framework for abstraction refinement-based model checking.In:Proc.of the Formal Methods in Computer Aided Design(FMCAD).IEEE,2017.176-179.[doi:10.23919/FMCAD.2017.8102257]
[16]Zhao J,Li X,Zheng T,Zheng G.Removing irrelevant atomic formulas for checking timed automata efficiently.In:Proc.of the Int’l Conf.on Formal Modeling and Analysis of Timed Systems.Berlin,Heidelberg:Springer-Verlag,2003.34-45.[doi:10.1007/978-3-540-40903-8_4]
[17]Zhao J,Li X,Zheng G.A quadratic-time DBM-based successor algorithm for checking timed automata.Information Processing Letters,2005,96(3):101-105.[doi:10.1016/j.ipl.2005.05.027]
[18]Lin H,Yi W.A proof system for timed automata.In:Proc.of the Int’l Conf.on Foundations of Software Science and Computation Structures.Berlin,Heidelberg:Springer-Verlag,2000.208-222.[doi:10.1007/3-540-46432-8_14]
[19]Lin H,Yi W.Axiomatising timed automata.Acta informatica,2002,38(4):277-305.[doi:10.1007/s236-002-8035-2]
[20]Doyen L,Juhl L,Larsen KG,Markey N,Shirmohammadi M.Synchronizing words for weighted and timed automata.In:Proc.of the Int’l Conf.on Foundation of Software Technology and Theoretical Computer Science.2014.121-132.[doi:10.4230/LIPIcs.FSTTCS.2014.121]
[21]Doyen L,Juhl L,Larsen KG,Markey N,Shirmohammadi M.Synchronizing words for timed and weighted automata.Research Report,LSV-13-15(version 2),Laboratoire Spécification et Vérification,ENS Cachan,France,2014.28.
[22]Eppstein D.Reset sequences for monotonic automata.SIAM Journal on Computing,1990,19(3):500-510.[doi:10.1137/0219033]
[23]Laroussinie F,Markey N,Schnoebelen P.Model checking timed automata with one or two clocks.In:Proc.of the Int’l Conf.on Concurrency Theory.Berlin,Heidelberg:Springer-Verlag,2004.387-401.[doi:10.1007/978-3-540-28644-8_25]
[24]Fearnley J,Jurdziński M.Reachability in two-clock timed automata is PSPACE-complete.Information and Computation,2015,243:26-36.[doi:10.1016/j.ic.2014.12.004]
[25]Courcoubetis C,Yannakakis M.Minimum and maximum delay problems in real-time systems.Formal Methods in System Design,1992,1(4):385-415.[doi:10.1007/BF00709157]
[26]Haase C,Ouaknine J,Worrell J.On the relationship between reachability problems in timed and counter automata.In:Proc.of the Int’l Workshop on Reachability Problems.Berlin,Heidelberg:Springer-Verlag,2012.54-65.[doi:10.1007/978-3-642-33512-9_6]
[27]Haase C,Ouaknine J,Worrell J.Relating reachability problems in timed and counter automata.Fundamenta Informaticae,2016,143(3-4):317-338.[doi:10.3233/FI-2016-1316]
[28]Martyugin P.Complexity of problems concerning carefully synchronizing words for PFA and directing words for NFA.In:Proc.of the Computer Science Symp.in Russia.2010.288-302.[doi:10.1007/978-3-642-13182-0_27]
[29]Martyugin P.Computational complexity of certain problems related to carefully synchronizing words for partial automata and directing words for nondeterministic automata.Theory of Computing Systems,2014,54(2):293-304.[doi:10.1007/s00224-013-9516-6]
[30]Babari P,Quaas K,Shirmohammadi M.Synchronizing data words for register automata.In:Proc.of the LIPIcs-Leibniz Int’l in Informatics.Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik,2016.58.[doi:10.4230/LIPIcs.MFCS.2016.15]
[31]Figueira D,Hofman P,Lasota S.Relating timed and register automata.Mathematical Structures in Computer Science,2016,26(6):993-1021.[doi:10.1017/S0960129514000322]
[32]Imreh B,Steinby M.Directable nondeterministic automata.Acta Cybernetica,1999,14(1):105-115.
[33]Olschewski J,Ummels M.The complexity of finding reset words in finite automata.Mathematical Foundations of Computer Science,2010,568-579.[doi:10.1007/978-3-642-15155-2_50]
[34]Pin J.On two combinatorial problems arising from automata theory.North-holland Mathematics Studies,1983,535-548.[doi:10.1016/S0304-0208(08)73432-7]
[35]Berlinkov MV.Approximating the minimum length of synchronizing words is hard.In:Proc.of the Computer Science Symp.in Russia.2010.37-47.[doi:10.1007/978-3-642-13182-0_4]
[36]Gazdag Z,Iván S,Nagy-Gy?rgy J.Improved upper bounds on synchronizing nondeterministic automata.Information Processing Letters,2009,109(17):986-990.[doi:10.1016/j.ipl.2009.05.007]
[37]Doyen L,Massart T,Shirmohammadi M.Infinite synchronizing words for probabilistic automata.In:Proc.of the Int’l Symp.on Mathematical Foundations of Computer Science.Berlin,Heidelberg:Springer-Verlag,2011.278-289.[doi:10.1007/978-3-642-22993-0_27]
[38]Caucal D.Synchronization of pushdown automata.In:Proc.of the Int’l Conf.on Developments in Language Theory.Berlin,Heidelberg:Springer-Verlag,2006.120-132.[doi:10.1007/11779148_12]
[39]Chistikov D,Martyugin P,Shirmohammadi M.Synchronizing automata over nested words.In:Proc.of the Int’l Conf.on Foundations of Software Science and Computation Structures.Berlin,Heidelberg:Springer-Verlag,2016.252-26.[doi:10.1007/978-3-662-49630-5_15]
[40]Quaas K,Shirmohammadi M,Worrell J.Revisiting reachability in timed automata.In:Proc.of the 32nd Annual ACM/IEEE Symp.on Logic in Computer Science(LICS).IEEE,2017.1-12.[doi:10.1109/LICS.2017.8005098]
[41]Bersani MM,Rossi M,San Pietro P.A logical characterization of timed regular languages.Theoretical Computer Science,2017,658:46-59.[doi:10.1016/j.tcs.2016.07.020]
[42]Maler O,Nickovic D,Pnueli A.From MITL to timed automata.In:Proc.of the Int’l Conf.on Formal Modeling and Analysis of Timed Systems.Berlin,Heidelberg:Springer-Verlag,2006.274-289.[doi:10.1007/11867340_20]
[43]Ni?kovi?D,Piterman N.From MTL to deterministic timed automata.In:Proc.of the Int’l Conf.on Formal Modeling and Analysis of Timed Systems.Berlin,Heidelberg:Springer-Verlag,2010.152-167.[doi:10.1007/978-3-642-15297-9_13]
[44]Papadimitriou CH.Computational Complexity.John Wiley and Sons Ltd.,2003.
[45]Schmitz S.Complexity hierarchies beyond elementary.ACM Trans.on Computation Theory(TOCT),2016,8(1):3:1-3:36.[doi:10.1145/2858784]
[7]宋富,吴志林.面向无穷数据的形式模型综述.软件学报,2016,27(3):1–9. http://www.jos.org.cn/1000-9825/4989.htm[doi:10.13328/j.cnki.jos.004989]