Multiparty compatibility in communicating automata: characterisation and synthesis of global session types

DOI10.1007/978-3-642-39212-2_18MaRDI QIDQ5327432zbMATH OpenOpenAlexFDO

Authors Pierre-Malo Deniélou, Nobuko Yoshida

Publication date 7 August 2013

Published in Automata, Languages, and Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1304.1902

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: 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.

Recommendations

• On global types and multi-party sessions
• Multiparty Asynchronous Session Types
• Multiparty session types meet communicating automata
• Multiparty session types, beyond duality
• Multiparty asynchronous session types

Cited in

(43)

• Multiparty session types, beyond duality
• Timed runtime monitoring for multiparty conversations
• A core model for choreographic programming
• Communicating finite state machines and an extensible toolchain for multiparty session types
• Fair refinement for asynchronous session types
• Session coalgebras: a coalgebraic view on session types and communication protocols
• An abstract framework for choreographic testing
• Global types with internal delegation
• Session typing and asynchronous subtyping for the higher-order \(\pi\)-calculus
• Multiparty session types as coherence proofs
• Contracts as games on event structures
• Automata for analysing service contracts
• Multiparty session nets
• A gentle introduction to multiparty asynchronous session types
• Multiparty Session Types Within a Canonical Binary Theory, and Beyond
• Typechecking safe process synchronization
• On global types and multi-party sessions
• Multiparty session types meet communicating automata
• Symbolic Semantics for Multiparty Interactions in the Link-Calculus
• Honesty by typing
• On the undecidability of asynchronous session subtyping
• Behavioural analysis of sessions using the calculus of structures
• Compliance in behavioural contracts: a brief survey
• Verifiable abstractions for contract-oriented systems
• Typestates to automata and back: a tool
• Exploring type-level bisimilarity towards more expressive multiparty session types
• scientific article; zbMATH DE number 7559468 (Why is no real title available?)
• Constructing weak simulations from linear implications for processes with private names
• Global escape in multiparty sessions
• Global progress for dynamically interleaved multiparty sessions
• scientific article; zbMATH DE number 7327953 (Why is no real title available?)
• A Sound Algorithm for Asynchronous Session Subtyping
• Domain-aware session types
• Precise Subtyping for Asynchronous Multiparty Sessions
• Verifying asynchronous interactions via communicating session automata
• A predicate transformer for choreographies. Computing preconditions in choreographic programming
• Comparing channel restrictions of communicating state machines, high-level message sequence charts, and multiparty session types
• Complete multiparty session type projection with automata
• Fair asynchronous session subtyping
• Timeout asynchronous session types: safe asynchronous mixed-choice for timed interactions
• Crash-stop failures in asynchronous multiparty session types
• Less is more revisited: association with global protocols and multiparty sessions
• Asynchronous global protocols, precisely

This page was built for publication: Multiparty compatibility in communicating automata: characterisation and synthesis of global session types

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5327432)