UCS, LTS Semantics

[2.3]

• An operational semantics using labelled transition systems.
  • States $S$, initial state $P_0 \in S$, labels $L$.
  • Transition $P \xrightarrow{x} Q$ where $x \in L$.
  • Special invisible action $\tau \in L$ unobservable/uncontrollable by environment.
• Traces calculable from LTS, FDR works on LTS instead of trace-sets.
• Process in FDR
  • Starts in initial state.
  • If state has outward-pointing visible actions, offers these actions to environment to synchronize.
  • Agrees to environment’s offered action if no $\tau$ actions.
  • May follow $\tau$ actions instead if available.

$$\mu\, p.\, (a \to p) \sqcap (b \to p)$$