C := Post - Pre
Post := P x T → N

T-flux := x | C.x = 0
T-semiflux := x ≥ 0 
∃ m  ∃σ | m[σ>m

∀m∈RS(S)  ∑y(pᵢ)m(pᵢ) = ∑y(pᵢ)m₀(pᵢ)

liveness:
liveness (t) := ∀m∈RS(m0) ∃σ | m[σ>m' ∧ m'[t>
CTL - liveness (t) : AG(EF t)

SOS:
Algebra := PA + SOS + Label

E →μ E'
———————— 
E || F →μ E' || F

F →μ F'
—————————
E || F →μ F'


CSP (||) := E ||ₙ F   |   E\\F    | E [[l]] F

E →μ E' 
———————– μ∈Int
E ||ₙ F →τ E' || F

E →μ E'
————————— μ ∈ Ext
E \\ F →μ E' \\ F