计算机科学 ›› 2020, Vol. 47 ›› Issue (1): 51-58.doi: 10.11896/jsjkx.181102026

• 计算机科学理论 • 上一篇    下一篇

GSOS算子下共变-异变模拟的公理刻画

李苏婷1,张严2   

  1. (南京航空航天大学计算机科学与技术学院 南京211106)1;
    (南京林业大学信息科学技术学院 南京210037)2
  • 收稿日期:2018-11-03 发布日期:2020-01-19
  • 通讯作者: 张严(zhangyan@njfu.edu.cn)
  • 基金资助:
    国家自然科学基金(61602249);江苏省普通高校自然科学研究资助项目(17KJB520012)

Axiomatizing Covariation-Contravariation Simulation Under GSOS Operators

LI Su-ting1,ZHANG Yan2   

  1. (College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China)1;
    (College of Information Science and Technology,Nanjing Forestry University,Nanjing 210037,China)2
  • Received:2018-11-03 Published:2020-01-19
  • About author:LI Su-ting,born in 1994,postgraduate.Her main research interests include process algebra and logics in computer science;ZHANG Yan,born in 1983,Ph.D,lecturer.His main research interests in-clude concurrent theory and formal methods.
  • Supported by:
    This work was supported by the National Natural Science Foundation of China (61602249),Natural Science Foundation of the Jiangsu Higher Education Institutions of China (17KJB520012).

摘要: 进程的行为理论是进程演算研究的核心内容之一,其侧重于讨论进程间的行为等价和模拟关系。共变-异变模拟(Covariant-Contravariant Simulation,CC-模拟)的概念是对经典(互)模拟概念的推广,它通过区分动作类型,刻画了规范与实现对系统主动、被动和通讯动作在精化关系中的不同要求。行为关系的(前)同余性和公理刻画是进程演算代数特征的集中体现,它们对规范及实现的分析和推理至关重要。一般而言,行为关系(前)同余性的证明和公理系统的构造需要基于不同进程演算系统的结构化操作语义(Structural Operational Semantics,SOS)分别展开。为了避免这类研究工作中的重复劳动,学术界针对一般化SOS规则形式的元理论开展了研究,GSOS是其中被广泛研究的规则形式之一。文中在考量了动作类型的基础上,基于CC-模拟对GSOS规则形式做出扩充,提出了CC-GSOS规则类型,证明了CC-模拟相对于CC-GSOS算子具有前同余性,并给出了在这些算子下CC-模拟的可靠完备公理系统的一般性构造方法。

关键词: GSOS, 共变-异变模拟, 结构化操作语义(SOS), 进程演算, 可靠性, 完备性

Abstract: The behavioral theory of processes is one of the core research contents of process calculus,which focuses on discussing behavioral equivalence or simulation relationships between processes.The Covariant-Contravariant simulation (CC-simulation) is the extension of the (bi)simulation,which distinguishes the types of actions and expresses the different requirement of active,passive and communication actions in refinement relationships between specifications and implementations.The (pre)congruence and axiomatization of behavioral relationships are the concentrated expression of the algebraic features of process calculus,which are essential for the analysis and reasoning of specifications and implementations.In general,the proof of behavioral (pre)congruence and the construction of axiomatic systems need to be based on the Structural Operational Semantics (SOS) of different process calculus systems.In order to avoid duplication of labor in these kinds of research work,the academia has carried out research on the meta-theory of the generalized SOS rule formats,and GSOS is one of the format that have been widely studied.Based on the consideration of action types,this paper extends the GSOS rule format for CC-simulation,proposes CC-GSOS rule format,and proves that the CC-simulation is a precongruent relation relative to CC-GSOS operators,gives a general method for constructing axiomatic system for CC-simulation which is sound and complete.

Key words: Completeness, Covariant-contravariant simulation, GSOS, Process calculus, Soundness, Structural operational semantics (SOS)

中图分类号: 

  • TP301
[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
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!