Discrete time process algebra and the semantics of SDL

We present an extension of discrete time process algebra with relative timing where recursion, propositional signals and conditions, a counting process creation operator, and the state operator are combined. Except the counting process creation operator, which subsumes the original process creation operator, these features have been developed earlier as largely separate extensions of time free process algebra. The change to the discrete time case and the combination of the features turn out to be far from trivial. We also propose asemantics for a simplified version of SDL, using this extension of discrete time process algebra to describe the meaning of the language constructs. This version covers all behavioural aspects of SDL, except for communication via delaying channels - which can easily he modelled. The semantics presented here facilitates the generation of finitely branching transition systems for SDL specifications and thus it enables validation