A calculus and logic of bunched resources and processes

详细信息    查看全文

• 作者：Gabrielle Anderson ^{gabrielle.anderson@ucl.ac.uk" class="auth_mail" title="E-mail the corresponding author} ; David Pym ; ^{d.pym@ucl.ac.uk" class="auth_mail" title="E-mail the corresponding author}
• 关键词：Modal logic ; Process algebra ; Bunched logic ; Resource semantics
• 刊名：Theoretical Computer Science
• 出版年：2016
• 出版时间：8 February 2016
• 年：2016
• 卷：614
• 期：Complete
• 页码：63-96
• 全文大小：857 K

文摘

Mathematical modelling and simulation modelling are fundamental tools of engineering, science, and social sciences such as economics, and provide decision-support tools in management. Mathematical models are essentially deployed at all scales, all levels of complexity, and all levels of abstraction. Models are often required to be executable, as a simulation, on a computer. We present some contributions to the process-theoretic and logical foundations of discrete-event modelling with resources and processes. Building on previous work in resource semantics, process calculus, and modal logic, we describe a process calculus with an explicit representation of resources in which processes and resources co-evolve. The calculus is closely connected to a substructural modal logic that may be used as a specification language for properties of models. In contrast to earlier work, we formulate the resource semantics, and its relationship with process calculus, in such a way that we obtain soundness and completeness of bisimulation with respect to logical equivalence for the naturally full range of logical connectives and modalities. We give a range of examples of the use of the process combinators and logical structure to describe system structure and behaviour.