Abstract
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 (A 1,A 2, c 1,2) 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 (A 1,A 2,A 3, c 1,2,c 2,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.
Partially supported by the European Research Training Network GAMES.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)
Abdulla, P.A., Jonsson, B.: Undecidable verification problems for programs with unreliable channels. Information and Computation 130(1), 71–90 (1996)
Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. Information and Computation 127(2), 91–101 (1996)
Bengtsson, J., Jonsson, B., Lilius, J., Yi, W.: Partial order reductions for timed systems. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 485–500. Springer, Heidelberg (1998)
Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30(2), 323–342 (1983)
Cécé, G., Finkel, A.: Verification of programs with half-duplex communication. Information and Computation 202(2), 166–190 (2005)
Cécé, G., Finkel, A., Iyer, S.P.: Unreliable channels are easier to verify than perfect channels. Information and Computation 124(1), 20–31 (1996)
Finkel, A., McKenzie, P.: Verifying identical communicating processes is undecidable. Theoretical Computer Science 174(1-2), 217–230 (1997)
Finkel, A., Iyer, S.P., Sutre, G.: Well-abstracted transition systems: Application to FIFO automata. Information and Computation 181(1), 1–31 (2003)
Genest, B., Muscholl, A., Kuske, D.: A Kleene theorem for a class of communicating automata with effective algorithms. In: Calude, C.S., Calude, E., Dinneen, M.J. (eds.) DLT 2004. LNCS, vol. 3340, pp. 30–48. Springer, Heidelberg (2004)
Krčál, P., Pelánek, R.: On sampled semantics of timed systems. In: Ramanujam, R., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 310–321. Springer, Heidelberg (2005)
Krcal, P., Yi, W.: Communicating timed automata. Technical Report 2006-008, Uppsala University (2006)
Pachl, J.K.: Reachability problems for communicating finite state machines. Technical Report CS-82-12, Department of Computer Science, University of Waterloo (1982)
Pachl, J.K.: Reachability problems for communicating finite state machines. ArXiv Computer Science e-prints, arXiv:cs/0306121 (2003)
Peng, W., Iyer, S.P.: Analysis of a class of communicating finite state machines. Acta Informatica 29(6/7), 422–499 (1992)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Krcal, P., Yi, W. (2006). Communicating Timed Automata: The More Synchronous, the More Difficult to Verify. In: Ball, T., Jones, R.B. (eds) Computer Aided Verification. CAV 2006. Lecture Notes in Computer Science, vol 4144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11817963_24
Download citation
DOI: https://doi.org/10.1007/11817963_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37406-0
Online ISBN: 978-3-540-37411-4
eBook Packages: Computer ScienceComputer Science (R0)