Synchronizability of Communicating Finite State Machines is not Decidable

Authors Alain Finkel, Etienne Lozes



PDF
Thumbnail PDF

File

LIPIcs.ICALP.2017.122.pdf
  • Filesize: 0.57 MB
  • 14 pages

Document Identifiers

Author Details

Alain Finkel
Etienne Lozes

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

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)
    0
    PDF Downloads

References

  1. 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.
  2. 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.
  3. 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.
  4. 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.
  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.
  6. 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.
  7. 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.
  8. 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.
  9. 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.
  10. 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.
  11. 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.
  12. 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.
  13. 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.
  14. 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.
  15. 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.
  16. 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.
  17. 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. Google Scholar
  18. 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.
  19. 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.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail