Foundations of Process Calculi and Contextual Systems

点击翻译按钮获取中文摘要

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.