【摘 要】
：
进程演算是刻画并发与交互式反应系统行为的原型规范语言,它们通过进程项来描述反应式系统的规范及实现,实现是否满足规范则由行为等价或者精化关系来刻画。经典的模拟(simulation)关系主要是针对反应式系统间的精化关系的刻画,这类系统只具有被动的行为。对于具有主动行为的系统,经典的模拟关系将不再适用。为此,学术界将模拟和互模拟(bisimulation)概念推广,提出共变-异变模拟(Covarian
论文部分内容阅读
进程演算是刻画并发与交互式反应系统行为的原型规范语言,它们通过进程项来描述反应式系统的规范及实现,实现是否满足规范则由行为等价或者精化关系来刻画。经典的模拟(simulation)关系主要是针对反应式系统间的精化关系的刻画,这类系统只具有被动的行为。对于具有主动行为的系统,经典的模拟关系将不再适用。为此,学术界将模拟和互模拟(bisimulation)概念推广,提出共变-异变模拟(Covariant-Contravariant simulation,CC-模拟)的概念,它通过区分动作类型,刻画了规范与实现对系统主动、被动和通讯动作在精化关系中的不同要求。由于行为关系相对演算系统中算子的(前)同余性((pre)congruence)是对规范进行模块化构造、分析及推理的根本基础,建立行为关系的(前)同余性是进程演算研究的重要内容之一。除此之外,行为关系的(不)等式公理的刻画是进程演算代数特性的集中体现,它为进程间的等价(或精化)关系的机器定理证明奠定了不可或缺的理论基础。行为关系(前)同余性的证明以及公理刻画均依赖于演算系统中算子的结构化操作语义(structural operational semantics,SOS)规则。为了避免研究工作中的重复劳动,学术界针对SOS元理论开展了研究,希望基于规范进程算子操作语义的SOS规则形式,给出同余性证明及公理化构造的普适性结论及方法。本文将基于被广泛使用的GSOS和ntyft/ntyxt规则形式针对CC-模拟的前同余性和公理系统进行研究,主要工作如下:1.基于GSOS规则形式探讨了确保CC-模拟具有前同余性的充分条件,提出CC-GSOS规则形式,证明了CC-GSOS算子下CC-模拟的前同余性,并通过例证说明CC-GSOS中的约束条件的必要性。在此基础上,进一步研究了更一般化的ntyft/ntyxt规则形式下CC-模拟相对算子的前同余性,提出CC-ntyft/ntyxt规则形式,并证明了CC-ntyft/ntyxt算子下CC-模拟的前同余性。2.在上述工作及Aceto等人的工作基础上,基于CC-GSOS规则定义的转换系统规范(transition system specifications),提出CC-模拟公理系统构造的一般性方法,该方法为CC-GSOS系统上的CC-模拟的公理化提供了快捷的途径,并证明了由此构建的公理系统相对CC-GSOS算子的可靠性与基完备性。3.对CC-ntyft/ntyxt算子下的互模拟公理系统和CC-模拟公理系统之间的联系开展了研究,证明了在互模拟可靠且完备的公理系统中加入S_p~r和S_p~l两条公理后得到的公理系统对CC-模拟也是可靠且完备的。
其他文献
近年来,无线通信技术的成熟与物联网技术的普及使人们的生活方式向着智能化方向转变,对室内环境下的智能感知需求日益增长。其中,入侵检测和室内定位技术更是人们的重点关注对象。而随着WIFI信号在全球范围内的广泛部署,利用WIFI实现入侵检测与室内定位可以适用于很多场所。不同于传统的WIFI接收信号强度(RSSI,Received Signal Strength Indication),本文选择能更细致刻
反导系统自诞生之初,便深刻影响着世界的战略平衡与稳定。冷战时期,美苏为夺取战略优势,进行了激烈的反导战略博弈。后两国认识到反导系统对核威慑平衡的破坏作用,展开了反导谈判,并签订了《反导条约》。这在很长一段时间内确保了世界的战略稳定与平衡。近年来,反导技术日新月异,反导系统的性能也发生了变化,具备了攻防兼备的特性。随着反导系统的扩散,反导部署趋向常态化,反导格局也日趋多极化,反导军备竞赛正在蔓延。反
新时代习近平同志基于马克思主义反腐败思想,作出反腐败重要论述,是基于中国具体实际情况的、具备中国特色的反腐败思想,构成习近平新时代中国特色社会主义思想中不可缺少的
口语教学是对外汉语教学的重要组成部分之一,很大程度上影响了汉语学习者的口头交际能力。教学设计是对外汉语教学中一个重要的环节,进行教学设计的目的是能在教学实践前对学习过程和学习资源有一个系统科学的安排。笔者担任泰国东北部乌隆他尼府的Don Bosco Vitthaya School汉语教师长达两年,并负责初中学生汉语口语课的教学工作。本文主要研究泰国初中生中级汉语口语课的教学,根据对外汉语教学理论,
谐振型无线无源声表面波(Surface Acoustic Wave,SAW)传感器通过谐振回波信号频率的提取能实现远距离无线无源参数的测量,并且该传感器能用于高温、低温、高电压、高加速度、强腐蚀性、强电磁场等复杂环境。这些优点的存在,使得SAW无线测量技术备受关注。随着SAW无线测量技术的发展,出现了很多难以解决的问题,主要有:(1)无源SAW传感器回波信号能量低,有效信号持续时间短,且工作环境复
本设计的核心为电源与驱动的整合设计,其最大的优点是提高了电源的效率,本技术实现了很多的创新,如:超薄设计,低待机功耗,节能环保等,技术上的优势为其推广应用奠定了基础。
随着各种数据采集手段的增多,真实数据往往呈现多模态或来自多个异构源,形成了多视图数据。而以此数据为研究对象进行机器学习任务称为多视图学习。由于样本标记的费时费力,多视图聚类,作为多视图学习中的重要范式受到了研究者的广泛关注。至今,大多数多视图聚类方法都是基于视图完整的假设。然而,在现实生活中,每个视图数据都有可能产生样本的缺失,这样的缺失使得常规的多视图聚类算法不能直接使用。对这样的数据进行聚类称
随着互联网和数据科学的快速发展,电子信息数据在云计算、互联网中的应用处理需求日益增大,且还需防范数据中可能夹杂的如越权存取、计算机病毒和网络攻击等危害风险,以降低计算机网络系统的安全隐患。这些夹杂危害极大地影响着人们的使用体验和个人隐私数据安全,并随着应用的不断增长网络攻击事件也层出不穷,严重威胁着整个互联网环境的网络空间安全。通过对以往重大网络攻击事件经验教训的总结归纳,可以提取攻击风险给防御作
大数据时代下,从海量数据集中选取用户感兴趣的精简结果集返回给用户是当代数据库系统进行多决策准则的重要功能之一。k-遗憾方法将最大遗憾率作为衡量标准,输出遗憾率最小的k个点作为整个数据库的代表点。但是现有k-遗憾方法以Skyline集合作为算法的候选集,算法耗时较多,并且不能很好地适应维度的变化。因此论文致力于寻找比Skyline集合更小的候选集从而提高k-遗憾查询算法的效率。论文的主要工作和创新点
本文运用社会学的调查研究方法,以国内艺术治疗从业者为研究对象,试图借他们之眼,更清晰的认识我国艺术治疗行业的发展状况。具体研究过程包括了问卷调查与深度访谈,通过对问卷结果的统计描述和对访谈结果的建构主义写作呈现出我国艺术治疗从业者视角下的行业真实而丰富的图景。结论概括如下:1.艺术治疗从业者以各类心理健康工作者的角色,或在学校、医院、企业等组织单位中,或以独立工作室的形式,服务于成年人、特殊群体等