logo SBA

ETD

Digital archive of theses discussed at the University of Pisa

 

Thesis etd-05282011-172623


Thesis type
Tesi di dottorato di ricerca
Author
MONREALE, GIACOMA
URN
etd-05282011-172623
Thesis title
Adequacy Issues in Reactive Systems: Barbed Semantics for Mobile Ambients
Academic discipline
INF/01
Course of study
INFORMATICA
Supervisors
tutor Prof. Gadducci, Fabio
Keywords
  • barbed semantics
  • graphical encodings
  • mobile ambients
  • reactive systems
Graduation session start date
21/06/2011
Availability
Full
Summary
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.
File