Multiparty Compatibility in Communicating Automata: Characterisation and Synthesis of Global Session Types

  • Pierre-Malo Deniélou
  • Nobuko Yoshida
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7966)


Multiparty session types are a type system that can ensure the safety and liveness of distributed peers via the global specification of their interactions. To construct a global specification from a set of distributed uncontrolled behaviours, this paper explores the problem of fully characterising multiparty session types in terms of communicating automata. We equip global and local session types with labelled transition systems (LTSs) that faithfully represent asynchronous communications through unbounded buffered channels. Using the equivalence between the two LTSs, we identify a class of communicating automata that exactly correspond to the projected local types. We exhibit an algorithm to synthesise a global type from a collection of communicating automata. The key property of our findings is the notion of multiparty compatibility which non-trivially extends the duality condition for binary session types.


Local Type Finite State Machine Safety Property Label Transition System Liveness Property 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Basu, S., Bultan, T., Ouederni, M.: Deciding choreography realizability. In: POPL 2012, pp. 191–202. ACM (2012)Google Scholar
  2. 2.
    Bettini, L., Coppo, M., D’Antoni, L., De Luca, M., Dezani-Ciancaglini, M., Yoshida, N.: Global progress in dynamically interleaved multiparty sessions. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 418–433. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  3. 3.
    Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30, 323–342 (1983)MathSciNetzbMATHCrossRefGoogle Scholar
  4. 4.
    Caires, L., Pfenning, F.: Session types as intuitionistic linear propositions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 222–236. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  5. 5.
    Castagna, G., Dezani-Ciancaglini, M., Padovani, L.: On global types and multi-party session. LMCS 8(1) (2012)Google Scholar
  6. 6.
    Cécé, G., Finkel, A.: Verification of programs with half-duplex communication. Inf. Comput. 202(2), 166–190 (2005)zbMATHCrossRefGoogle Scholar
  7. 7.
    Deniélou, P.-M., Yoshida, N.: Dynamic multirole session types. In: POPL, pp. 435–446. ACM, Full version, Prototype at
  8. 8.
    Deniélou, P.-M., Yoshida, N.: Multiparty session types meet communicating automata. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 194–213. Springer, Heidelberg (2012)Google Scholar
  9. 9.
  10. 10.
    Girard, J.-Y.: Linear logic. TCS 50 (1987)Google Scholar
  11. 11.
    Gouda, M., Manning, E., Yu, Y.: On the progress of communication between two finite state machines. Information and Control 63, 200–216 (1984)MathSciNetzbMATHCrossRefGoogle Scholar
  12. 12.
    Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 122–138. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  13. 13.
    Honda, K., Yoshida, N., Carbone, M.: Multiparty Asynchronous Session Types. In: POPL 2008, pp. 273–284. ACM (2008)Google Scholar
  14. 14.
    Lange, J., Tuosto, E.: Synthesising choreographies from local session types. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 225–239. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  15. 15.
    Mostrous, D., Yoshida, N., Honda, K.: Global principal typing in partially commutative asynchronous sessions. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 316–332. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  16. 16.
    Muscholl, A.: Analysis of communicating automata. In: Dediu, A.-H., Fernau, H., Martín-Vide, C. (eds.) LATA 2010. LNCS, vol. 6031, pp. 50–57. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  17. 17.
    DoC Technical Report, Imperial College London, Computing, DTR13-5 (2013)Google Scholar
  18. 18.
    Takeuchi, K., Honda, K., Kubo, M.: An interaction-based language and its typing system. In: Halatsis, C., Philokyprou, G., Maritsas, D., Theodoridis, S. (eds.) PARLE 1994. LNCS, vol. 817, pp. 398–413. Springer, Heidelberg (1994)CrossRefGoogle Scholar
  19. 19.
    Villard, J.: Heaps and Hops. PhD thesis, ENS Cachan (2011)Google Scholar
  20. 20.
    Wadler, P.: Proposition as Sessions. In: ICFP 2012, pp. 273–286 (2012)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Pierre-Malo Deniélou
    • 1
  • Nobuko Yoshida
    • 2
  1. 1.Royal HollowayUniversity of LondonUK
  2. 2.Imperial College LondonUK

Personalised recommendations