A calculus for costed computations

We develop a version of the picalculus Picost where channels are interpreted as resources which have costs associated with them. Code runs under the financial responsibility of owners; they must pay to use resources, but may profit by providing them. We provide a proof methodology for processes described in Picost based on bisimulations. The underlying behavioural theory is justified via a contextual characterisation. We also demonstrate its usefulness via examples.

• Type: Journal
• Year: 2010
• Where: CORR
• Authors: Matthew Hennessy
• Keywords: CORR 2010, Education, Financial Responsibility, Picalculus Picost, Proof Methodology