A Characterization of Finitary Bisimulation

Resumé

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 been
discussed 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 abstraction
results 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 bisimulationbased
preorder 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's
behaviour, but at times the behaviour of p may be less specified than that of q.
A common problem in relating denotational semantics for process description
languages, 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 processes
based on infinite observations. (Cf. the seminal study [1] for a detailed analysis of this phenomenon.) To overcome this mismatch between the denotational
and 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 <^F q iff t < p implies t < q, for every finite synchronization tree t.
An alternative characterization of the finitary bisimulation for arbitrary transition systems has been given by Abramsky in [1]. This characterization is couched in logical terms, and is an impressive byproduct of Abramsky's "theory
of domains in logical form" programme. More precisely, Abramsky shows that two processes in any transition system are equated by the finitary bisimulation
iff they satisfy the same formulae in the finitary version of the domain logic for transition systems. The existence of this logical view of the finitary bisimulation gives us a handle to work with this relation. However, an alternative,
behavioural view of the finitary bisimulation might be more useful when establishing results which are more readily shown on the behavioural, rather than on the logical, side. Examples of such results are complete axiomatizations for
the finitary bisimulation and full abstraction results. A behavioural characterization of the finitary bisimulation would also provide an easier way to establish when two processes in a transition system are related by it or not, thus giving more insight on the kind of identifications made by this relation. In this study, we offer a behavioural characterization of the finitary bisimulation
for arbitrary transition systems (cf. Thm. 3.5). This result may be seen as the behavioural counterpart of Abramsky's logical characterization theorem [1, Thm. 5.5.8]. Moreover, for the important class of sort-finite transition systems
we present a sharpened version of a behavioural characterization result first proven by Abramsky in [3, Propn. 6.13]. The interested reader may consult the unpublished report [5] for more results on the finitary bisimulation.