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.
Corradini F., Gorrieri R., Roccetti M. (1997). Performance preorder and competitive equivalence. ACTA INFORMATICA, 34(11), 805-831 [10.1007/s002360050107].
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
