CSP: Semantik (Spur-Semantik)

zu P∈$\mathbb {P}$ (E) konstruiere Automaten A (mit ε-Übergängen) über E.

Die Spur-Sprache von P : = die Sprache von A

Startzustand von A ist P, Übergangsrelation von A ist:

• (a→P)$\;\stackrel{{a}}{{\to}}\;$P
• (STOP;Q)$\;\stackrel{{\epsilon}}{{\to}}\;$Q,     wenn P$\;\stackrel{{a}}{{\to}}\;$P', dann (P;Q)$\;\stackrel{{a}}{{\to}}\;$(P';Q),

• (P$\Box$Q)$\;\stackrel{{\epsilon}}{{\to}}\;$P,      (P$\Box$Q)$\;\stackrel{{\epsilon}}{{\to}}\;$Q

• a∈C∧P$\;\stackrel{{a}}{{\to}}\;$P'∧Q$\;\stackrel{{a}}{{\to}}\;$Q'⇒(P|_CQ)$\;\stackrel{{a}}{{\to}}\;$(P'|_CQ'),

• a $\notin$C∧P$\;\stackrel{{a}}{{\to}}\;$P'⇒(P|_CQ)$\;\stackrel{{a}}{{\to}}\;$(P'|_CQ),

• a $\notin$C∧Q$\;\stackrel{{a}}{{\to}}\;$Q'⇒(P|_CQ)$\;\stackrel{{a}}{{\to}}\;$(P|_CQ'),

• P^*$\;\stackrel{{\epsilon}}{{\to}}\;$STOP,      P^*$\;\stackrel{{\epsilon}}{{\to}}\;$(P;P^*).