Tech Report: HPL-2004-170R1: A Calculus and Logic

Pym, David ; Tofts, Chris

HP Development Company

关键词: logic;    concurrency;    resources;    processes;    modelling;    parallel;   

RP-ID  :  HPL-2004-170R1

学科分类：计算机科学（综合）

美国|英语

来源: HP Labs

【 摘 要 】

Recent advances in logics for reasoning about resources provide a new approach to compositional reasoning in interacting systems. We present a calculus of resources and processes, based on a development of Milner's synchronous calculus of communication systems, SCCS, that uses an explicit model of resource. Our calculus models the co- evolution of resources and processes with synchronization constrained by the availability of resources. We provide a logical characterization, analogous to Hennessy-Milner logic's characterization of bisimulation in CCS, of bisimulation between resource processes which is compositional in the concurrent and local structure of systems. Notes: David Pym visiting from University of Bath 28 Pages