Foundations of Process Calculi and Contextual Systems

进程演算是理想化的语言，旨在对与并发和移动性相关的各种基本问题进行建模，包括并发、不确定性和代理的移动性，包括逻辑和物理的。不幸的是，这种演算的语义非常复杂且高度专业化。由此产生的对关于这类系统的推理的证明方法的局部优化意味着到目前为止很难分离出健壮的概念和技术。建议建立一个理论框架，承诺在广泛的过程语言和模型上提供对操作语义和证明技术的统一理解，这些过程语言和模型旨在捕捉并发和移动计算的各种现象，以及用于分子和系统生物学现象研究的新兴过程语言和图形模型。该框架将用范畴理论的语言来表达，强调概括性和数学优雅。它应该通过扩展现有的反应系统理论来发展，反应系统理论对进程演算和一般计算形式的两个重要特征进行了建模：上下文和归约。该理论允许推导行为良好的标记转换系统，从而允许使用协归纳证明技术来推理上下文等价性。通过扩展理论，我们将能够涵盖在GUC中出现的更多重要的例子，并分离出关于其组件的推理的健壮证明技术。

Process calculi are idealised languages which aim to model various foundational issues associated with concurrency and mobility, including concurrency, nondeterminism and mobility of agents, both logical and physical. Unfortunately, the semantics of such calculi are very complicated and highly specialised. The resulting local optimisation on the proof methods for reasoning about such systems has meant that it has so far been difficult to isolate robust concepts and techniques. It is proposed to develop a theoretical framework which promises to provide a uniform understanding of operational semantics and proof techniques across a wide range of process languages and models which aim to capture various phenomena of concurrent and mobile computation, as well as emerging process languages and graphical models for the study of phenomena from molecular and systems biology. The framework is to be expressed in the language of category theory, with emphasis placed on generality and mathematical elegance. It shall be developed by extending the existing theory of reactive systems, which model two important features of process calculi and computational formalisms in general: context and reduction. The theory allows the derivation of well-behaved labelled transition systems, which allow coinductive proof techniques for reasoning about contextual equivalence. By extending the theory, we shall be able to cover more significant examples which arise in GUC and isolate robust proof techniques for reasoning about its components.