1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
//! # Process Algebra
//!
//! Process algebras provide mathematical frameworks for describing and reasoning about
//! concurrent and communicating systems. The two major calculi are:
//!
//! ## CCS — Calculus of Communicating Systems (Milner, 1980)
//!
//! CCS processes are defined by:
//! ```text
//! P ::= 0 -- nil (deadlock/stop)
//! | α.P -- action prefix (α ∈ Act)
//! | P + Q -- nondeterministic choice
//! | P | Q -- parallel composition
//! | P\L -- restriction (hide labels in L)
//! | P\[f\] -- relabeling by function f
//! | X -- process variable
//! | μX.P -- recursive definition
//! ```
//!
//! ## CSP — Communicating Sequential Processes (Hoare, 1978)
//!
//! CSP extends CCS with:
//! - **Synchronous parallel** `P ‖ Q` (must synchronize on shared events)
//! - **Alphabetized parallel** `P ‖_A Q`
//! - **Sequential composition** `P ; Q`
//! - **Interrupt** `P △ Q`
//! - **Failures/divergence** semantics
//!
//! ## Key Equivalences
//!
//! - **Bisimulation**: processes `P ~ Q` if they can simulate each other step-by-step
//! - **Weak bisimulation**: ignores internal τ-transitions
//! - **Trace equivalence**: processes accept the same sequences of visible actions
//! - **Failures equivalence**: traces + sets of refusals
//! - **Testing equivalence**: indistinguishable by all tests
//!
//! ## Hennessy-Milner Logic (HML)
//!
//! Modal logic for describing process properties:
//! ```text
//! φ ::= tt | ff | φ ∧ ψ | φ ∨ ψ | ¬φ | ⟨α⟩φ | \[α\]φ
//! ```
//! - `⟨α⟩φ`: can do α and then satisfy φ (diamond modality)
//! - `[α]φ`: every α-transition leads to a state satisfying φ (box modality)
pub use *;
pub use *;