Abstract
Communicating finite state machines (CFSMs) represent processes which communicate by asynchronous exchanges of messages via FIFO channels. Their major impact has been in characterising essential properties of communications such as freedom from deadlock and communication error, and buffer boundedness. CFSMs are known to be computationally hard: most of these properties are undecidable even in restricted cases. At the same time, multiparty session types are a recent typed framework whose main feature is its ability to efficiently enforce these properties for mobile processes and programming languages. This paper ties the links between the two frameworks to achieve a two-fold goal. On one hand, we present a generalised variant of multiparty session types that have a direct semantical correspondence to CFSMs. Our calculus can treat expressive forking, merging and joining protocols that are absent from existing session frameworks, and our typing system can ensure properties such as safety, boundedness and liveness on distributed processes by a polynomial time type checking. On the other hand, multiparty session types allow us to identify a new class of CFSMs that automatically enjoy the aforementioned properties , generalising Gouda et al’s work [12] (for two machines) to an arbitrary number of machines.
Keywords
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.
References
Basu, S., Bultan, T., Ouederni, M.: Deciding choreography realizability. In: POPL 2012. ACM (to appear, 2012)
Basu, S., Bultan, T., Ouederni, M.: Synchronizability for Verification of Asynchronously Communicating Systems. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 56–71. Springer, Heidelberg (2012)
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)
Business Process Model and Notation, http://www.bpmn.org
Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30, 323–342 (1983)
Castagna, G., Dezani-Ciancaglini, M., Padovani, L.: On Global Types and Multi-party Sessions. In: Bruni, R., Dingel, J. (eds.) FORTE 2011 and FMOODS 2011. LNCS, vol. 6722, pp. 1–28. Springer, Heidelberg (2011)
Cécé, G., Finkel, A.: Verification of programs with half-duplex communication. Inf. Comput. 202(2), 166–190 (2005)
Corin, R., Deniélou, P.M., Fournet, C., Bhargavan, K., Leifer, J.: Secure implementations for typed session abstractions. In: CSF, pp. 170–186 (2007)
Deniélou, P.M., Yoshida, N.: Buffered Communication Analysis in Distributed Multiparty Sessions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 343–357. Springer, Heidelberg (2010)
Deniélou, P.M., Yoshida, N.: Dynamic multirole session types. In: POPL, pp. 435–446. ACM (2011), full version, Prototype at, http://www.doc.ic.ac.uk/~pmalo/dynamic
Genest, B., Muscholl, A., Peled, D.: Message Sequence Charts. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 537–558. Springer, Heidelberg (2004)
Gouda, M., Manning, E., Yu, Y.: On the progress of communication between two finite state machines. Information and Control 63, 200–216 (1984)
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)
Honda, K., Yoshida, N., Carbone, M.: Multiparty Asynchronous Session Types. In: POPL 2008, pp. 273–284. ACM (2008)
Kouzapas, D., Yoshida, N., Honda, K.: On Asynchronous Session Semantics. In: Bruni, R., Dingel, J. (eds.) FORTE 2011 and FMOODS 2011. LNCS, vol. 6722, pp. 228–243. Springer, Heidelberg (2011)
Lozes, E., Villard, J.: Reliable contracts for unreliable half-duplex communications. In: WS-FM. Springer, Heidelberg (2011) (to appear)
Ng, N., Yoshida, N., Pernet, O., Hu, R., Kryftis, Y.: Safe Parallel Programming with Session Java. In: De Meuter, W., Roman, G.-C. (eds.) COORDINATION 2011. LNCS, vol. 6721, pp. 110–126. Springer, Heidelberg (2011)
Online Appendix, http://www.doc.ic.ac.uk/~malo/msa/
Savara JBoss Project, http://www.jboss.org/savara
Scribble JBoss Project, http://www.jboss.org/scribble
Sivaramakrishnan, K.C., Nagaraj, K., Ziarek, L., Eugster, P.: Efficient Session Type Guided Distributed Interaction. In: Clarke, D., Agha, G. (eds.) COORDINATION 2010. LNCS, vol. 6116, pp. 152–167. Springer, Heidelberg (2010)
Swamy, N., Chen, J., Fournet, C., Strub, P.Y., Bharagavan, K., Yang, J.: Secure distributed programming with value-dependent types. In: ICFP, pp. 266–278. ACM (2011)
Villard, J.: Heaps and Hops. Ph.D. thesis, ENS Cachan (2011)
Yoshida, N., Deniélou, P.M., Bejleri, A., Hu, R.: Parameterised Multiparty Session Types. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol. 6014, pp. 128–145. Springer, Heidelberg (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Deniélou, PM., Yoshida, N. (2012). Multiparty Session Types Meet Communicating Automata. In: Seidl, H. (eds) Programming Languages and Systems. ESOP 2012. Lecture Notes in Computer Science, vol 7211. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28869-2_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-28869-2_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28868-5
Online ISBN: 978-3-642-28869-2
eBook Packages: Computer ScienceComputer Science (R0)