Multiparty half-duplex systems and synchronous communications. (English) Zbl 07649240

Di Giusto, Cinzia; Guizouarn, Loïc Germerie; Lozes, Etienne

J. Log. Algebr. Methods Program. 131, Article ID 100843, 17 p. (2023).

Summary: FIFO automata are finite state machines communicating through FIFO queues. They can be used, for instance, to model distributed protocols. Due to the unboundedness of the FIFO queues, several verification problems are undecidable for these systems. In order to model check such systems, one may look for decidable subclasses of FIFO systems. Binary half-duplex systems are systems of two FIFO automata exchanging over a half-duplex channel. They were studied by Cécé and Finkel who established the decidability in polynomial time of several properties. There is no obvious way to generalize the half-duplex property to multiparty systems. Cécé and Finkel proposed some generalizations but concluded that their notions of multiparty half-duplex systems were either too restrictive or too expressive.
We explore in this paper other ways of generalizing half-duplex systems to multiparty. First, we introduce systems realizable with synchronous communications (RSC) and we show that RSC systems generalize half-duplex systems and retain the same good properties as binary half-duplex systems. Second, we introduce a notion of multiparty half-duplex systems that differs from the ones explored by Cécé and Finkel, and we show two results about this notion: (1) for mailbox communications, half-duplex systems are essentially the same as RSC systems, and (2) for peer-to-peer communications, the two notions are distinct, and RSC systems appear to be “the good one”, since peer-to-peer half-duplex systems are Turing powerful.

MSC:

68-XX

Computer science

Keywords:

communicating finite state machines; FIFO systems; model-checking; message sequence charts; models of communications; synchronizability

Software:

McScM

References:

