Complete multiparty session type projection with automata

DOI10.1007/978-3-031-37709-9_17zbMATH Open1547.68506MaRDI QIDQ6535693

Thomas Wies, Elaine Li, Damien Zufferey, Felix Stutz

Publication date: 1 February 2024

zbMATH Keywords

deadlock freedomprotocol verificationcommunicating state machinesmultiparty session typesprotocol fidelity

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Analysis of a class of communicating finite state machines
• Multiparty session types, beyond duality
• On the boundary between decidability and undecidability of asynchronous session subtyping
• Realizability and verification of MSC graphs
• Realizability of high-level message sequence charts: closing the gaps
• Session coalgebras: a coalgebraic view on session types and communication protocols
• Certifying data in multiparty session types
• Verification of programs with half-duplex communication
• A Gentle Introduction to Multiparty Asynchronous Session Types
• On Global Types and Multi-Party Session
• Multiparty Session Types Meet Communicating Automata
• Context-free session types
• On the Undecidability of Asynchronous Session Subtyping
• Multiparty asynchronous session types
• On Communicating Finite-State Machines
• Time, clocks, and the ordering of events in a distributed system
• Data Communicating Processes with Unreliable Channels
• Non axiomatisability of positive relation algebras with constants, via graph homomorphisms
• Multiparty Compatibility in Communicating Automata: Characterisation and Synthesis of Global Session Types
• Meeting Deadlines Together
• Context-Bounded Analysis of Concurrent Queue Systems
• Parameterised Multiparty Session Types
• Verifying asynchronous interactions via communicating session automata
• Generalising Projection in Asynchronous Multiparty Session Types.
• Generalised multiparty session types with crash-stop failures
• Comparing the expressive power of the synchronous and asynchronous \(\pi\)-calculi

This page was built for publication: Complete multiparty session type projection with automata