The semantics of process calculi has traditionally been specified by labelled transition systems (LTSS), but, with the development of name calculi, it turned Out that reaction rules (i.e., Unlabelled transition rules) are often more natural. This leads to the question of how behavioral equivalences (bisimilarity, trace equivalence, etc.) defined for US can be transferred to unlabelled transition systems. Recently, in order to answer this question, several proposals have been made with the aim of automatically deriving an LTS from reaction rules in Such a way that the resulting equivalences are congruences. Furthermore, these equivalences should agree with the standard semantics, whenever one exists. In this paper, we propose saturated semantics, based on a weaker notion of observation and orthogonal to all the previous proposals, and we demonstrate the appropriateness of our semantics by means of two examples: logic programming and open Petri nets. We also show that saturated semantics can be efficiently characterized through the so called semi-saturated games. Finally, we provide coalgebraic models relying on presheaves. (C) 2009 Elsevier B.V. All rights reserved.

Reactive systems, (semi-)saturated semantics and coalgebras on presheaves

Bonchi F;MONTANARI, UGO GIOVANNI ERASMO
2009

Abstract

The semantics of process calculi has traditionally been specified by labelled transition systems (LTSS), but, with the development of name calculi, it turned Out that reaction rules (i.e., Unlabelled transition rules) are often more natural. This leads to the question of how behavioral equivalences (bisimilarity, trace equivalence, etc.) defined for US can be transferred to unlabelled transition systems. Recently, in order to answer this question, several proposals have been made with the aim of automatically deriving an LTS from reaction rules in Such a way that the resulting equivalences are congruences. Furthermore, these equivalences should agree with the standard semantics, whenever one exists. In this paper, we propose saturated semantics, based on a weaker notion of observation and orthogonal to all the previous proposals, and we demonstrate the appropriateness of our semantics by means of two examples: logic programming and open Petri nets. We also show that saturated semantics can be efficiently characterized through the so called semi-saturated games. Finally, we provide coalgebraic models relying on presheaves. (C) 2009 Elsevier B.V. All rights reserved.
Bonchi, F; Montanari, UGO GIOVANNI ERASMO
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11568/205075
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? 10
social impact