Skip to content

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