CC-模拟相对GSOS/ntyft/ntyxt算子的前同余性及公理刻画

发布时间：2021-08-26 19:46

　　进程演算是刻画并发与交互式反应系统行为的原型规范语言,它们通过进程项来描述反应式系统的规范及实现,实现是否满足规范则由行为等价或者精化关系来刻画。经典的模拟（simulation）关系主要是针对反应式系统间的精化关系的刻画,这类系统只具有被动的行为。对于具有主动行为的系统,经典的模拟关系将不再适用。为此,学术界将模拟和互模拟（bisimulation）概念推广,提出共变-异变模拟（Covariant-Contravariant simulation,CC-模拟）的概念,它通过区分动作类型,刻画了规范与实现对系统主动、被动和通讯动作在精化关系中的不同要求。由于行为关系相对演算系统中算子的（前）同余性（（pre）congruence）是对规范进行模块化构造、分析及推理的根本基础,建立行为关系的（前）同余性是进程演算研究的重要内容之一。除此之外,行为关系的（不）等式公理的刻画是进程演算代数特性的集中体现,它为进程间的等价（或精化）关系的机器定理证明奠定了不可或缺的理论基础。行为关系（前）同余性的证明以及公理刻画均依赖于演算系统中算子的结构化操作语义（structural operationa... 

【文章来源】：南京航空航天大学江苏省 211工程院校

【文章页数】：77 页

【学位级别】：硕士

【部分图文】：

SOS 规则形式间的包含关系

图 2.1 证明树示例图设 S ( Σ,R)是一正 TSS，S 是 S 的相关模型，对任意转且仅当 |S 。理可自然的得出这样一个事实：正 TSS S 的最小模型也是 S

文献[53]将符号S 的含义拓展到表示一个可分层的 TSS S 的相间的关系给出了下图 2.2 的说明，其中 A B表示 A 结构类包含于 B 结个正 TSS S 的 A 和 B 是一致的。

【参考文献】：
硕士论文
[1]可观测共变—逆变模拟及其公理系统的研究[D]. 张威.南京航空航天大学 2014



本文编号：3364856