Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
A hierarchy of compositional models of I/O-Automata
RISE - Research Institutes of Sweden, ICT, SICS.
1991 (Engelska)Rapport (Övrigt vetenskapligt)
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.

Ort, förlag, år, upplaga, sidor
Kista, Sweden: Swedish Institute of Computer Science , 1991, 1. , s. 28
Serie
SICS Research Report, ISSN 0283-3638 ; R91:04
Nationell ämneskategori
Data- och informationsvetenskap
Identifikatorer
URN: urn:nbn:se:ri:diva-22172OAI: oai:DiVA.org:ri-22172DiVA, id: diva2:1041715
Anmärkning

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.

Tillgänglig från: 2016-10-31 Skapad: 2016-10-31 Senast uppdaterad: 2025-09-23Bibliografiskt granskad

Open Access i DiVA

fulltext(3530 kB)126 nedladdningar
Filinformation
Filnamn FULLTEXT01.pdfFilstorlek 3530 kBChecksumma SHA-512
0034c6ba04d95c7eab077c3fec46c2c008fb8acd43f22910f13a97980e49aad19871e497bd02a7a263af3e2466e4c92bc387782e61525cd8c74845e6c34a9004
Typ fulltextMimetyp application/pdf

Av organisationen
SICS
Data- och informationsvetenskap

Sök vidare utanför DiVA

GoogleGoogle Scholar
Totalt: 126 nedladdningar
Antalet nedladdningar är summan av nedladdningar för alla fulltexter. Det kan inkludera t.ex tidigare versioner som nu inte längre är tillgängliga.

urn-nbn

Altmetricpoäng

urn-nbn
Totalt: 74 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf