Step semantics for "true'' concurrency with recursion

We present a variety of denotational linear time semantics for a language with recursion and true concurrency in a form of synchronous co-operation, which in the literature is known as step semantics. We show that this can be done by a generalization of known results for interleaving semantics. A general method is presented to define semantical operators and denotational semantics in the Smyth powerdomain of streams. With this method, first a naive and then more sophisticated semantics for synchronous co-operation are developed, which include such features as interleaving and synchronization. Then we refine the semantics to deal with a bounded number of processors, subatomic actions, maximal parallelism and a real-time operator. Finally, it is indicated how to apply these ideas to branching-time models, where it becomes possible to analyze deadlock behaviour as well as a form of true concurrency.