Record Details

A Characterization of Finitary Bisimulation

BRICS Report Series

View Archive Info
 
 
Field Value
 
Title A Characterization of Finitary Bisimulation
 
Creator Aceto, Luca
Ingólfsdóttir, Anna
 
Description Following a paradigm put forward by Milner and Plotkin, a primary criterion to judge the appropriateness of denotational models for programming and specification languages is that they be in agreement with operational intuition about program behaviour. Of the "good t" criteria for such models that have beendiscussed in the literature, the most desirable one is that of full abstraction.Intuitively, a fully abstract denotational model is guaranteed to relate exactly all those programs that are operationally indistinguishable with respect to some chosen notion of observation. Because of its prominent role in process theory, bisimulation [12] has been a natural yardstick to assess the appropriateness of denotational models for several process description languages. In particular, when proving full abstractionresults for denotational semantics based on the Scott-Strachey approach for CCS-like languages, several preorders based on bisimulation have been considered; see, e.g., [6, 3, 4]. In this paper, we shall study one such bisimulationbasedpreorder whose connections with domain-theoretic models are by now well understood, viz. the prebisimulation preorder . investigated in, e.g., [6, 3]. Intuitively, p < q holds of processes p and q if p and q can simulate each other'sbehaviour, but at times the behaviour of p may be less specified than that of q. A common problem in relating denotational semantics for process descriptionlanguages, based on Scott's theory of domains or on the theory of algebraic semantics, with behavioural semantics based on bisimulation is that the chosen behavioural theory is, in general, too concrete. The reason for this phenomenon is that two programs are related by a standard denotational interpretation if, in some precise sense, they afford the same finite observations. On the other hand, bisimulation can make distinctions between the behaviours of two processesbased on infinite observations. (Cf. the seminal study [1] for a detailed analysis of this phenomenon.) To overcome this mismatch between the denotationaland the behavioural theory, all the aforementioned full abstraction results are obtained with respect to the so-called finitely observable, or finitary, part of bisimulation. The finitary bisimulation is defined on any labelled transition system thus: p
 
Publisher Aarhus University
 
Date 1997-01-26
 
Type info:eu-repo/semantics/article
info:eu-repo/semantics/publishedVersion
 
Format application/pdf
 
Identifier https://tidsskrift.dk/brics/article/view/18952
10.7146/brics.v4i26.18952
 
Source BRICS Report Series; No 26 (1997): RS-26 A Characterization of Finitary Bisimulation
BRICS Report Series; Nr. 26 (1997): RS-26 A Characterization of Finitary Bisimulation
1601-5355
0909-0878
 
Language eng
 
Relation https://tidsskrift.dk/brics/article/view/18952/16591