Document Open Access Logo

A Unifying Framework for Deciding Synchronizability

Authors Benedikt Bollig , Cinzia Di Giusto , Alain Finkel , Laetitia Laversa , Etienne Lozes , Amrita Suresh

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2021.14.pdf
  • Filesize: 0.87 MB
  • 18 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
Keywords
  • communicating finite-state machines
  • message sequence charts
  • synchronizability
  • MSO logic
  • special tree-width

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Several notions of synchronizability of a message-passing system have been introduced in the literature. Roughly, a system is called synchronizable if every execution can be rescheduled so that it meets certain criteria, e.g., a channel bound. We provide a framework, based on MSO logic and (special) tree-width, that unifies existing definitions, explains their good properties, and allows one to easily derive other, more general definitions and decidability results for synchronizability.

Cite As Get BibTex

Benedikt Bollig, Cinzia Di Giusto, Alain Finkel, Laetitia Laversa, Etienne Lozes, and Amrita Suresh. A Unifying Framework for Deciding Synchronizability. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.CONCUR.2021.14

Author Details

Benedikt Bollig
  • Université Paris-Saclay, ENS Paris-Saclay, CNRS, LMF, France
Cinzia Di Giusto
  • Université Côte d’Azur, CNRS, I3S, France
Alain Finkel
  • Université Paris-Saclay, ENS Paris-Saclay, CNRS, LMF, France
  • Institut Universitaire de France, Paris, France
Laetitia Laversa
  • Université Côte d’Azur, CNRS, I3S, France
Etienne Lozes
  • Université Côte d’Azur, CNRS, I3S, France
Amrita Suresh
  • Université Paris-Saclay, ENS Paris-Saclay, CNRS, LMF, France

