Decision Problems for Timed Automata : A Survey
作者： Rajeev Alur , P. Madhusudan
DOI: 10.1007/978-3-540-30080-9_1
关键词:
摘要: Finite automata and regular languages have been useful in a wide variety of problems computing, communication control, including formal modeling verification. Traditional do not admit an explicit time, consequently, timed [2] were introduced as notation to model the behavior real-time systems. Timed accept consisting sequences events tagged with their occurrence times. Over years, formalism has extensively studied leading many results establishing connections circuits logic, much progress made developing verification algorithms, heuristics, tools. This paper provides survey theoretical concerning decision reachability, language inclusion equivalence for its variants, some new proofs comparisons. We conclude discussion open problems.
springer.com
core.ac.uk
mimuw.edu.pl 参考文章(44)
Vineet Gupta, Thomas A. Henzinger, Radha Jagadeesan, Robust Timed Automata HART '97 Proceedings of the International Workshop on Hybrid and Real-Time Systems. pp. 331- 345 ,(1997) , 10.1007/BFB0014736
Vincent Danos, Jean Krivine, Reversible Communicating Systems CONCUR 2004 - Concurrency Theory. ,vol. 3170, pp. 292- 307 ,(2004) , 10.1007/978-3-540-28644-8_19
Rajeev Alur, Robert P. Kurshan, Timing analysis in COSPAN Proceedings of the DIMACS/SYCON workshop on Hybrid systems III : verification and control: verification and control. pp. 220- 231 ,(1996) , 10.1007/BFB0020948
Stavros Tripakis, Folk Theorems on the Determinization and Minimization of Timed Automata formal modeling and analysis of timed systems. pp. 182- 188 ,(2003) , 10.1007/978-3-540-40903-8_15
Hybrid Systems: Computation and Control. Defense Technical Information Center. ,(1998) , 10.1007/3-540-64358-3
Martin De Wulf, Laurent Doyen, Nicolas Markey, Jean-François Raskin, Robustness and Implementability of Timed Automata Lecture Notes in Computer Science. ,vol. 3253, pp. 118- 133 ,(2004) , 10.1007/978-3-540-30206-3_10
Joseph S. Miller, Decidability and Complexity Results for Timed Automata and Semi-linear Hybrid Automata acm international conference hybrid systems computation and control. pp. 296- 309 ,(2000) , 10.1007/3-540-46430-1_26
Thomas A. Henzinger, Jean-François Raskin, Robust Undecidability of Timed and Hybrid Systems acm international conference hybrid systems computation and control. ,vol. 1790, pp. 145- 159 ,(2000) , 10.1007/3-540-46430-1_15
Rajeev Alur, Kousha Etessami, P. Madhusudan, A Temporal Logic of Nested Calls and Returns tools and algorithms for construction and analysis of systems. ,vol. 2988, pp. 467- 481 ,(2004) , 10.1007/978-3-540-24730-2_35
F. Laroussinie, N. Markey, Ph. Schnoebelen, Model Checking Timed Automata with One or Two Clocks CONCUR 2004 - Concurrency Theory. pp. 387- 401 ,(2004) , 10.1007/978-3-540-28644-8_25