The semantics of tcc is deﬁned as a function [[·]] which associates to each process a set of infinite sequences of constraints. We use C^{ω} to denote the set of infinite sequence of constraints in an underlying constraint system.

The semantic equations are described below:

Recall that [[P]] aims at capturing the strongest postcondition (or quiescent sequences) of a process P. So, **skip** cannot add any information to any sequence (Equation **DSkip**). The sequences to which **tell** ( c ) cannot add information are those whose first element entails c (Equation **DTell**). A sequence s is in
[[**when** c **do** P ]] if either s(1) cannot entail the guard c or s(1) entails c and is quiescent for Q (Equation **DAsk**). A sequence is quiescent for P || Q if it is for P and Q (Equation **DPar**).

The process **next** P has no influence on the first element of a sequence, thus d.s is quiescent for it if s is quiescent for P (Equation **DNext**). A similar explanation can be given for the process **unless** c **next** P (Equation **DUnl**). A sequence s is quiescent for !P if every suffix of s is quiescent for P (Equation **DRep**).

We say that s is an x-variant of s' if ∃x.s(i)=∃x.s'(i) for i>0 (i.e. s and s' differ only on the information about x). A sequence s is quiescent for Q=(**local** x;c )P if there exists an x-variant s' of s s.t. s' is quiescent for P and s'(1) entails c. Hence, if P cannot add any information to s' then Q cannot add any information to s.