References

  1. Parosh Aziz Abdulla, C. Aiswarya & Mohamed Faouzi Atig (2016): Data Communicating Processes with Unreliable Channels. In: Martin Grohe, Eric Koskinen & Natarajan Shankar: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016. ACM, pp. 166–175, doi:10.1145/2933575.2934535.
  2. Parosh Aziz Abdulla, Ahmed Bouajjani & Bengt Jonsson (1998): On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channels. In: Alan J. Hu & Moshe Y. Vardi: Computer Aided Verification, 10th International Conference, CAV'98, Vancouver, BC, Canada, June 28 - July 2, 1998, Proceedings, Lecture Notes in Computer Science 1427. Springer, pp. 305–318, doi:10.1007/BFb0028754.
  3. C. Aiswarya, Paul Gastin & K. Narayan Kumar (2014): Verifying Communicating Multi-pushdown Systems via Split-Width. In: Franck Cassez & Jean-François Raskin: Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3-7, 2014, Proceedings, Lecture Notes in Computer Science 8837. Springer, pp. 1–17, doi:10.1007/978-3-319-11936-6_1.
  4. Rajeev Alur, Kousha Etessami & Mihalis Yannakakis (2003): Inference of Message Sequence Charts. IEEE Trans. Software Eng. 29(7), pp. 623–633, doi:10.1109/TSE.2003.1214326.
  5. Rajeev Alur, Kousha Etessami & Mihalis Yannakakis (2005): Realizability and verification of MSC graphs. Theor. Comput. Sci. 331(1), pp. 97–114, doi:10.1016/j.tcs.2004.09.034.
  6. Rajeev Alur & Mihalis Yannakakis (1999): Model Checking of Message Sequence Charts. In: Jos C. M. Baeten & Sjouke Mauw: CONCUR '99: Concurrency Theory, 10th International Conference, Eindhoven, The Netherlands, August 24-27, 1999, Proceedings, Lecture Notes in Computer Science 1664. Springer, pp. 114–129, doi:10.1007/3-540-48320-9_10.
  7. Franco Barbanera, Ivan Lanese & Emilio Tuosto (2020): Choreography Automata. In: Simon Bliudze & Laura Bocchi: 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, Valletta, Malta, June 15-19, 2020, Proceedings, Lecture Notes in Computer Science 12134. Springer, pp. 86–106, doi:10.1007/978-3-030-50029-0_6.
  8. Hanêne Ben-Abdallah & Stefan Leue (1997): Syntactic Detection of Process Divergence and Non-local Choice inMessage Sequence Charts. In: Ed Brinksma: Tools and Algorithms for Construction and Analysis of Systems, Third International Workshop, TACAS '97, Enschede, The Netherlands, April 2-4, 1997, Proceedings, Lecture Notes in Computer Science 1217. Springer, pp. 259–274, doi:10.1007/BFb0035393.
  9. Bernard Boigelot, Patrice Godefroid, Bernard Willems & Pierre Wolper (1997): The Power of QDDs (Extended Abstract). In: Pascal Van Hentenryck: Static Analysis, 4th International Symposium, SAS '97, Paris, France, September 8-10, 1997, Proceedings, Lecture Notes in Computer Science 1302. Springer, pp. 172–186, doi:10.1007/BFb0032741.
  10. Benedikt Bollig, Alain Finkel & Amrita Suresh (2020): Bounded Reachability Problems Are Decidable in FIFO Machines. In: Igor Konnov & Laura Kovács: 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference), LIPIcs 171. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 49:1–49:17, doi:10.4230/LIPIcs.CONCUR.2020.49.
  11. Benedikt Bollig & Paul Gastin (2019): Non-Sequential Theory of Distributed Systems. CoRR abs/1904.06942, doi:10.48550/arXiv.1904.06942. ArXiv:1904.06942.
  12. Benedikt Bollig, Cinzia Di Giusto, Alain Finkel, Laetitia Laversa, Étienne Lozes & Amrita Suresh (2021): A Unifying Framework for Deciding Synchronizability. In: Serge Haddad & Daniele Varacca: 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference, LIPIcs 203. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 14:1–14:18, doi:10.4230/LIPIcs.CONCUR.2021.14.
  13. Ahmed Bouajjani, Constantin Enea, Kailiang Ji & Shaz Qadeer (2018): On the Completeness of Verifying Message Passing Programs Under Bounded Asynchrony. In: Hana Chockler & Georg Weissenbacher: Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II, Lecture Notes in Computer Science 10982. Springer, pp. 372–391, doi:10.1007/978-3-319-96142-2_23.
  14. Daniel Brand & Pitro Zafiropulo (1983): On Communicating Finite-State Machines. J. ACM 30(2), pp. 323–342, doi:10.1145/322374.322380.
  15. Marco Carbone, Kohei Honda, N. Yoshida, R. Milner, G. Brown & Steve Ross-Talbot (2005): A Theoretical Basis of Communication-Centred Concurrent Programming.
  16. Giuseppe Castagna, Mariangiola Dezani-Ciancaglini & Luca Padovani (2012): On Global Types and Multi-Party Session. Log. Methods Comput. Sci. 8(1), doi:10.2168/LMCS-8(1:24)2012.
  17. Gérard Cécé & Alain Finkel (2005): Verification of programs with half-duplex communication. Inf. Comput. 202(2), pp. 166–190, doi:10.1016/j.ic.2005.05.006.
  18. Haitao Dan, Robert M. Hierons & Steve Counsell (2010): Non-local Choice and Implied Scenarios. In: José Luiz Fiadeiro, Stefania Gnesi & Andrea Maggiolo-Schettini: 8th IEEE International Conference on Software Engineering and Formal Methods, SEFM 2010, Pisa, Italy, 13-18 September 2010. IEEE Computer Society, pp. 53–62, doi:10.1109/SEFM.2010.14.
  19. Pierre-Malo Deniélou & Nobuko Yoshida (2012): Multiparty Session Types Meet Communicating Automata. In: Helmut Seidl: 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, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings, Lecture Notes in Computer Science 7211. Springer, pp. 194–213, doi:10.1007/978-3-642-28869-2_10.
  20. Manuel Fähndrich, Mark Aiken, Chris Hawblitzel, Orion Hodson, Galen C. Hunt, James R. Larus & Steven Levi (2006): Language support for fast and reliable message-based communication in singularity OS. In: Yolande Berbers & Willy Zwaenepoel: Proceedings of the 2006 EuroSys Conference, Leuven, Belgium, April 18-21, 2006. ACM, pp. 177–190, doi:10.1145/1217935.1217953.
  21. Alain Finkel & Étienne Lozes (2017): Synchronizability of Communicating Finite State Machines is not Decidable. In: Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn & Anca Muscholl: 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland, LIPIcs 80. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 122:1–122:14, doi:10.4230/LIPIcs.ICALP.2017.122.
  22. Simon J. Gay & Vasco Thudichum Vasconcelos (2010): Linear type theory for asynchronous session types. J. Funct. Program. 20(1), pp. 19–50, doi:10.1017/S0956796809990268.
  23. Thomas Gazagnaire, Blaise Genest, Loïc Hélouët, P. S. Thiagarajan & Shaofa Yang (2007): Causal Message Sequence Charts. In: Luís Caires & Vasco Thudichum Vasconcelos: CONCUR 2007 - Concurrency Theory, 18th International Conference, CONCUR 2007, Lisbon, Portugal, September 3-8, 2007, Proceedings, Lecture Notes in Computer Science 4703. Springer, pp. 166–180, doi:10.1007/978-3-540-74407-8_12.
  24. Blaise Genest, Dietrich Kuske & Anca Muscholl (2007): On Communicating Automata with Bounded Channels. Fundam. Inform. 80(1-3), pp. 147–167. Available at http://content.iospress.com/articles/fundamenta-informaticae/fi80-1-3-09.
  25. Blaise Genest & Anca Muscholl (2005): Message Sequence Charts: A Survey. In: Fifth International Conference on Application of Concurrency to System Design (ACSD 2005), 6-9 June 2005, St. Malo, France. IEEE Computer Society, pp. 2–4, doi:10.1109/ACSD.2005.25.
  26. Blaise Genest, Anca Muscholl & Doron A. Peled (2003): Message Sequence Charts. In: Jörg Desel, Wolfgang Reisig & Grzegorz Rozenberg: Lectures on Concurrency and Petri Nets, Advances in Petri Nets [This tutorial volume originates from the 4th Advanced Course on Petri Nets, ACPN 2003, held in Eichstätt, Germany in September 2003. In addition to lectures given at ACPN 2003, additional chapters have been commissioned], Lecture Notes in Computer Science 3098. Springer, pp. 537–558, doi:10.1007/978-3-540-27755-2_15.
  27. Blaise Genest, Anca Muscholl, Helmut Seidl & Marc Zeitoun (2006): Infinite-state high-level MSCs: Model-checking and realizability. J. Comput. Syst. Sci. 72(4), pp. 617–647, doi:10.1016/j.jcss.2005.09.007.
  28. Cinzia Di Giusto, Laetitia Laversa & Étienne Lozes (2020): On the k-synchronizability of Systems. In: Jean Goubault-Larrecq & Barbara König: Foundations of Software Science and Computation Structures - 23rd International Conference, FOSSACS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Lecture Notes in Computer Science 12077. Springer, pp. 157–176, doi:10.1007/978-3-030-45231-5_9.
  29. Loïc Hélouët & Claude Jard (2000): Conditions for synthesis of communicating automata from HMSCs. In: In 5th International Workshop on Formal Methods for Industrial Critical Systems (FMICS).
  30. Alexander Heußner, Jérôme Leroux, Anca Muscholl & Grégoire Sutre (2012): Reachability Analysis of Communicating Pushdown Systems. Log. Methods Comput. Sci. 8(3), doi:10.2168/LMCS-8(3:23)2012.
  31. Kohei Honda (1993): Types for Dyadic Interaction. In: Eike Best: CONCUR '93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, August 23-26, 1993, Proceedings, Lecture Notes in Computer Science 715. Springer, pp. 509–523, doi:10.1007/3-540-57208-2_35.
  32. Kohei Honda, Nobuko Yoshida & Marco Carbone (2008): Multiparty asynchronous session types. In: George C. Necula & Philip Wadler: Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008. ACM, pp. 273–284, doi:10.1145/1328438.1328472.
  33. Kohei Honda, Nobuko Yoshida & Marco Carbone (2016): Multiparty Asynchronous Session Types. J. ACM 63(1), pp. 9:1–9:67, doi:10.1145/2827695.
  34. Chris Köcher (2021): Reachability Problems on Reliable and Lossy Queue Automata. Theory Comput. Syst. 65(8), pp. 1211–1242, doi:10.1007/s00224-021-10031-2.
  35. Julien Lange & Nobuko Yoshida (2019): Verifying Asynchronous Interactions via Communicating Session Automata. In: Isil Dillig & Serdar Tasiran: Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I, Lecture Notes in Computer Science 11561. Springer, pp. 97–117, doi:10.1007/978-3-030-25540-4_6.
  36. Markus Lohrey (2003): Realizability of high-level message sequence charts: closing the gaps. Theor. Comput. Sci. 309(1-3), pp. 529–554, doi:10.1016/j.tcs.2003.08.002.
  37. P. Madhusudan (2001): Reasoning about Sequential and Branching Behaviours of Message Sequence Graphs. In: Fernando Orejas, Paul G. Spirakis & Jan van Leeuwen: Automata, Languages and Programming, 28th International Colloquium, ICALP 2001, Crete, Greece, July 8-12, 2001, Proceedings, Lecture Notes in Computer Science 2076. Springer, pp. 809–820, doi:10.1007/3-540-48224-5_66.
  38. Rupak Majumdar, Madhavan Mukund, Felix Stutz & Damien Zufferey (2021): Generalising Projection in Asynchronous Multiparty Session Types. In: Serge Haddad & Daniele Varacca: 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference, LIPIcs 203. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 35:1–35:24, doi:10.4230/LIPIcs.CONCUR.2021.35.
  39. Sjouke Mauw & Michel A. Reniers (1997): High-level message sequence charts. In: Ana R. Cavalli & Amardeo Sarma: SDL '97 Time for Testing, SDL, MSC and Trends - 8th International SDL Forum, Evry, France, 23-29 September 1997, Proceedings. Elsevier, pp. 291–306.
  40. Arjan J. Mooij, Nicolae Goga & Judi Romijn (2005): Non-local Choice and Beyond: Intricacies of MSC Choice Nodes. In: Maura Cerioli: Fundamental Approaches to Software Engineering, 8th International Conference, FASE 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings, Lecture Notes in Computer Science 3442. Springer, pp. 273–288, doi:10.1007/978-3-540-31984-9_21.
  41. Henry Muccini (2003): Detecting Implied Scenarios Analyzing Non-local Branching Choices. In: Mauro Pezzè: Fundamental Approaches to Software Engineering, 6th International Conference, FASE 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings, Lecture Notes in Computer Science 2621. Springer, pp. 372–386, doi:10.1007/3-540-36578-8_26.
  42. Wuxu Peng & S. Purushothaman (1992): Analysis of a Class of Communicating Finite State Machines. Acta Informatica 29(6/7), pp. 499–522, doi:10.1007/BF01185558.
  43. Abhik Roychoudhury, Ankit Goel & Bikram Sengupta (2012): Symbolic Message Sequence Charts. ACM Trans. Softw. Eng. Methodol. 21(2), pp. 12:1–12:44, doi:10.1145/2089116.2089122.
  44. Alceste Scalas & Nobuko Yoshida (2019): Less is more: multiparty session types revisited. Proc. ACM Program. Lang. 3(POPL), pp. 30:1–30:29, doi:10.1145/3290343.
  45. Felix Stutz & Damien Zufferey (2022): Comparing Channel Restrictions of Communicating State Machines, High-level Message Sequence Charts, and Multiparty Session Types. CoRR abs/2208.05559, doi:10.48550/arXiv.2208.05559. ArXiv:2208.05559.
  46. Salvatore La Torre, P. Madhusudan & Gennaro Parlato (2008): Context-Bounded Analysis of Concurrent Queue Systems. In: C. R. Ramakrishnan & Jakob Rehof: 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, Budapest, Hungary, March 29-April 6, 2008. Proceedings, Lecture Notes in Computer Science 4963. Springer, pp. 299–314, doi:10.1007/978-3-540-78800-3_21.
  47. Tayssir Touili & Mohamed Faouzi Atig (2010): Verifying parallel programs with dynamic communication structures. Theor. Comput. Sci. 411(38-39), pp. 3460–3468, doi:10.1016/j.tcs.2010.05.028.
  48. International Telecommunication Union (1996): Z.120: Message Sequence Chart. Technical Report. International Telecommunication Union. Available at https://www.itu.int/rec/T-REC-Z.120.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org