This document is best viewed in "raw format" on github.
The LTS (labelled transition system, or SOS, for structural operational semantics) of CSSK is the set of "reduction rules" describing how the system reacts / evolves. It is given, for instance, in Forward-Reverse Observational Equivalences in CCSK (page 4, for the forward-only system), or in this exercise sheet.
For simplification, we have written these rules down in 'ascii' format. They are as follows:
+-----------------------------------------------+---------------------------------------------------------------------+
| Rule | Example(s) |
+:=============================================:+:===================================================================:+
| | - `a.P -a[k0]-> a[k0].P` | | | - `a.b.P -a[k0]-> a[k0].b.P` | | | | | std(X)------------------ (top) | | | a.X -a[m]-> a[m].X | | | | | | | | | | |
+-----------------------------------------------+---------------------------------------------------------------------+
| | - `a[k0].b.P -b[k1]-> a[k0].b[k1].P` | | | - `a[k0].(b.X|Y) -b[k1]-> a[k0].(b[k1].X|Y)` | | | | | X -b[n]-> X' | | | m neq n------------------------ (pre.) | | | a[m].X -b[n]-> a[m].X' | | | | | | | | | | |
+-----------------------------------------------+---------------------------------------------------------------------+
| | - `a.P\{b} -a[k0]-> a[k0].P\{b}` | | | | | | | | X -z[m]-> X' | | | z notin {a, 'a} --------------------- (res.) | | | X\{a} -z[m]-> X'\{a} | | | | | | | | | | |
+-----------------------------------------------+---------------------------------------------------------------------+
| | - `a.P|b.Q -a[k0]-> a[k0].P|b.Q` | | | | | | | | X -a[m]-> X' | | | m notin keys(Y)-------------------- (|L) | | | X|Y -a[m]-> X'|Y | | | | | | | | | | |
+-----------------------------------------------+---------------------------------------------------------------------+
| | - `a.P|b.Q -b[k0]-> a.P|b[k0].Q` | | | | | | | | Y -a[m]-> Y' | | | m notin keys(X)-------------------- (|R) | | | X|Y -a[m]-> X|Y' | | | | | | | | | | |
+-----------------------------------------------+---------------------------------------------------------------------+
| | - `a.P + b.Q -a[k0]-> a[k0].P + b.Q` | | | | | | | | X -a[m]-> X' | | | std(Y)------------------------ (+L) | | | X+Y -a[m]-> X'+Y | | | | | | | | | | |
+-----------------------------------------------+---------------------------------------------------------------------+
| | - `a.P + b.Q -b[k0]-> a.P + b[k0].Q` | | | | | | | | Y -a[m]-> Y' | | | std(X)------------------------ (+R) | | | X+Y -a[m]-> X+Y' | | | | | | | | | | |
+-----------------------------------------------+---------------------------------------------------------------------+
| | - `a.P|'a.Q -Tau{a,'a}[k0]-> Tau{a,'a}[k0].P|Tau{a,'a}[k0].Q` | | | | | | | | X -a[m]-> X' Y -'a[m]-> Y' | | | -------------------------------- (syn.) | | | X|Y -Tau{a,'a}[m]-> X'|Y' | | | | | | | | | | |
+-----------------------------------------------+---------------------------------------------------------------------+