← Formal Protocol Theory

October 3, 2025

SIGFPT Process Calculi 3: Labeled Transition Systems and Structural Operational Semantics

Labeled Transition Systems (LTS) and their role in formalizing CCS processesStructural Operational Semantics (SOS) as inductive rules for valid transitionsBisimulation as a core equivalence notion in process calculiNotation challenges in process calculus (+ for choice, | for parallelism)Actor model as alternative concurrent system frameworkRelationship between process calculi and state diagrams/FSMs

Participants: _vgr, ediblebadger, mtraven, heterotic, .unipuff, timber1997, maparent

The SIGFPT group continued its deep dive into process calculi with a focus on how CCS processes are formalized as Labeled Transition Systems and governed by Structural Operational Semantics. Ediblebadger led the session with multiple presentations of related concepts, laying groundwork for future discussion of bisimulation as a key equivalence notion. The group discussed notation challenges, particularly around the use of '+' for nondeterministic choice and '|' for parallelism, with some participants finding the mathematical notation unintuitive despite its standardness in formal semantics. The conversation also touched on alternative approaches like the actor model and connections to conversation analysis. Discussion of broader SIG organizational questions emerged regarding BDFQ (presumably facilitators) roles and writing audiences, with acknowledgment that the material's abstractness is justified as a trade-off favoring mathematical precision over accessibility.

  • Labeled Transition Systems provide a precise mathematical foundation for CCS processes, with Structural Operational Semantics formalizing valid transitions through inductive rules.
  • The notation used in process calculi (particularly + for nondeterministic choice and | for parallelism) presents usability challenges for designers despite being mathematically standard.
  • Abstractness in formal systems may be less exclusionary than prerequisite material requirements; the group compared this favorably to category theory adoption in other SIG channels.
  • Process calculi can be interpreted as directed graphs or state diagrams, making them tractable for understanding concurrent systems without requiring extensive background knowledge.
Links discussed
View discussion in Discord →