Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
A hierarchy of compositional models of I/O-Automata
RISE - Research Institutes of Sweden, ICT, SICS.
1991 (English)Report (Other academic)
Abstract [en]

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.

Place, publisher, year, edition, pages
Kista, Sweden: Swedish Institute of Computer Science , 1991, 1. , p. 28
Series
SICS Research Report, ISSN 0283-3638 ; R91:04
National Category
Computer and Information Sciences
Identifiers
URN: urn:nbn:se:ri:diva-22172OAI: oai:DiVA.org:ri-22172DiVA, id: diva2:1041715
Note

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.

Available from: 2016-10-31 Created: 2016-10-31 Last updated: 2018-02-07Bibliographically approved

Open Access in DiVA

fulltext(3530 kB)90 downloads
File information
File name FULLTEXT01.pdfFile size 3530 kBChecksum SHA-512
0034c6ba04d95c7eab077c3fec46c2c008fb8acd43f22910f13a97980e49aad19871e497bd02a7a263af3e2466e4c92bc387782e61525cd8c74845e6c34a9004
Type fulltextMimetype application/pdf

By organisation
SICS
Computer and Information Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 90 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

urn-nbn

Altmetric score

urn-nbn
Total: 46 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf