A preorder based on execution speed, called performance preorder, is introduced for a simple process algebra with durational actions. Two processes E and F are related -E (Square image of or equal to)p F-if they have the same functionality (in this case, we have chosen strong bisimulation equivalence) and E is at least as fast as F. Hence, this preorder supports the stepwise refinement "from specification to implementation" by increasing efficiency while retaining the same functionality. We show that the problem of finding faster implementations for a specification is connected to the problem of finding more distributed implementations of the same specification. Both performance preorder and the induced equivalence, called competitive equivalence, are provided with sound and complete axiomatizations for finite agents.

Performance preorder and competitive equivalence

Gorrieri R.;Roccetti M.
1997

Abstract

A preorder based on execution speed, called performance preorder, is introduced for a simple process algebra with durational actions. Two processes E and F are related -E (Square image of or equal to)p F-if they have the same functionality (in this case, we have chosen strong bisimulation equivalence) and E is at least as fast as F. Hence, this preorder supports the stepwise refinement "from specification to implementation" by increasing efficiency while retaining the same functionality. We show that the problem of finding faster implementations for a specification is connected to the problem of finding more distributed implementations of the same specification. Both performance preorder and the induced equivalence, called competitive equivalence, are provided with sound and complete axiomatizations for finite agents.
1997
Corradini F.; Gorrieri R.; Roccetti M.
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/895097
 Attenzione

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

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