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 |