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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.