Semantics of parallelism. Non-interleaving representation of behaviour

Publication date 14 December 1997

asynchronous transition systems concurrent systems discrete behavioral presentations morphisms between trace languages process algebras

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to computer science (68-02) Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Semantics in the theory of computing (68Q55)

Review text

There is a wide variation among formal theories of concurrent systems both in terms of their syntax and their semantics. In this book, an attempt is made to compare these theories at the semantic level, based on an automata theory for concurrent systems. The automata in question, rather than generating sets of sequences, effectively generate systems of labelled preordered sets which model possible behaviors of the system, the preorder being interpreted as ``no later than. Characteristically, these automata and the objects which represented their possible behaviors are designed to model both concurrency and/or simultaneity explicit. This is in contrast to the interleaving approach favored by the proponents of process algebras. The book starts with a definition of behavioral presentations and the basic temporal relations which they determine. A particular subclass, the discrete behavioral presentations, are then formally characterized. The principal order-theoretic properties of a class of behavioral presentations are discussed, which includes those that are discrete. These properties play a crucial part in relating behavioral presentations to trace and vector languages, thereby building a bridge between order-theoretic and algebraic representation of behavior. Next, the relationship between the behavioral presentation model and two kinds of event structure is examined. It is shown that event structures correspond to behavioral presentations which are closed; equivalently, which are prime algebraic and coherent. In the following chapters, a characterization of important synchronic properties is given. It is used to define a semantics based on behavioral presentations for Karp and Miller computation graphs in order to show that the behavioral presentations, which are images of computation graphs under this semantics, have such properties. After that, algebraic ways of representing behavior, via trace and vector languages, are considered. The equivalence of the two representations is shown, order-theoretic properties of certain kinds of these languages (those which are left-closed with respect to the ordering on traces or vectors) are demonstrated. It turns out that every such language determines a discrete behavioral presentation. The author characterizes, up to isomorphism, the behavioral presentations which may be obtained by construction from left-closed trace languages, so-called iota-linuistic behavioral presentations. The theory developed so far is used to characterize the structure of vector languages having certain determinacy and finiteness properties. In the next chapter, the automata-theoretic aspects of the theory are dealt with, by showing how to associate a (necessarily sequential) behavioral presentation with an unambiguous transition system with initial state. It is shown that this semantics establishes a bijection between a certain class of equivalence classes of unambiguous transition systems and a certain class of equivalence classes of behavioral presentations. The equivalence relations concerned are isomorphism, in the case of behavioral presentations and a form of strong equivalence as defined by Milner for CCS. The next chapter considers non-sequential automata with the introduction of asynchronous transition systems. These are shown to determine left-closed trace languages and, hence, iota-linguistic behavioral presentations. A relation between as asynchronous transition systems with initial states is defined and it is proved that two such automata are in this relation if and only if they determine isomorphic behavioral presentations. In the following chapters, the condition/event model of Petri is described, together with a non-interleaving semantics based on process nets. Also, an alternative semantics based on asynchronous transition systems is introduced and shown that the two semantics are equivalent. Next, the loosely-coupled systems model is introduced and a semantics based on asynchronous transition systems is attached to it. After that, notions of morphisms between trace languages, asynchronous transition systems and discrete behavioral presentations are examined. All three classes of object become categories, which are then seen to be strongly structurally related. Asynchronous transitions systems are related to certain ideas in category theory and to previously established semantics. As a consequence, the author is able to show that every loosely coupled system may be represented by a net, and, hence, derives a construction which builds a net from a loosely coupled system in such a way that the two have the same meaning within the asynchronous transition system semantics. Finally, the general automata model is met, that of hybrid transition systems. It is shown that any discrete behavioral presentation may arise as the behavioral semantics of such automata and that, in fact, such automata have precisely discrete behavioral presentations as their behavioral semantics. The following chapters see an application of hybrid transition systems to provide a non-interleaving semantics for a net-based model of parallel computation due to Keller, the path/process notations that lies at the centre of the COSY notation and to the process model of Nivat and Arnold. Finally, constructions on automata are described used to provide non-interleaving semantics for CCS and a subset of TCSP. In each case, the author shows that the semantics associated with these notations may be recovered from the semantics proposed in this book, effectively by removing concurrency.

Recommendations

Cited in

(6)

This page was built for publication: Semantics of parallelism. Non-interleaving representation of behaviour

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4372486)