One of the most studied behavioural equivalences is bisimilarity. Its success is much due to the associated bisimulation proof method, which can be further enhanced by means of "bisimulation up-to" techniques such as "up-to context." A different proof method is discussed, based on a unique solution of special forms of inequations called contractions and inspired by Milner's theorem on unique solution of equations. The method is as powerful as the bisimulation proof method and its "up-to context" enhancements. The definition of contraction can be transferred onto other behavioural equivalences, possibly contextual and non-coinductive. This enables a coinductive reasoning style on such equivalences, either by applying the method based on unique solution of contractions or by injecting appropriate contraction preorders into the bisimulation game. The techniques are illustrated in CCS-like languages; an example dealing with higher-order languages is also shown.

Equations, contractions, and unique solutions

Sangiorgi, Davide
2017

Abstract

One of the most studied behavioural equivalences is bisimilarity. Its success is much due to the associated bisimulation proof method, which can be further enhanced by means of "bisimulation up-to" techniques such as "up-to context." A different proof method is discussed, based on a unique solution of special forms of inequations called contractions and inspired by Milner's theorem on unique solution of equations. The method is as powerful as the bisimulation proof method and its "up-to context" enhancements. The definition of contraction can be transferred onto other behavioural equivalences, possibly contextual and non-coinductive. This enables a coinductive reasoning style on such equivalences, either by applying the method based on unique solution of contractions or by injecting appropriate contraction preorders into the bisimulation game. The techniques are illustrated in CCS-like languages; an example dealing with higher-order languages is also shown.
File in questo prodotto:
Eventuali allegati, non sono esposti

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/11585/619244
 Attenzione

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

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