A calculus for costed computations

TL;DR

This paper introduces picost, a pi-calculus variant modeling resource costs and ownership, with a bisimulation-based proof methodology and practical examples demonstrating its applicability.

Contribution

It presents a novel calculus for costed computations, incorporating resource costs and ownership, with a formal proof technique and contextual semantics.

Findings

Bisimulation-based proof methodology for picost processes

Formal justification via contextual characterization

Practical examples demonstrating usefulness

Abstract

We develop a version of the pi-calculus, 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.