PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Pierre-Malo Deniélou, Nobuko Yoshida

arXiv:1304.1902v1cs.FLcs.DC

TL;DR

The paper asks when distributed communicating automata can be reconstructed as global multiparty session specifications while preserving communication safety and liveness. It equips global and local types with LTSs, uses multiparty compatibility to characterise suitable automata, and gives a synthesis procedure whose soundness and completeness are established for basic CFSM systems.

  • Problem

    The paper addresses the need for sound and complete conditions to reconstruct global session types from distributed CFSM specifications.

  • Method

    The paper defines LTSs for global and local types, relates projected local types to CFSMs, and uses decidable multiparty compatibility with 1-bounded executions for synthesis.

  • Results

    For basic multiparty-compatible CFSM systems, the paper proves existence of an equivalent global type; conversely, well-formed global types correspond to systems satisfying the three safety properties.

  • Takeaways & Limitations

    Multiparty compatibility provides a necessary and sufficient condition for obtaining safe global types from the considered basic CFSM systems.

  • Takeaways & Limitations

    The formal characterisation assumes basic CFSMs and relies on connected-machine assumptions; the relevant safety properties are otherwise undecidable for general CFSMs.

Abstract

from arXiv · show

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.

1 Introduction

The paper addresses reconstructing global session specifications from distributed CFSM behaviours. It generalises binary duality to multiparty compatibility, characterises when synthesis is possible, and presents extensions beyond classical multiparty session types.

  • Motivation: The paper seeks sound and complete conditions for reconstructing a global type from distributed CFSM specifications.Such specifications arise from endpoint projections, inferred control flow, or existing service interfaces.
  • Binary baseline: Binary session types rely on duality, deterministic communications, non-mixed states, and compatible traces to guarantee deadlock-free composition.Violating these conditions can permit deadlocks, while violating the first two makes compatibility checking undecidable.
  • Multiparty challenge: The commit protocol illustrates the multiparty challenge through coordinated choices among Alice, Bob, and Carol.Alice directs Bob to act or quit; subsequent messages determine whether the protocol commits or saves data before termination.
  • Main idea: Multiparty compatibility generalises duality by checking each automaton against the others after their internal communications, using 1-bounded executions.If extended duality holds from every 1-bounded reachable state, the machines can form a well-formed global choreography.
  • Extensions: The work extends its synthesis results to generalised multiparty session types with graph-like control flow and parallelism.The extension uses generalised well-formedness, Petri-net intermediate representations, and 1-bounded behavioural exploration, with applicability to Choreography BPMN 2.0.

2 Communicating Finite State Machines

This section defines communicating finite-state machines and their asynchronous communicating systems. It formalises configurations, executions, reachability, boundedness, traces, and the safety and liveness properties later used for characterisation.

  • CFSM model: A CFSM is a finite transition system whose states, channels, initial state, message alphabet, and labelled transitions define one participant’s behaviour.A communicating system is a tuple of such machines sharing directed channels between distinct participants.
  • Machine properties: CFSM states are classified as sending, receiving, final, mixed, or directed according to their outgoing actions and communication partners.The section also assumes each CFSM is connected and defines determinism by requiring identical actions from a state to have the same successor.
  • Configurations and transitions: System configurations combine each machine’s local control state with the contents of every channel buffer.Sending and receiving transitions update machine states and add or remove messages from the corresponding buffers.
  • Executions and traces: The framework defines initial, final, reachable, and traced behaviours, together with k-bounded executions whose reachable configuration sets are finite and computable.Trace equivalences compare all traces or only traces whose send-receive imbalance is bounded by n.
  • Safety and liveness: The later characterisation uses deadlock-freedom, orphan-message freedom, reception-error freedom, and liveness as the system properties session types should enforce.These properties are generally undecidable for CFSMs, motivating stronger decidable conditions in the synthesis results.

3 Global and local types: the LTSs and translations

