TY - GEN
T1 - Communicating timed automata
T2 - 18th International Conference on Computer Aided Verification, CAV 2006
AU - Krcal, Pavel
AU - Yi, Wang
PY - 2006
Y1 - 2006
N2 - We study channel systems whose behaviour (sending and receiving messages via unbounded FIFO channels) must follow given timing constraints specifying the execution speeds of the local components. We propose Communicating Timed Automata (CTA) to model such systems. The goal is to study the borderline between decidable and undecidable classes of channel systems in the timed setting. Our technical results include: (1) CTA with one channel without shared states in the form (A1,A2,c12) is equivalent to one-counter machine, implying that verification problems such as checking state reachability and channel boundedness are decidable, and (2) CTA with two channels without sharing states in the form (A1,A 2, A3, c1,2,c2, 3) has the power of Turing machines. Note that in the untimed setting, these systems are no more expressive than finite state machines. This shows that the capability of synchronizing on time makes it substantially more difficult to verify channel systems.
AB - We study channel systems whose behaviour (sending and receiving messages via unbounded FIFO channels) must follow given timing constraints specifying the execution speeds of the local components. We propose Communicating Timed Automata (CTA) to model such systems. The goal is to study the borderline between decidable and undecidable classes of channel systems in the timed setting. Our technical results include: (1) CTA with one channel without shared states in the form (A1,A2,c12) is equivalent to one-counter machine, implying that verification problems such as checking state reachability and channel boundedness are decidable, and (2) CTA with two channels without sharing states in the form (A1,A 2, A3, c1,2,c2, 3) has the power of Turing machines. Note that in the untimed setting, these systems are no more expressive than finite state machines. This shows that the capability of synchronizing on time makes it substantially more difficult to verify channel systems.
UR - https://www.scopus.com/pages/publications/33749830336
U2 - 10.1007/11817963_24
DO - 10.1007/11817963_24
M3 - 会议稿件
AN - SCOPUS:33749830336
SN - 354037406X
SN - 9783540374060
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 249
EP - 262
BT - Computer Aided Verification - 18th International Conference, CAV 2006, Proceedings
PB - Springer Verlag
Y2 - 17 August 2006 through 20 August 2006
ER -