algebra¶
CSP process algebra for modeling multi-agent coordination.
This module provides 13 CSP operators (8 core primitives + 5 agent-specific extensions), operational semantics (LTS construction, trace extraction, deadlock detection), process equivalence checking, refinement verification, and 6 coordination patterns.
Process Algebra module for formal verification of agent coordination.
This module provides: - CSP (Communicating Sequential Processes) primitives - Labeled Transition Systems (LTS) for operational semantics - Process equivalence (trace equivalence, bisimulation) - Refinement checking for specification verification - Coordination patterns for multi-agent systems
Based on: - Hoare (1985) - Communicating Sequential Processes - Milner (1980) - Calculus of Communicating Systems - Roscoe (1998) - The Theory and Practice of Concurrency
Submodules¶
| Module | Description |
|---|---|
csp |
13 process classes — Stop, Skip, Prefix, ExternalChoice, InternalChoice, Parallel, Sequential, Hiding, Interrupt, Timeout, Guard, Rename, Pipe, Recursion, Variable |
semantics |
LTS construction, trace extraction, deadlock detection |
equivalence |
Trace equivalence, bisimulation, failures equivalence |
refinement |
Trace, failures, and failures-divergence refinement |
patterns |
6 coordination patterns |