计算机科学 ›› 2020, Vol. 47 ›› Issue (1): 51-58.doi: 10.11896/jsjkx.181102026
李苏婷1,张严2
LI Su-ting1,ZHANG Yan2
摘要: 进程的行为理论是进程演算研究的核心内容之一,其侧重于讨论进程间的行为等价和模拟关系。共变-异变模拟(Covariant-Contravariant Simulation,CC-模拟)的概念是对经典(互)模拟概念的推广,它通过区分动作类型,刻画了规范与实现对系统主动、被动和通讯动作在精化关系中的不同要求。行为关系的(前)同余性和公理刻画是进程演算代数特征的集中体现,它们对规范及实现的分析和推理至关重要。一般而言,行为关系(前)同余性的证明和公理系统的构造需要基于不同进程演算系统的结构化操作语义(Structural Operational Semantics,SOS)分别展开。为了避免这类研究工作中的重复劳动,学术界针对一般化SOS规则形式的元理论开展了研究,GSOS是其中被广泛研究的规则形式之一。文中在考量了动作类型的基础上,基于CC-模拟对GSOS规则形式做出扩充,提出了CC-GSOS规则类型,证明了CC-模拟相对于CC-GSOS算子具有前同余性,并给出了在这些算子下CC-模拟的可靠完备公理系统的一般性构造方法。
中图分类号:
[1]MILNER R.Communication and concurrency[M].Prentice-Hall International,Englewood Cliffs,1989. [2]HOARE C A R.Communicating sequential processes[J].Communications of the Acm,1978,21(21):666-677. [3]AUSTRY D,BOUDOL G.Algèbre de processus et synchronisation[J].Theoretical Computer Science,1984,30(1):91-131. [4]FÁBREGAS I,FRUTOS-ESCRIG D,PALOMINO M.Equa- tional Characterization of Covariant-Contravariant Simulation and Conformance Simulation Semantics[C]∥The Workshop on Structural Operational Semantics.2010:1-14. [5]ESCRIG F,DAVID D,RODRÍGUEZ,et al.Ready to preorder:an algebraic and general proof[J].Journal of Logic & Algebraic Programming,2009,78(7):539-551. [6]GROOTE J F,VAANDRAGER F.Structured operational se- mantics and bisimulation as a congruence[J].Information & Computation,1992,100(2):202-260. [7]BLOOM B,ISTRAIL S,MEYER A R.Bisimulation Can’t be Traced:Preliminary Report[C]∥ACM Symposium on Principales of Programming Languages.ACM,1987:229-239. [8]ACETO L,BLOOM B,VAANDRAGER F.Turning SOS rules into equations[C]∥Proceedings of the Seventh IEEESympo-sium on Logic in Computer Science,1992(LICS’92).IEEE,1994:113-124. [9]D’ARGENIO P R,GEBLER D,LEE M D.Axiomatizing Bisimulation Equivalences and Metrics from Probabilistic SOS Rules[C]∥International Conference on Foundations of Software Science and Computation Structures.2014:289-303. [10]KLIN B,SASSONE V.Structural operational semantics for stochastic and weighted transition systems[J].Information & Computation,2013,227(2):58-83. [11]BONCHI F,VAN BUSSEL T,LEE M D,et al.Bisimilarity of open terms in stream GSOS[M]∥Fundamentals of Software Engineering.Cham:Springer,2019:35-50. [12]KLIN B.Bialgebras for structural operational semantics:An introduction[J].Theoretical Computer Science,2011,412(38):5043-5069. [13]ACETO L,FÁBREGAS I,GREGORIO-RODRÍGUEZ C,et al.Logical Characterisations and Compositionality of Input-Output Conformance Simulation[M]∥SOFSEM 2017:Theory and Practice of Computer Science.Cham:Springer,2017:37-48. [14]ROT J.Distributive Laws for Monotone Specifications[C]∥ Combined Workshop on Expressiveness in Concurrency and Structural Operational Semantics (EXPRESS/SOS 2017).EPTCS,2017:83-97. [15]GLABBEEK V R J.The Linear Time-Branching Time Spectrum I-The Semantics of Concrete,Sequential Processes[M]∥Handbook of Process Algebra.Elsevier,2001:3-99. [16]LYNCH N.I/O automata:A model for discrete event systems[C]∥Annual Conference on Information Sciences and Systems.Princeton,N J,1988:29-38. [17]FÁBREGAS I,ESCRIG D D F,PALOMINO M.Logics for Contravariant Simulations[M]∥Formal Techniques for Distributed Systems.Berlin:Springer,2010:224-231. [18]FÁBREGAS I,ESCRIG D D F,PALOMINO M.Non-strongly Stable Orders Also Define Interesting Simulation Relations[C]∥International Conference on Algebra and Coalgebra in Computer Science.Springer-Verlag,2009:221-235. [19]KELLER R M.Formal verification of parallel programs[J]. Comm Acm,1976,19(7):371-384. [20]BAETEN J C M,WEIJLAND W P.Process algebra[M].Cambridge:Cambridge University Press,1990. |
[1] | 王鑫, 周泽宝, 余芸, 陈禹旭, 任昊文, 蒋一波, 孙凌云. 一种面向电能量数据的联邦学习可靠性激励机制 Reliable Incentive Mechanism for Federated Learning of Electric Metering Data 计算机科学, 2022, 49(3): 31-38. https://doi.org/10.11896/jsjkx.210700195 |
[2] | 房婷, 宫傲宇, 张帆, 林艳, 贾林琼, 张一晋. 一种传输时限下认知无线电网络的动态广播策略 Dynamic Broadcasting Strategy in Cognitive Radio Networks Under Delivery Deadline 计算机科学, 2021, 48(7): 340-346. https://doi.org/10.11896/jsjkx.200900001 |
[3] | 亓慧, 史颖, 李灯熬, 穆晓芳, 侯明星. 基于连续型深度置信神经网络的软件可靠性预测 Software Reliability Prediction Based on Continuous Deep Confidence Neural Network 计算机科学, 2021, 48(5): 86-90. https://doi.org/10.11896/jsjkx.210200055 |
[4] | 冯凯, 马鑫玉. (n,k)-冒泡排序网络的子网络可靠性 Subnetwork Reliability of (n,k)-bubble-sort Networks 计算机科学, 2021, 48(4): 43-48. https://doi.org/10.11896/jsjkx.201100139 |
[5] | 冯凯, 李婧. k元n方体的子网络可靠性研究 Study on Subnetwork Reliability of k-ary n-cubes 计算机科学, 2020, 47(7): 31-36. https://doi.org/10.11896/jsjkx.190700170 |
[6] | 王慧妍, 徐经纬, 许畅. 环境感知自适应软件的运行时输入验证技术综述 Survey on Runtime Input Validation for Context-aware Adaptive Software 计算机科学, 2020, 47(6): 1-7. https://doi.org/10.11896/jsjkx.200400081 |
[7] | 程煜, 刘伟, 孙童心, 魏志刚, 杜薇. 近阈值电压下可容错的一级缓存结构设计 Design of Fault-tolerant L1 Cache Architecture at Near-threshold Voltage 计算机科学, 2020, 47(4): 42-49. https://doi.org/10.11896/jsjkx.190300088 |
[8] | 王洪, 官礼和. 顶点序下图的支配集算法 Dominating Set Algorithm for Graphs Based on Vertex Order 计算机科学, 2020, 47(11A): 444-448. https://doi.org/10.11896/jsjkx.200300023 |
[9] | 李蜜, 庄毅, 胡镡文. 一种结合AADL与Z的嵌入式软件可靠性建模与评估方法 Embedded Software Reliability Model and Evaluation Method Combining AADL and Z 计算机科学, 2019, 46(8): 217-223. https://doi.org/10.11896/j.issn.1002-137X.2019.08.036 |
[10] | 弋泽龙,温玉梅,林燕敏,陈伟庭,吕冠宇. 多层缺陷关联效应对软件可靠性增长过程的影响 Impacts of Correlation Effects among Multi-layer Faults on Software Reliability Growth Processes 计算机科学, 2018, 45(2): 241-248. https://doi.org/10.11896/j.issn.1002-137X.2018.02.042 |
[11] | 吴文华, 宋亚飞, 刘晶. 直觉模糊框架内的证据动态可靠性评估及应用 Dynamic Reliability Evaluation Method of Evidence Based on Intuitionistic Fuzzy Sets and Its Applications 计算机科学, 2018, 45(12): 160-165. https://doi.org/10.11896/j.issn.1002-137X.2018.12.025 |
[12] | 刘凯, 梁欣, 张俊萍. 基于软硬系统综合方法的软件失效问题分析 Analysis on Technical Support Equipments’ Software Invalidation Based on Soft and Hard Integrated System Methodology 计算机科学, 2018, 45(11A): 494-496. |
[13] | 赵冉, 潘根梅. 能量捕获无线传感器网络中高可靠数据收集策略 High Reliable Data Collection Algorithm in Energy Harvesting Wireless Sensor Networks 计算机科学, 2018, 45(11A): 303-307. |
[14] | 李灵俐, 白光伟, 沈航, 王天荆. 基于簇的认知多媒体传感器网络实时路由协议 Cluster-based Real-time Routing Protocol for Cognitive Multimedia Sensor Networks 计算机科学, 2018, 45(10): 83-88. https://doi.org/10.11896/j.issn.1002-137X.2018.10.016 |
[15] | 欧阳城添,陈莉莉,王曦. 高层次时序电路可靠度估计方法研究进展 Survey on Reliability Estimation Methods of Sequential Circuit in Height-level 计算机科学, 2017, 44(Z11): 33-38. https://doi.org/10.11896/j.issn.1002-137X.2017.11A.006 |
|