Denote CSP with Temporal Formulas

This is a sequel of 1 to give a temporal semantics to a full version of CSP, including hiding operator and nested parallelism. The semantic definition is of denotational style, and employs set of temporal formulas as denotations. The continuity is proved, when the hiding operator is restricted to channels only with finite possible messages.