CSP-Agda的跟踪和稳定故障语义
Trace and Stable Failures Semantics for CSP-Agda
摘要：
CSP-Agda是一个库，它使用共归纳数据类型在交互式定理证明器Agda中形式化进程代数CSP。在CSP-Agda中，CSP过程是一元形式的，支持过程的模块化开发。本文在CSP-Agda中实现了CSP的两个主要模型：跟踪和稳定故障语义，并定义了相应的精化和等价关系。由于一元设置，需要进行一些调整。作为例子，我们证明了外选择算子w.r.t. CSP-Agda中的跟踪语义，以及对W.R.T.稳定失效语义是一个偏序。所有的证明和定义都在Agda中进行了类型检查。代数定律的进一步证明将在CSP-Agda存储库中提供。
英文摘要：
CSP-Agda is a library, which formalises the process algebra CSP in the interactive theorem prover Agda using coinductive data types. In CSP-Agda, CSP processes are in monadic form, which sup- ports a modular development of processes. In this paper, we implement two main models of CSP, trace and stable failures semantics, in CSP-Agda, and define the corresponding refinement and equal- ity relations. Because of the monadic setting, some adjustments need to be made. As an example, we prove commutativity of the external choice operator w.r.t. the trace semantics in CSP-Agda, and that refinement w.r.t. stable failures semantics is a partial order. All proofs and definitions have been type checked in Agda. Further proofs of algebraic laws will be available in the CSP-Agda repository.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
