Substructural modal logic for optimal resource allocation
Gabrielle Anderson, David J. Pym · 2015
We introduce a substructural modal logic for reasoning about (optimal) resource allocation in models of distributed systems. The underlying logic is a variant of the modal logic of bunched implications, and based on the same resource semantics, which is itself closely related to concurrent separation logic. By considering notions of cost, strategy, and utility, we are able to formulate characterizations of Pareto optimality, best responses, and Nash equilibrium within resource semantics.