Abstract
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.
| Original language | English |
|---|---|
| Pages (from-to) | 495-517 |
| Number of pages | 23 |
| Journal | Formal Aspects of Computing |
| Volume | 18 |
| Issue number | 4 |
| Publication status | Published - 2006 |