Counting the cost in the picalculus.

PUBLISHED Reykjavik, Iceland We design a new variation on the picalculus, ?cost, in which the use of channels or resources must be paid for. Processes operate relative to a cost environment, and communications can only happen if principals have provided sufficient funds for the channels associated w...

Full description

Bibliographic Details
Published in:Electronic Notes in Theoretical Computer Science
Main Author: HENNESSY, MATTHEW
Format: Conference Object
Language:English
Published: Elsevier Science Publishers B. V 2009
Subjects:
Online Access:http://hdl.handle.net/2262/53335
http://people.tcd.ie/mcbhenne
https://doi.org/10.1016/j.entcs.2009.06.042
Description
Summary:PUBLISHED Reykjavik, Iceland We design a new variation on the picalculus, ?cost, in which the use of channels or resources must be paid for. Processes operate relative to a cost environment, and communications can only happen if principals have provided sufficient funds for the channels associated with the communications. We define a bisimulation-based behavioural preorder in which two processes are related if, intuitively, they exhibit the same behaviour but one may be more efficient than the other. We justify our choice of preorder by proving that it is characterised by three intuitive properties which behavioural preorders should satisfy in a framework in which the use of resources must be funded. This work is a part of the doctoral studies of the second author and is supported by Commonwealth Scholarship Commission UK (Ref: INCS-2005-145). The support of SFI, Ireland is also acknowledged.