LIPIcs.ICALP.2017.122.pdf
- Filesize: 0.57 MB
- 14 pages
Document
Synchronizability of Communicating Finite State Machines is not Decidable
Authors
-
Part of:
Volume:
44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Colloquium on Automata, Languages, and Programming (ICALP) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2017-07-07
Cite AsGet BibTex
Alain Finkel and Etienne Lozes. Synchronizability of Communicating Finite State Machines is not Decidable. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 122:1-122:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.ICALP.2017.122
https://doi.org/10.4230/LIPIcs.ICALP.2017.122
Abstract
A system of communicating finite state machines is synchronizable if its send trace semantics, i.e. the set of sequences of sendings it can perform, is the same when its communications are FIFO asynchronous and when they are just rendez-vous synchronizations. This property was claimed to be decidable in several conference and journal papers for either mailboxes or peer-to-peer communications, thanks to a form of small model property. In this paper, we show that this small model property does not hold neither for mailbox communications, nor for peer-to-peer communications, therefore the decidability of synchronizability becomes an open question. We close this question for peer-to-peer communications, and we show that synchronizability is actually undecidable. We show that synchronizability is decidable if the topology of communications is an oriented ring. We also show that, in this case, synchronizability implies the absence of unspecified receptions and orphan messages, and the channel-recognizability of the reachability set.
Keywords
- verification
- distributed system
- asynchronous communications
- choreographies
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Samik Basu and Tevfik Bultan. Choreography conformance via synchronizability. In Procs. of WWW 2011, pages 795-804, 2011. URL: http://dx.doi.org/10.1145/1963405.1963516.
- Samik Basu and Tevfik Bultan. On deciding synchronizability for asynchronously communicating systems. Theor. Comput. Sci., 656:60-75, 2016. URL: http://dx.doi.org/10.1016/j.tcs.2016.09.023.
- Samik Basu, Tevfik Bultan, and Meriem Ouederni. Deciding choreography realizability. In Procs. of POPL'12, pages 191-202, 2012. URL: http://dx.doi.org/10.1145/2103656.2103680.
- Samik Basu, Tevfik Bultan, and Meriem Ouederni. Synchronizability for verification of asynchronously communicating systems. In Procs. of VMCAI 2012, 2012. URL: http://dx.doi.org/10.1007/978-3-642-27940-9_5.
- Bernard Boigelot and Patrice Godefroid. Symbolic verification of communication protocols with infinite state spaces using qdds. Formal Methods in System Design, 14(3):237-255, 1999. URL: http://dx.doi.org/10.1023/A:1008719024240.
- Daniel Brand and Pitro Zafiropulo. On communicating finite-state machines. J. ACM, 30(2):323-342, April 1983. URL: http://dx.doi.org/10.1145/322374.322380.
- Gerald Cécé and Alain Finkel. Verification of programs with half-duplex communication. Inf. Comput., 202(2):166-190, 2005. URL: http://dx.doi.org/10.1016/j.ic.2005.05.006.
- Pierre Chambart and Philippe Schnoebelen. Mixing lossy and perfect fifo channels. In Procs. of CONCUR 2008, pages 340-355, 2008. URL: http://dx.doi.org/10.1007/978-3-540-85361-9_28.
- Lorenzo Clemente, Frédéric Herbreteau, and Grégoire Sutre. Decidable topologies for communicating automata with FIFO and bag channels. In Procs. of CONCUR 2014, pages 281-296, 2014. URL: http://dx.doi.org/10.1007/978-3-662-44584-6_20.
- Pierre-Malo Deniélou and Nobuko Yoshida. Multiparty session types meet communicating automata. In Procs. of ESOP 2012, pages 194-213, 2012. URL: http://dx.doi.org/10.1007/978-3-642-28869-2_10.
- Alain Finkel and Etienne Lozes. Synchronizability of communicating finite state machines is not decidable. Technical report, arXiv, 2017. URL: https://arxiv.org/abs/1702.07213.
- Blaise Genest, Dietrich Kuske, and Anca Muscholl. A kleene theorem and model checking algorithms for existentially bounded communicating automata. Inf. Comput., 204(6):920-956, 2006. URL: http://dx.doi.org/10.1016/j.ic.2006.01.005.
- Alexander Heußner, Tristan Le Gall, and Grégoire Sutre. Mcscm: A general framework for the verification of communicating machines. In Procs. of TACAS 2012, pages 478-484, 2012. URL: http://dx.doi.org/10.1007/978-3-642-28756-5_34.
- Alexander Heußner, Jérôme Leroux, Anca Muscholl, and Grégoire Sutre. Reachability analysis of communicating pushdown systems. Logical Methods in Computer Science, 8(3), 2012. URL: http://dx.doi.org/10.2168/LMCS-8(3:23)2012.
- Salvatore La Torre, Parthasarathy Madhusudan, and Gennaro Parlato. Context-bounded analysis of concurrent queue systems. In Procs. of TACAS 2008, pages 299-314, 2008. URL: http://dx.doi.org/10.1007/978-3-540-78800-3_21.
- Rajit Manohar and Alain J. Martin. Slack elasticity in concurrent computing. In Procs. of Math. of Prog. Construction (MPC'98), pages 272-285, 1998. URL: http://dx.doi.org/10.1007/BFb0054295.
-
Jan Pachl. Protocol description and analysis based on a state transition model with channel expressions. In Proc. of Protocol Specification, Testing, and Verification, VII, 1987.
- Stephen F. Siegel. Efficient verification of halting properties for MPI programs with wildcard receives. In Procs. of VMCAI 2005, pages 413-429, 2005. URL: http://dx.doi.org/10.1007/978-3-540-30579-8_27.
- Sarvani Vakkalanka, Anh Vo, Ganesh Gopalakrishnan, and Robert M. Kirby. Precise dynamic analysis for slack elasticity: Adding buffering without adding bugs. In Procs. of EuroMPI 2010, pages 152-159, 2010. URL: http://dx.doi.org/10.1007/978-3-642-15646-5_16.