Abstract
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 a semantics 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 be modelled.
The semantics presented here facilitates the generation of finitely
branching transition systems for SDL specifications and thus it
enables validation.
Preprint available here.