Abstract interpretation can be used to formalize the concept of parametricity in the concurrency field. The concrete domain is the proved transition system, whose transitions are labelled by encodings of the parallel structure of processes. Suitable relabelling functions of proved transitions allow us to retrieve many non interleaving models presented in the literature. We prove here that such relabelling functions are indeed abstraction functions in the sense of abstract interpretations, considering causality as a test-bed. They induce Galois connections between the concrete domain and the abstract semantic models. We prove that abstractions preserve non interleaving bisimulations.

True Concurrency via Abstract Interpretation

BODEI, CHIARA;PRIAMI CORRADO
1997-01-01

Abstract

Abstract interpretation can be used to formalize the concept of parametricity in the concurrency field. The concrete domain is the proved transition system, whose transitions are labelled by encodings of the parallel structure of processes. Suitable relabelling functions of proved transitions allow us to retrieve many non interleaving models presented in the literature. We prove here that such relabelling functions are indeed abstraction functions in the sense of abstract interpretations, considering causality as a test-bed. They induce Galois connections between the concrete domain and the abstract semantic models. We prove that abstractions preserve non interleaving bisimulations.
1997
9783540634683
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/53837
 Attenzione

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

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