The paper gives global and local multiparty session types asynchronous LTS semantics and establishes trace-preserving connections between local types and communicating finite-state machines.

  • Syntax and projection: Global types describe whole-session conversations, while local types abstract each participant’s endpoint view using branching, selection, recursion, and termination.Projection, extended with a merging operator, maps global types to local types when branches have compatible interaction patterns.
  • LTS over global types: The global-type LTS represents message emission and reception separately, allowing asynchronous reordering when consecutive communications involve disjoint participants.Intermediate states record messages that have been sent but not yet received; participant-subject conditions enforce the permitted ordering constraints.
  • LTS over local types: The local-type semantics follows CFSM configurations with FIFO channel queues, and visible traces are defined for global types, local types, and communicating systems.A configuration combines the local states of all participants with one FIFO queue for each directed channel.
  • Correspondence: Projection is sound and complete: a global type is trace-equivalent to the collection of its projected local types with empty buffers.The theorem connects the global LTS with the asynchronous configuration semantics of projected local types.
  • Translations: Local types translate to deterministic, directed CFSMs without mixed states, while basic CFSMs translate back to local types while preserving trace semantics.The two translations satisfy M ≈ T(M) for basic CFSMs and T ≈ A(T) for local types.

4 Completeness and synthesis

The paper defines multiparty compatibility as a decidable generalisation of binary duality, proves its safety and liveness consequences, and synthesises equivalent well-formed global types from compatible basic CFSM systems.

  • Multiparty compatibility: Multiparty compatibility requires each machine’s actions to be matched by dual actions from the remaining machines through internal 1-bounded alternations.The other machines may perform intermediate actions that are unobservable from the selected machine’s viewpoint.
  • Safety and liveness: A basic multiparty-compatible system satisfies the three safety properties, and it is live when at least one machine contains a final state.Safety follows from compatibility and stability; liveness additionally requires the stated final-state condition.
  • Compatibility checking: For basic systems, compatibility is decidable by exploring reachable states under 1-bounded executions and checking matching send and receive transitions.The procedure checks every machine and every stable state in the 1-bounded reachable-state set.
  • Synthesis: The one-buffer equivalence lemma lifts equivalence of basic multiparty-compatible systems from 1-bounded executions to unrestricted executions.This result is the bridge from the bounded exploration used by synthesis to full trace equivalence.
  • Characterisation: Theorem 4.3 establishes soundness and completeness: every basic multiparty-compatible system corresponds to a global type, and every well-formed global type has a corresponding safe system.The correspondence is trace equivalence between the communicating system and the global type.

5 Conclusion and related work

The paper closes the open problem of characterising multiparty session types with CFSMs and synthesising global types from basic CFSMs. It positions multiparty compatibility as a decidable foundation with applications beyond syntax-dependent local-type synthesis.

  • 5 Conclusion and related work: The paper establishes a sound and complete characterisation of multiparty session types in CFSMs and develops a decidable synthesis algorithm from basic CFSMs.
  • 5 Conclusion and related work: Multiparty compatibility extends binary duality and, together with basic conditions, is necessary and sufficient for obtaining safe global types.
  • 5 Conclusion and related work: The work targets applications including inferring and testing implementation communication structure against choreographies and monitoring distributed update paths.
  • 5 Conclusion and related work: The synthesis is more general than syntax-dependent approaches because it operates on CFSMs rather than projected local-type syntax.

A.1 Proof of Theorem 3.1

This appendix proves that global-type transitions correspond step by step to transitions of projected local configurations. The proof combines extended projection with local-type subtyping and establishes the required equivalence.

  • A.1 Proof of Theorem 3.1: Local-type subtyping orders a type below a supertype that offers more receive transitions and extends pointwise to configurations with identical buffers.
  • A.1 Proof of Theorem 3.1: Extended projection represents intermediate global states with projected participant types and buffers, allowing global and local transitions to be matched step by step.
  • A.1 Proof of Theorem 3.1: Step equivalence states that a global transition exists exactly when the corresponding projected local configuration transition exists, preserving the subtyping relation.
  • A.1 Proof of Theorem 3.1: The proof handles selections, branch receptions, recursion, and merged projections by induction over global reductions and projection structure.

A.2 Local types and CFSMs

The appendix verifies that translated local types yield basic CFSM properties and that the translation clauses are established mechanically by induction. These properties support the correspondence between local types and automata.

  • A.2 Local types and CFSMs: Translated local types satisfy determinism, directedness, and the absence of mixed sending and receiving states.
  • A.2 Local types and CFSMs: The appendix therefore supplies the basic-machine conditions needed for the paper’s local-type and CFSM characterisation.
  • A.2 Local types and CFSMs: The translation properties in both directions follow by induction on the CFSM or local-type structure and are described as mechanical.

