Jonsson, Bengt (1991) A hierarchy of compositional models of I/O-Automata. [SICS Report]
A semantic model of computer systems is compositional if it adequately represents the behavior of the modeled systems in a context of other systems. A compositional model is thus a good basis for specifying and reasoning about systems in a modular fashion. I/O-automata is a class of communicating system which can represent several types of asyncronously communicating systems, such as message-passing distributed systems, systems with broadcast communication, and systems with shared variables. In contrast to many other classes of communicating systems (e.g. in CCS or CSP), semantic models based only on traces(sequences of communication events) can in a compositional way represent safety, liveness and many other proportiesd of I/O-automata. In this paper, we investigate which semantic models of I/O-automata are compositional, and which are not. The investigation is confined to models based on traces. We study a number of trace-based semantical models of I/O-automata, which differ in their capability to represent safety, liveness, termination, and divergence properties. The defined models can be naturally ordered into a hierarchy, according to how much information they convey about the modeled systems. The main contribution of the paper is an investigation of whether there are other compositional models between adjacent compositional models in our hierarchy. Surprisingly enough, we can prove that for several pairs of adjacent models in the hierarchy, the gap between the two models contains no other compositional model. For instance, the nonexistence of a compositional model in the gap between a model that represents safety properties and a model that represents liveness properties means that liveness properties cannot be only partially represented if compositionality is desired. We indicate how our results can be applied to derive results about full abstraction.
|Item Type:||SICS Report|
|Additional Information:||An extended abstract of this research report has appeared under the same title in the Proceedings of the Symposium on mathematical Foundations of Computer Science, Banska Bystrica, Czeckoslovakia, Aug. 1990. published as vol. 452 of Lecture notes in Computer Science, Springer Verlag, pp347-354.|
|Deposited By:||Vicki Carleson|
|Deposited On:||22 Oct 2009|
|Last Modified:||18 Nov 2009 16:09|
Repository Staff Only: item control page