• barbed semantics
• graphical encodings
• mobile ambients
• reactive systems

Reactive systems represent a meta-framework aimed at deriving behavioral congruences for those specification formalisms whose operational semantics is provided by rewriting rules.
The aim of this thesis is to address one of the main issues of the framework, concerning the adequacy of the standard observational semantics (the IPO and the saturated one) in modelling the concrete semantics of actual formalisms. The problem is that IPO-bisimilarity (obtained considering only minimal labels) is often too discriminating, while the saturated one (via all labels) may be too coarse, and intermediate proposals should then be put forward.
We then introduce a more expressive semantics for reactive systems which, thanks to its flexibility,
allows for recasting a wide variety of observational, bisimulation-based equivalences. In particular, we propose suitable notions of barbed and weak barbed semantics for reactive systems, and an efficient characterization of them through the IPO-transition systems.
We also propose a novel, more general behavioural equivalence: L-bisimilarity, which is able to recast both its IPO and saturated counterparts, as well as the barbed one. The equivalence is parametric with respect to a set L of reactive systems labels, and it is shown that under mild conditions on L it is a congruence.
In order to provide a suitable test-bed, we instantiate our proposal over the asynchronous CCS and, most importantly, over the mobile ambients calculus, whose semantics is still in a flux.