B Appendix for Section 4

This appendix develops causality and diamond-property machinery for basic communicating machines, then uses multiparty compatibility to prove input availability. These lemmas support the appendix’s compatibility and synthesis arguments.

  • B Appendix for Section 4: The diamond property classifies independent transitions and provides the permutation basis for reordering compatible executions.
  • B Appendix for Section 4: The causality proof analyses alternating output and input causal chains and uses determinism, FIFO channels, directedness, and non-mixed states to exclude incompatible paths.
  • B Appendix for Section 4: Maximum causality decomposes executions so a maximum causal chain can be placed before the remaining execution without changing the reached state.
  • B Appendix for Section 4: Basic machines cannot contain a causal chain from one output to a different input on the same channel without an intervening matching input.
  • B Appendix for Section 4: Multiparty compatibility guarantees that after an output pp′!a, a corresponding input pp′?a becomes available after other machines perform independent internal communications.
  • B Appendix for Section 4: The general input-availability lemma extends this guarantee from a single output to the broader execution pattern established for basic multiparty-compatible systems.

B.1 Proofs of Theorem 4.1

The proof establishes stability by transforming executions into 1-bounded forms, then derives safety and liveness properties from stability and multiparty compatibility.

  • B.1 Proofs of Theorem 4.1: The stable property is proved by induction on the number of outstanding messages that must be matched by receptions.After all messages are closed, the execution can be made 1-bounded.
  • B.1 Proofs of Theorem 4.1: The proof repeatedly closes unmatched sending actions with corresponding receptions, applying compatibility and execution permutations.The construction handles successive sending states until a 1-bounded execution is reached.
  • B.1 Proofs of Theorem 4.1: Once stability holds, orphan-message freedom and reception-error freedom follow immediately, while liveness follows from orphan-message and deadlock-freedom.The remaining proof obligation is deadlock-freedom.
  • B.1 Proofs of Theorem 4.1: Deadlock-freedom is shown by advancing receiving states through a compatible 1-bounded execution until the resulting configuration is stable.Applying the argument to all receiving states completes the proof.

B.2 Proof for Lemma 4.1

The lemma proof shows that bounded traces can be simulated by rearranging causally independent actions, while the surrounding construction represents generalized control flow and projection.

  • B.2 Proof for Lemma 4.1: The induction proves that n-bounded trace equivalence implies (n+1)-bounded trace equivalence.The argument inducts on trace length and buffer usage.
  • B.2 Proof for Lemma 4.1: The proof isolates the last action and the last unmatched send, then uses commutation cases to construct a shorter or lower-buffer simulation.The cases distinguish sends and receives, including independent actions and conflicting choices.
  • B.2 Proof for Lemma 4.1: Causal dependencies prevent non-permutable action orders, while valid commutations preserve the transition sequence between the two systems.This enables the inductive simulation to be permuted back to the required trace.
  • Generalised global and local types: Generalized global types add fork, join, choice, and merge constructs to describe control-flow graphs beyond series-parallel syntax trees.The example models concurrent data transmission and logging, with local projections preserving the structure of the global type.
  • Generalised global and local types: Generalized local types retain sends, receives, concurrency, choices, joins, merges, indirection, and termination as state-machine-like constructs.Their syntax supports the corresponding generalized global-type projections.

C.2 Labelled transitions of generalised global and local types

The paper gives labelled semantics for generalized global and local types, proves their trace equivalence, and connects local types with CFSMs through Petri-net representations.

  • C.2 Labelled transitions of generalised global and local types: Global and local type LTSs model participant states together with communication-buffer contents, using asynchronous send and receive transitions.Global semantics also includes structural progression for participants not involved in a transition.
  • C.2 Labelled transitions of generalised global and local types: Projection is sound and complete: projected local types have semantics equivalent to the corresponding global type.The result is stated for both the generalized setting and the global-to-local LTS correspondence.
  • Translations between general local types and CFSMs: Local types translate to CFSMs by treating state variables as automaton states and local send or receive actions as labelled transitions.The initial state is the local type’s initial variable, with channels and message labels inherited from the type.
  • Translations between general local types and CFSMs: CFSMs translate back through Petri nets, whose regions preserve traces and expose concurrency before being converted into local-type transitions.The construction constrains the net’s initial and final places and the arity of labelled transitions.
  • Translations between general local types and CFSMs: Round-trip translation preserves traces but may return only an isomorphic local type rather than the original syntactic representation.This limitation appears in the data-transfer example.

