Skip to content

mpst

Multiparty Session Types for specifying and verifying multi-party communication protocols.

This module provides global type definitions, local type projection, well-formedness checking, runtime session monitoring, and 4 communication patterns.

Multiparty Session Types (MPST) for formal protocol verification.

This module provides a comprehensive framework for specifying and verifying multi-agent communication protocols using session types.

Based on: Honda, Yoshida, Carbone (2008) - Multiparty Session Types

Key Components: - Global Types: Bird's-eye view of session choreography - Local Types: Participant-specific session behavior - Projection: Global → Local type derivation - Type Checking: Static verification of well-formedness - Session Monitoring: Runtime conformance checking

Example

Define a request-response protocol

from agenticraft_foundation.mpst import ( msg, end, request_response, Projector, SessionTypeChecker, )

Using the convenience pattern

protocol = request_response("client", "server")

Or build manually

protocol = msg("client", "server", "request", msg("server", "client", "response"))

Project to local types

projector = Projector() client_type = projector.project(protocol, "client") server_type = projector.project(protocol, "server")

Verify well-formedness

checker = SessionTypeChecker() result = checker.verify_global(protocol) print(f"Well-formed: {result.is_valid}")

Submodules

Module Description
types Session type definitions
global_types Global type specification for multi-party protocols
local_types Local type projection per role
checker Well-formedness checking
patterns 4 communication patterns