The theory of processes with durational actions proposed in [8] is equipped here with a preorder based on execution speed, called performance preorder. Two processes P and Q are related if they are strong bisimilar (i.e., functional equivalent) and the first one is at least as fast as the second one. 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. This is an immediate consequence of the proof that the location preorder, which is based on a measure of distribution, implies the performance preorder.
Performance preorder: Ordering processes with respect to speed
Gorrieri R.;Roccetti M.
1995
Abstract
The theory of processes with durational actions proposed in [8] is equipped here with a preorder based on execution speed, called performance preorder. Two processes P and Q are related if they are strong bisimilar (i.e., functional equivalent) and the first one is at least as fast as the second one. 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. This is an immediate consequence of the proof that the location preorder, which is based on a measure of distribution, implies the performance preorder.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
