Computer Science ›› 2020, Vol. 47 ›› Issue (1): 51-58.doi: 10.11896/jsjkx.181102026

• Computer Science Theory • Previous Articles     Next Articles

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).

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)

CLC Number: 

  • 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] TAO Xiao-yan, YAN Chun-gang, LIU Guan-jun. Dynamic Data Refining Strategy for Soundness Verification Based on WFT-net [J]. Computer Science, 2021, 48(7): 99-104.
[2] WANG Hong, GUANG Li-he. Dominating Set Algorithm for Graphs Based on Vertex Order [J]. Computer Science, 2020, 47(11A): 444-448.
[3] YANG Yue and ZHANG De-sheng. Technology of Extracting Topical Keyphrases from Chinese Corpora [J]. Computer Science, 2017, 44(Z11): 432-436.
[4] DAI Hua, YE Qing-qun, YANG Geng, XIAO Fu and HE Rui-liang. Overview of Secure Top-k Query Processing in Two-tiered Wireless Sensor Networks [J]. Computer Science, 2017, 44(5): 6-13.
[5] WANG Ting,LIU Ren-ren and MA Ke. Research on Classification of Precomplete Classes in Partial Multiple-valued Logic Function Sets [J]. Computer Science, 2014, 41(8): 60-62.
[6] ZHANG Wei. Axiomatizing Weak Covariant-contravariant Simulation Semantics [J]. Computer Science, 2014, 41(11): 99-102.
[7] HAN Jing-yu and CHEN Ke-jia. Ranking Data Quality of Web Article Content by Extracting Facts [J]. Computer Science, 2014, 41(11): 247-251.
[8] DAI Fei,LI Tong,XIE Zhong-wen,MO Qi and JIN Yun-zhi. Research on Structure Soundness of Software Processes Based on EPMM [J]. Computer Science, 2013, 40(8): 186-190.
[9] . Some Results on the Decision of the Minimal Covering for Full Symmetric Function Sets in Partial K-valued Logic [J]. Computer Science, 2012, 39(5): 205-207.
[10] . Proving NP-completeness of Polynomial Reduction from the SAT Problem to the MSP Problem [J]. Computer Science, 2012, 39(11): 179-182.
[11] . Number of Simply Separable and Full Symmetric Relations in Partial Multiple-valued Logic [J]. Computer Science, 2012, 39(10): 224-226.
[12] CHEN Wei-dong,ZHANG Wei-ming. Data Quality Model and Metrics Research at Attribute Granularity [J]. Computer Science, 2010, 37(5): 139-142.
[13] . [J]. Computer Science, 2008, 35(8): 277-280.
[14] ZHOU Cong-Hua ,LIU Zhi-Feng (School of Computer Science and Telecommunication Engineering, Jiangsu University, Zhenjiang 212013). [J]. Computer Science, 2008, 35(2): 115-119.
[15] LIU Ji (State Key Laboratory for Novel Software Technology, Department of Computer Science and Technology, Nanjing University, Nanjing 210093). [J]. Computer Science, 2007, 34(1): 203-207.
Full text



No Suggested Reading articles found!