C.4 Parallelism and local choice condition

For generalized interactions, compatibility is combined with concurrency-aware choice conditions to obtain stability, safety, and deadlock-freedom, with decidability restricted to bounded checks.

  • C.4 Parallelism and local choice condition: Generalized CFSM conditions extend classical ones because concurrent interactions invalidate the no-mixed-choice condition and require richer projectability constraints.The extension addresses parallelism in generalized multiparty session types.
  • C.4 Parallelism and local choice condition: A mixed-parallel state requires every send transition to satisfy the diamond property with every receive transition.This captures commutation between concurrent send and receive actions.
  • C.4 Parallelism and local choice condition: Under determinism, multiparty compatibility, mixed parallelism, and commuting-or-unique-sender receive choices, systems are stable and free of reception errors and orphan messages.The unique sender condition supplies input availability in the proof.
  • C.4 Parallelism and local choice condition: Adding the receiver condition yields deadlock-freedom for systems satisfying the preceding assumptions.Such systems are called session-compatible.
  • C.4 Parallelism and local choice condition: Multiparty compatibility is decidable for deterministic CFSMs, while receiver and unique-sender checks become decidable under compatibility when restricted to 1-bounded executions.Combined with synthesis, this identifies a decidable subset that yields well-formed global types.

C.5 Synthesis of general multiparty session automata

This section establishes that session-compatible communicating systems correspond to generalised multiparty session types and can be synthesised into equivalent global types.

  • C.5 Synthesis of general multiparty session automata: An algorithm synthesises a global type G from a session-compatible system S such that S ≈G.The construction restricts executions to the 1-bounded finite-state LTS, replaces matching send-receive pairs with global transitions, and converts the result through Petri nets.
  • C.5 Synthesis of general multiparty session automata: The synthesis construction first turns matching communications into transitions labelled by sender, receiver, and message before applying Petri-net and global-type conversions.This produces the global type whose behaviour is equivalent to the original communicating system.
  • C.5 Synthesis of general multiparty session automata: Session-compatible systems are exactly characterised by generalised multiparty session types: each compatible system corresponds to a global type, and each well-formed global type has a safe, live implementation.The stated safety and liveness properties include deadlock-freedom, reception error-freedom, and orphan message-freedom.
  • C.5 Synthesis of general multiparty session automata: The global-to-local projection maps a global send to an output at its sender, an input at its receiver, and no action at uninvolved participants.Parallel composition is preserved, while choices become internal or external choices depending on whether the participant is an active sender.
  • C.5 Synthesis of general multiparty session automata: The characterisation is supported by equivalence relations that identify structurally interchangeable parallel compositions in global and translated systems.Both relations include commutativity and associativity of parallel composition.

D.2 Proof of Proposition C.1

The proof derives contradiction from a supposedly permanently blocked input by combining receiver, determinacy, diamond, and multiparty-compatibility conditions.

  • D.2 Proof of Proposition C.1: The unique-sender condition ensures that the required action remains possible during the compatibility argument, unlike in the directed basic-CFSM setting.Without this condition, a transition used in the proof may not be enabled in the compared configuration.
  • D.2 Proof of Proposition C.1: A permanently blocked input with an empty queue would contradict the assumed reception-error freedom, orphan-message freedom, and stability properties.The proof reduces the issue to a reachable configuration containing an input state with no output from another participant.
  • D.2 Proof of Proposition C.1: When the blocked input is the first input at its participant, determinacy gives a distinct competing label, and compatibility makes both corresponding outputs available.This contradicts the assumption that the input state is deadlocked on its label.
  • D.2 Proof of Proposition C.1: When earlier inputs exist, the proof compares the first divergent actions of two executions and repeatedly applies the diamond property to reduce to the first case or contradict deadlock.The argument uses shorter execution prefixes until the contradiction is reached.
Loading 1304.1902v1…