[1]	Cécé, G.; Finkel, A., Verification of programs with half-duplex communication, Inf. Comput., 202, 2, 166-190 (2005) · Zbl 1101.68676
[2]	Honda, K., Types for dyadic interaction, (Best, E., CONCUR’93, 4th International Conference on Concurrency Theory, Proceedings. CONCUR’93, 4th International Conference on Concurrency Theory, Proceedings, Hildesheim, Germany, August 23-26, 1993. CONCUR’93, 4th International Conference on Concurrency Theory, Proceedings. CONCUR’93, 4th International Conference on Concurrency Theory, Proceedings, Hildesheim, Germany, August 23-26, 1993, Lecture Notes in Computer Science, vol. 715 (1993), Springer), 509-523
[3]	Honda, K.; Vasconcelos, V. T.; Kubo, M., Language primitives and type discipline for structured communication-based programming, (Hankin, C., Programming Languages and Systems - ESOP’98, 7th European Symposium on Programming, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS’98, Proceedings. Programming Languages and Systems - ESOP’98, 7th European Symposium on Programming, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS’98, Proceedings, Lisbon, Portugal, March 28 - April 4, 1998. Programming Languages and Systems - ESOP’98, 7th European Symposium on Programming, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS’98, Proceedings. Programming Languages and Systems - ESOP’98, 7th European Symposium on Programming, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS’98, Proceedings, Lisbon, Portugal, March 28 - April 4, 1998, Lecture Notes in Computer Science, vol. 1381 (1998), Springer), 122-138
[4]	Fähndrich, M.; Aiken, M.; Hawblitzel, C.; Hodson, O.; Hunt, G. C.; Larus, J. R.; Levi, S., Language support for fast and reliable message-based communication in singularity OS, (Berbers, Y.; Zwaenepoel, W., Proceedings of the 2006 EuroSys Conference. Proceedings of the 2006 EuroSys Conference, Leuven, Belgium, April 18-21, 2006 (2006), ACM), 177-190
[5]	Lozes, É.; Villard, J., Reliable contracts for unreliable half-duplex communications, (WS-FM 2011. WS-FM 2011, LNCS, vol. 7176 (2011)), 2-16
[6]	Charron-Bost, B.; Mattern, F.; Tel, G., Synchronous, asynchronous, and causally ordered communication, Distrib. Comput., 9, 4, 173-191 (1996)
[7]	Heußner, A.; Leroux, J.; Muscholl, A.; Sutre, G., Reachability analysis of communicating pushdown systems, Log. Methods Comput. Sci., 8, 3 (2012) · Zbl 1248.68330
[8]	Chevrou, F.; Hurault, A.; Quéinnec, P., On the diversity of asynchronous communication, Form. Asp. Comput., 28, 5, 847-879 (2016) · Zbl 1345.68022
[9]	Basu, S.; Bultan, T., On deciding synchronizability for asynchronously communicating systems, Theor. Comput. Sci., 656, 60-75 (2016) · Zbl 1353.68195
[10]	Bouajjani, A.; Enea, C.; Ji, K.; Qadeer, S., On the completeness of verifying message passing programs under bounded asynchrony, (Chockler, H.; Weissenbacher, G., Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings, Part II. Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings, Part II, Oxford, UK, July 14-17, 2018. Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings, Part II. Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings, Part II, Oxford, UK, July 14-17, 2018, Lecture Notes in Computer Science, vol. 10982 (2018), Springer), 372-391
[11]	Genest, B.; Kuske, D.; Muscholl, A., On communicating automata with bounded channels, Fundam. Inform., 80, 1-3, 147-167 (2007) · Zbl 1137.68447
[12]	Di Giusto, C.; Germerie Guizouarn, L.; Lozes, É., Towards generalised half-duplex systems, (Proceedings 14th Interaction and Concurrency Experience, ICE 2021. Proceedings 14th Interaction and Concurrency Experience, ICE 2021, 18th June 2021 (2021)), 22-37, Online
[13]	Akroun, L.; Salaün, G., Automated verification of automata communicating via FIFO and bag buffers, Form. Methods Syst. Des., 52, 3, 260-276 (2018)
[14]	Itu-ts: Itu-ts recommendation z. 120: Message sequence chart (msc). itu-ts, 1999.
[15]	Honda, K.; Yoshida, N.; Carbone, M., Multiparty asynchronous session types, J. ACM, 63, 1, 9:1-9:67 (2016) · Zbl 1426.68047
[16]	Deniélou, P.; Yoshida, N., Multiparty session types meet communicating automata, (Seidl, H., Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Proceedings. Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Proceedings, Tallinn, Estonia, March 24 - April 1, 2012. Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Proceedings. Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Proceedings, Tallinn, Estonia, March 24 - April 1, 2012, Lecture Notes in Computer Science, vol. 7211 (2012), Springer), 194-213 · Zbl 1352.68182
[17]	Scalas, A.; Yoshida, N., Less is more: multiparty session types revisited, Proc. ACM Program. Lang., 3, POPL, 30:1-30:29 (2019)
[18]	Boigelot, B.; Godefroid, P., Symbolic verification of communication protocols with infinite state spaces using QDDs (extended abstract), (Alur, R.; Henzinger, T. A., Computer Aided Verification, 8th International Conference, CAV ’96, Proceedings. Computer Aided Verification, 8th International Conference, CAV ’96, Proceedings, New Brunswick, NJ, USA, July 31 - August 3, 1996. Computer Aided Verification, 8th International Conference, CAV ’96, Proceedings. Computer Aided Verification, 8th International Conference, CAV ’96, Proceedings, New Brunswick, NJ, USA, July 31 - August 3, 1996, Lecture Notes in Computer Science, vol. 1102 (1996), Springer), 1-12
[19]	Boigelot, B.; Godefroid, P.; Willems, B.; Wolper, P., The power of QDDs (extended abstract), (Hentenryck, P. V., Static Analysis, 4th International Symposium, SAS ’97, Proceedings. Static Analysis, 4th International Symposium, SAS ’97, Proceedings, Paris, France, September 8-10, 1997. Static Analysis, 4th International Symposium, SAS ’97, Proceedings. Static Analysis, 4th International Symposium, SAS ’97, Proceedings, Paris, France, September 8-10, 1997, Lecture Notes in Computer Science, vol. 1302 (1997), Springer), 172-186
[20]	Genest, B.; Muscholl, A.; Peled, D. A., Message sequence charts, (ACPN 2003. ACPN 2003, LNCS, vol. 3098 (2003)), 537-558 · Zbl 1088.68124
[21]	Post, Emil L., A variant of a recursively unsolvable problem, Bull. Am. Math. Soc., 52, 264-268 (1946) · Zbl 0063.06329
[22]	Bollig, B.; Di Giusto, C.; Finkel, A.; Laversa, L.; Lozes, É.; Suresh, A., A unifying framework for deciding synchronizability, (32nd International Conference on Concurrency Theory, CONCUR 2021, Virtual Conference. 32nd International Conference on Concurrency Theory, CONCUR 2021, Virtual Conference, August 24-27, 2021 (2021)), 14:1-14:18
[23]	J.K. Pachl, Reachability problems for communicating finite state machines, CoRR cs.LO/0306121, 2003. http://arxiv.org/abs/cs/0306121.
[24]	Heußner, A.; Gall, T. L.; Sutre, G., Mcscm: a general framework for the verification of communicating machines, (Flanagan, C.; König, B., Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Proceedings. Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Proceedings, Tallinn, Estonia, March 24 - April 1, 2012. Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Proceedings. Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Proceedings, Tallinn, Estonia, March 24 - April 1, 2012, Lecture Notes in Computer Science, vol. 7214 (2012), Springer), 478-484
[25]	Torre, S. L.; Madhusudan, P.; Parlato, G., Context-bounded analysis of concurrent queue systems, (Ramakrishnan, C. R.; Rehof, J., Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Proceedings. Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Proceedings, Budapest, Hungary, March 29-April 6, 2008. Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Proceedings. Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Proceedings, Budapest, Hungary, March 29-April 6, 2008, Lecture Notes in Computer Science, vol. 4963 (2008), Springer), 299-314 · Zbl 1134.68446
[26]	Cécé, G.; Finkel, A.; Iyer, S. P., Unreliable channels are easier to verify than perfect channels, Inf. Comput., 124, 1, 20-31 (1996) · Zbl 0844.68035
[27]	Abdulla, P. A.; Jonsson, B., Verifying programs with unreliable channels, Inf. Comput., 127, 2, 91-101 (1996) · Zbl 0856.68096
[28]	Chambart, P.; Schnoebelen, P., Mixing lossy and perfect FIFO channels, (van Breugel, F.; Chechik, M., CONCUR 2008 - Concurrency Theory, 19th International Conference, CONCUR 2008, Proceedings. CONCUR 2008 - Concurrency Theory, 19th International Conference, CONCUR 2008, Proceedings, Toronto, Canada, August 19-22, 2008. CONCUR 2008 - Concurrency Theory, 19th International Conference, CONCUR 2008, Proceedings. CONCUR 2008 - Concurrency Theory, 19th International Conference, CONCUR 2008, Proceedings, Toronto, Canada, August 19-22, 2008, Lecture Notes in Computer Science, vol. 5201 (2008), Springer), 340-355 · Zbl 1160.68460
[29]	Sen, K.; Viswanathan, M., Model checking multithreaded programs with asynchronous atomic methods, (Ball, T.; Jones, R. B., Computer Aided Verification (2006), Springer: Springer Berlin, Heidelberg), 300-314 · Zbl 1188.68198
[30]	Schnoebelen, P., Verifying lossy channel systems has nonprimitive recursive complexity, Inf. Process. Lett., 83, 5, 251-261 (2002) · Zbl 1043.68016
[31]	Schnoebelen, P., On flat lossy channel machines, (Baier, C.; Goubault-Larrecq, J., 29th EACSL Annual Conference on Computer Science Logic, CSL 2021, Virtual Conference. 29th EACSL Annual Conference on Computer Science Logic, CSL 2021, Virtual Conference, January 25-28, 2021, Ljubljana, Slovenia. 29th EACSL Annual Conference on Computer Science Logic, CSL 2021, Virtual Conference. 29th EACSL Annual Conference on Computer Science Logic, CSL 2021, Virtual Conference, January 25-28, 2021, Ljubljana, Slovenia, LIPIcs, vol. 183 (2021), Schloss Dagstuhl - Leibniz-Zentrum für Informatik), 37:1-37:22
[32]	Czerwinski, W.; Lasota, S.; Lazic, R.; Leroux, J.; Mazowiecki, F., The reachability problem for Petri nets is not elementary, J. ACM, 68, 1, 7:1-7:28 (2021)
[33]	Lohrey, M.; Muscholl, A., Bounded MSC communication, Inf. Comput., 189, 2, 160-181 (2004) · Zbl 1091.68006
[34]	Kuske, D.; Muscholl, A., Communicating automata, (Pin, J.-E., Handbook of Automata: from Mathematics to Applications (AutoMathA) (2019), European Science Foundation)
[35]	Lange, J.; Yoshida, N., Verifying asynchronous interactions via communicating session automata, (CAV 2019. CAV 2019, LNCS, vol. 11561 (2019)), 97-117
[36]	Di Giusto, C.; Laversa, L.; Lozes, É., On the k-synchronizability of systems, (FOSSACS 2020. FOSSACS 2020, LNCS, vol. 12077 (2020)), 157-176 · Zbl 07250937
[37]	Finkel, A.; Lozes, É., Synchronizability of communicating finite state machines is not decidable, (Chatzigiannakis, I.; Indyk, P.; Muscholl, A.; Kuhn, F., Proceedings of the 44th International Colloquium on Automata, Languages and Programming (ICALP’17). Proceedings of the 44th International Colloquium on Automata, Languages and Programming (ICALP’17), Leibniz International Proceedings in Informatics, vol. 80 (2017), Leibniz-Zentrum für Informatik: Leibniz-Zentrum für Informatik Warsaw, Poland), 122:1-122:14 · Zbl 1442.68138
[38]	Barbanera, F.; Lanese, I.; Tuosto, E., Choreography automata, (Bliudze, S.; Bocchi, L., Coordination Models and Languages - 22nd IFIP WG 6.1 International Conference, COORDINATION 2020, Held as Part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Proceedings. Coordination Models and Languages - 22nd IFIP WG 6.1 International Conference, COORDINATION 2020, Held as Part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Proceedings, Valletta, Malta, June 15-19, 2020. Coordination Models and Languages - 22nd IFIP WG 6.1 International Conference, COORDINATION 2020, Held as Part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Proceedings. Coordination Models and Languages - 22nd IFIP WG 6.1 International Conference, COORDINATION 2020, Held as Part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Proceedings, Valletta, Malta, June 15-19, 2020, Lecture Notes in Computer Science, vol. 12134 (2020), Springer), 86-106