TY - CHAP
T1 - Decision Problems for Timed Automata
T2 - A Survey
AU - Alur, Rajeev
AU - Madhusudan, P.
PY - 2004
Y1 - 2004
N2 - Finite automata and regular languages have been useful in a wide variety of problems in computing, communication and control, including formal modeling and verification. Traditional automata do not admit an explicit modeling of time, and consequently, timed automata [2] were introduced as a formal notation to model the behavior of real-time systems. Timed automata accept timed languages consisting of sequences of events tagged with their occurrence times. Over the years, the formalism has been extensively studied leading to many results establishing connections to circuits and logic, and much progress has been made in developing verification algorithms, heuristics, and tools. This paper provides a survey of the theoretical results concerning decision problems of reachability, language inclusion and language equivalence for timed automata and its variants, with some new proofs and comparisons. We conclude with a discussion of some open problems.
AB - Finite automata and regular languages have been useful in a wide variety of problems in computing, communication and control, including formal modeling and verification. Traditional automata do not admit an explicit modeling of time, and consequently, timed automata [2] were introduced as a formal notation to model the behavior of real-time systems. Timed automata accept timed languages consisting of sequences of events tagged with their occurrence times. Over the years, the formalism has been extensively studied leading to many results establishing connections to circuits and logic, and much progress has been made in developing verification algorithms, heuristics, and tools. This paper provides a survey of the theoretical results concerning decision problems of reachability, language inclusion and language equivalence for timed automata and its variants, with some new proofs and comparisons. We conclude with a discussion of some open problems.
UR - http://www.scopus.com/inward/record.url?scp=35048817380&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=35048817380&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-30080-9_1
DO - 10.1007/978-3-540-30080-9_1
M3 - Chapter
AN - SCOPUS:35048817380
SN - 9783540230687
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 1
EP - 24
BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
A2 - Bernardo, Marco
A2 - Corradini, Flavio
PB - Springer
ER -