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 |