logo SBA

ETD

Archivio digitale delle tesi discusse presso l’Università di Pisa

Tesi etd-05282011-172623


Tipo di tesi
Tesi di dottorato di ricerca
Autore
MONREALE, GIACOMA
URN
etd-05282011-172623
Titolo
Adequacy Issues in Reactive Systems: Barbed Semantics for Mobile Ambients
Settore scientifico disciplinare
INF/01
Corso di studi
INFORMATICA
Relatori
tutor Prof. Gadducci, Fabio
Parole chiave
  • barbed semantics
  • graphical encodings
  • mobile ambients
  • reactive systems
Data inizio appello
21/06/2011
Consultabilità
Completa
Riassunto
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