References

  1. C. Aiswarya and Paul Gastin. Reasoning about distributed systems: WYSIWYG (invited talk). In Venkatesh Raman and S. P. Suresh, editors, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2014, December 15-17, 2014, New Delhi, India, volume 29 of LIPIcs, pages 11-30. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2014.11.
  2. C. Aiswarya, Paul Gastin, and K. Narayan Kumar. Verifying communicating multi-pushdown systems via split-width. In Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, volume 8837 of Lecture Notes in Computer Science, pages 1-17. Springer, 2014. Google Scholar
  3. Samik Basu and Tevfik Bultan. Choreography conformance via synchronizability. In Sadagopan Srinivasan, Krithi Ramamritham, Arun Kumar, M. P. Ravindra, Elisa Bertino, and Ravi Kumar, editors, Proceedings of the 20th International Conference on World Wide Web, WWW 2011, Hyderabad, India, March 28 - April 1, 2011, pages 795-804. ACM, 2011. URL: https://doi.org/10.1145/1963405.1963516.
  4. Bernard Boigelot and Patrice Godefroid. Symbolic verification of communication protocols with infinite state spaces using qdds (extended abstract). In Rajeev Alur and Thomas A. Henzinger, editors, Computer Aided Verification, 8th International Conference, CAV '96, New Brunswick, NJ, USA, July 31 - August 3, 1996, Proceedings, volume 1102 of Lecture Notes in Computer Science, pages 1-12. Springer, 1996. URL: https://doi.org/10.1007/3-540-61474-5_53.
  5. Benedikt Bollig, Alain Finkel, and Amrita Suresh. Bounded reachability problems are decidable in FIFO machines. In Igor Konnov and Laura Kovacs, editors, Proceedings of the 31st International Conference on Concurrency Theory (CONCUR'20), volume 171 of Leibniz International Proceedings in Informatics, pages 49:1-49:17, Vienna, Austria, 2020. Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2020.49.
  6. Benedikt Bollig, Marie Fortin, and Paul Gastin. Communicating finite-state machines, first-order logic, and star-free propositional dynamic logic. J. Comput. Syst. Sci., 115:22-53, 2021. Google Scholar
  7. Benedikt Bollig and Paul Gastin. Non-sequential theory of distributed systems. CoRR, abs/1904.06942, 2019. URL: http://arxiv.org/abs/1904.06942.
  8. Ahmed Bouajjani, Constantin Enea, Kailiang Ji, and Shaz Qadeer. On the completeness of verifying message passing programs under bounded asynchrony. In Hana Chockler and Georg Weissenbacher, editors, 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, volume 10982 of Lecture Notes in Computer Science, pages 372-391. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-96142-2_23.
  9. Daniel Brand and Pitro Zafiropulo. On communicating finite-state machines. J. ACM, 30(2):323-342, 1983. URL: https://doi.org/10.1145/322374.322380.
  10. Gérard Cécé and Alain Finkel. Verification of programs with half-duplex communication. Information and Computation, 202(2):166-190, 2005. URL: https://doi.org/10.1016/j.ic.2005.05.006.
  11. Gérard Cécé, Alain Finkel, and S. Purushothaman Iyer. Unreliable channels are easier to verify than perfect channels. Information and Computation, 124(1):20-31, 1996. URL: http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CFP-IC96.ps.
  12. Bruno Courcelle. Special tree-width and the verification of monadic second-order graph properties. In FSTTCS, volume 8 of LIPIcs, pages 13-29, 2010. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2010.13.
  13. Aiswarya Cyriac, Paul Gastin, and K. Narayan Kumar. MSO decidability of multi-pushdown systems via split-width. In Maciej Koutny and Irek Ulidowski, editors, CONCUR 2012 - Concurrency Theory - 23rd International Conference, CONCUR 2012, Newcastle upon Tyne, UK, September 4-7, 2012. Proceedings, volume 7454 of Lecture Notes in Computer Science, pages 547-561. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-32940-1_38.
  14. Cinzia Di Giusto, Laetitia Laversa, and Étienne Lozes. On the k-synchronizability of systems. In Jean Goubault-Larrecq and Barbara König, editors, Foundations of Software Science and Computation Structures - 23rd International Conference, FOSSACS 2020, Proceedings, volume 12077 of Lecture Notes in Computer Science, pages 157-176. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-45231-5_9.
  15. Javier Esparza, Pierre Ganty, and Rupak Majumdar. A perfect model for bounded verification. In Proceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer Science, LICS '12, pages 285-294, Washington, DC, USA, 2012. IEEE Computer Society. URL: https://doi.org/10.1109/LICS.2012.39.
  16. Alain Finkel and Étienne Lozes. Synchronizability of communicating finite state machines is not decidable. In Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn, and Anca Muscholl, editors, 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland, volume 80 of LIPIcs, pages 122:1-122:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. Google Scholar
  17. Alain Finkel and M. Praveen. Verification of Flat FIFO Systems. Logical Methods in Computer Science, 20(4), 2020. URL: https://doi.org/10.23638/LMCS-16(4:4)2020.
  18. Blaise Genest, Dietrich Kuske, and Anca Muscholl. On communicating automata with bounded channels. Fundamenta Informaticae, 80(1-3):147-167, 2007. Google Scholar
  19. Blaise Genest, Anca Muscholl, and Dietrich Kuske. A kleene theorem for a class of communicating automata with effective algorithms. In Cristian Calude, Elena Calude, and Michael J. Dinneen, editors, Developments in Language Theory, 8th International Conference, DLT 2004, Auckland, New Zealand, December 13-17, 2004, Proceedings, volume 3340 of Lecture Notes in Computer Science, pages 30-48. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-30550-7_4.
  20. Cinzia Di Giusto, Laetitia Laversa, and Étienne Lozes. Guessing the buffer bound for k-synchronizability. In Implementation and Application of Automata - 25th International Conference, CIAA 2021, Proceedings, Lecture Notes in Computer Science. Springer, 2021. To appear. Google Scholar
  21. Jesper G. Henriksen, Madhavan Mukund, K. Narayan Kumar, Milind Sohoni, and P.S. Thiagarajan. A theory of regular msc languages. Information and Computation, 202(1):1-38, 2005. Google Scholar
  22. Dietrich Kuske and Anca Muscholl. Communicating automata, 2014. Google Scholar
  23. Julien Lange and Nobuko Yoshida. Verifying asynchronous interactions via communicating session automata. CoRR, abs/1901.09606, 2019. URL: http://arxiv.org/abs/1901.09606.
  24. Markus Lohrey and Anca Muscholl. Bounded MSC communication. In Mogens Nielsen and Uffe Engberg, editors, Foundations of Software Science and Computation Structures, 5th International Conference, FOSSACS 2002. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8-12, 2002, Proceedings, volume 2303 of Lecture Notes in Computer Science, pages 295-309. Springer, 2002. URL: https://doi.org/10.1007/3-540-45931-6_21.
  25. Markus Lohrey and Anca Muscholl. Bounded MSC communication. Inf. Comput., 189(2):160-181, 2004. URL: https://doi.org/10.1016/j.ic.2003.10.002.
  26. P. Madhusudan and Gennaro Parlato. The tree width of auxiliary storage. In Thomas Ball and Mooly Sagiv, editors, Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, pages 283-294. ACM, 2011. Google Scholar
  27. Robert S. Streett. Propositional dynamic logic of looping and converse. In Proceedings of the 13th Annual ACM Symposium on Theory of Computing, May 11-13, 1981, Milwaukee, Wisconsin, USA, pages 375-383. ACM, 1981. Google Scholar
  28. Gregor von Bochmann. Communication protocols and error recovery procedures. Operating Systems Review, 9(3):45-50, 1975. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact