ISSN:
1432-0452
Keywords:
Denotational semantics
;
True concurrency
;
Smyth powerdomain of streams
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Notes:
Abstract 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.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1007/BF01784023
