Shared flowchart

Software · L5 · Process Calculi Landscape

Sign in to clone

How CSP and the π-calculus relate through labelled transition systems, and how bisimulation and model checking sit on top.

by @openstemUpdated Software
CSP: synchronous events, static channelsLabelled Transition System (S, Act, →)π-calculus: mobile, first-class channel namesTrace equivalence (too coarse)Bisimulation: step-by-step matchingStrong bisimulation: matches every actionWeak bisimulation: abstracts τ-actionsModel checking: M, s0 ⊨ φState explosion: k^n global statesPartial-order reduction / BDDsmitigate

We use privacy-friendly product analytics (no session recording, PII masked) to improve OpenStem. Load analytics? Privacy Policy