Hostname: page-component-586b7cd67f-l7hp2 Total loading time: 0 Render date: 2024-11-25T02:31:57.793Z Has data issue: false hasContentIssue false

Structured transition systems with parametric observations: observational congruences and minimal realizations

Published online by Cambridge University Press:  01 June 1997

GIANLUIGI FERRARI
Affiliation:
Dipartimento di Informatica, Università di Pisa, Corso Italia 40, I-56100 Pisa, Italy
UGO MONTANARI
Affiliation:
Dipartimento di Informatica, Università di Pisa, Corso Italia 40, I-56100 Pisa, Italy
MIRANDA MOWBRAY
Affiliation:
Hewlett-Packard Labs, Filton Road, Stoke Gifford, Bristol BS126QZ, UK

Abstract

A large number of observational semantics for process description languages have been developed, many of which are based on the notion of bisimulation. In this paper, we consider in detail the problem of defining a semantic framework to unify these. The discussion takes place in a purely algebraic setting. We introduce a special class of algebras called Structured Transition Systems. A structured transition system can be viewed as a transition system with an algebraic structure both on states and transitions. In this framework, observations of behaviours are dealt with by means of maps from the transitions to some algebra of observations.

Using several examples, we show that this framework allows us to describe a range of observational semantics within a single underlying presentation: it is enough to consider different mappings and algebras of observations. Furthermore, we introduce a notion of bisimulation that is parameterized with respect to the choice of the algebra of observations, and we find circumstances under which a Structured Transition System has good properties with respect to this parameterized bisimulation.

First, some general syntactic constraints, independent from the choice of the algebra of the observations, are given for Structured Transition System presentations. We show that these constraints ensure that parameterized bisimulation is always a congruence. Next, we address the problem of Minimal Realizations. We show that when the presentation satisfies the syntactic constraints there exists a minimal realization, i.e., there is a model of the presentation whose elements fully characterize congruence classes under bisimulation.

Type
Research Article
Copyright
1997 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Footnotes

This research was supported by, and collaboratively carried out at, Hewlett-Packard Laboratories, Pisa Science Centre, and by CNR project ‘Strumenti per la specifica e la verifica di proprietà critiche di sistemi concorrenti e distribuiti’.