Paper Info
Title
Deriving Bisimulation Congruences for Reactive Systems
Abstract
The dynamics of reactive systems, e.g. CCS, has often been defined using a labelled transition system (LTS). More recently it has become natural in defining dynamics to use reaction rules - i.e. unlabelled transition rules - together with a structural congruence. But LTSs lead more naturally to behavioural equivalences. So one would like to derive from reaction rules a suitable LTS. This paper shows how to derive an LTS for a wide range of reactive systems. A label for an agent a is defined to be any context F which intuitively is just large enough so that the agent Fa ("a in context F") is able to perform a reaction. The key contribution of this paper is a precise definition of "just large enough", in terms of the categorical notion of relative pushout (RPO), which ensures that bisimilarity is a congruence when sufficient RPOs exist. Two examples - a simplified form of action calculi and term-rewriting - are given, for which it is shown that sufficient RPOs indeed exist. The thrust of this paper is, therefore, towards a general method for achieving useful behavioural congruence relations.
Year
DOI
Venue
2000
10.1007/3-540-44618-4_19
CONCUR
Keywords
Field
DocType
agent fa,sufficient rpos,suitable lts,reactive system,reaction rule,context f,structural congruence,labelled transition system,useful behavioural congruence relation,reactive systems,large enough,deriving bisimulation congruences
Transition system,Discrete mathematics,Bigraph,Computer science,Pushout,Bisimulation,Reactive system,Process calculus,Congruence (geometry),Congruence relation
Conference
ISBN
Citations 
PageRank 
3-540-67897-2
115
5.17
References 
Authors
20
2
Search Limit
100115
Name
Order
Citations
PageRank
James J. Leifer124412.67
Robin Milner24037751.80