September 5, 2025
Process Calculi II: Modeling Handshaking and Handwashing Protocols in CCS
Participants: _vgr, ediblebadger, timber1997, plague_year, zoesh, nattfrosten, giovanni.merlino, .unipuff, ananth9921
The SIGFPT group continued their process calculi track by applying CCS formalism to model real-world protocols: handshaking and handwashing. The session began with a recap of previous material and leveraged LLMs to generate notation references and worked examples. Participants brainstormed relevant modeling dimensions and then independently developed formal specifications, with several novel approaches emerging.
Key contributions included: _vgr's basic CCS handshake model; nattfrosten's three-agent handwashing system (NEED, POSTER, HUMAN) capturing the cognitive reminder loop; giovanni.merlino's π-calculus variant using name passing for partner selection in crowds and CSP variant for explicit refusal/consent modeling; and .unipuff's detailed handwashing specification accounting for different initial states (dirty, oily, clean) with corresponding action sequences. Participants identified interesting safety, liveness, and mutual exclusion properties to investigate further.
The group highlighted compliance as a critical formalization challenge—protocol correctness depends on hidden assumptions and expectations not always explicit in the specification. Future work includes applying Allen's temporal interval calculus to add duration semantics and further composing simple protocols into larger systems to identify interesting trace behaviors.
- CCS provides a tractable framework for modeling prototypical protocols like handshaking and handwashing by explicitly representing agents, states, and transitions, though some participants found the notation unintuitive initially.
- π-calculus with name passing enables elegant modeling of dynamic partner selection in crowd scenarios by using public channels for rendezvous and private channels for actual interaction.
- Handwashing can be naturally modeled as a multi-state system with different initial conditions (dirty, oily, clean) requiring different action sequences, capturing real-world complexity beyond simple protocols.
- Compliance in protocols relates to hidden expectations and assumptions that may need to be formalized as hidden events in CSP, raising questions about what constitutes correct protocol adherence.
- LLMs proved valuable for quickly generating notation cheat sheets and simple examples, reducing cognitive overhead in technical skill acquisition.