Computer Science ›› 2014, Vol. 41 ›› Issue (11): 99-102,106.doi: 10.11896/j.issn.1002-137X.2014.11.019

Previous Articles     Next Articles

Axiomatizing Weak Covariant-contravariant Simulation Semantics

ZHANG Wei   

  • Online:2018-11-14 Published:2018-11-14

Abstract: Process algebra,as one of the important tools for describing and analyzing concurrent and distributed systems,becomes a central branch of research in concurrency theory.Simulation is considered as one of the fundamental notions for describing the refinement relation between processes.Covariant-contravariant simulation generalizes plain simulation and distinguishes the types of actions.Intuitively,it captures the fact that it is not always the case that “the larger the number of behaviors,the better”.But covariant-contravariant simulation ignores the difference between observable actions and silent actions.This paper presented the notion of a weak covariant-contravariant simulation and provided its axiomatic system.The soundness and ground-completeness are established in this system.Furthermore,we proved that such system is also ω-complete.

Key words: Process algebra,Covariant-contravariant simulation,Soundness,Completeness

[1] Baeten J C M,Basten T,Basten T,et al.Process algebra:equational theories of communicating processes[M].Cambridge University Press,2010
[2] Bergstra J A,Klop J W.Process algebra for synchronous communication[J].Information and control,1984,60(1):109-137
[3] Milner R.Communication and concurrency[M].Prentice-Hall,Inc.,1989
[4] Hoare C A R.Communicating sequential processes[J].Communications of the ACM,1978,21(8):666-677
[5] Van Glabbeek R J.The linear time-branching timespectrum I[C]∥The Semantics of Concrete,Sequential Processes.Handbook of Process Algebra.Elsevier,2001:3-99
[6] Aceto L,De Frutos Escrig D,Gregorio-Rodríguez C,et al.Axiomatizing weak simulation semantics over BCCSP[J].Theoretical Computer Science,2014,7:42-71
[7] Fábregas I,De Frutos Escrig D,Palomino M.Logics for contravariant simulations[M]∥Formal Techniques for Distributed Systems.Springer Berlin Heidelberg,2010:224-231
[8] Fábregas I,De Frutos Escrig D,Palomino M.Non-strongly stable orders also define interesting simulation relations[M]∥Algebra and Coalgebra in Computer Science.Springer Berlin Heidelberg,2009:221-235
[9] Fábregas I,Escrig D F,Palomino M.Equational characterization of covariant-contravariant simulationand conformance simulation semantics[C]∥Proceedings Seventh Workshop on Operational Semantics.Paris,France,2010:1-14 (下转第106页)(上接第102页)
[10] Aceto L,Fábregas I,De Frutos Escrig D,et al.Relating modal refinements,covariant-contravariant simulations and partial bisimulations[M]∥Fundamentals of Software Engineering.Springer Berlin Heidelberg,2012:268-283
[11] Hennessy M C B,Milner R.Algebraic laws for nondeterminism and concurrency[J].JACM,1985,32(1):137-161
[12] Glabbeek R J.The linear time-branching time spectrum II[C]∥Proceedings of the 4th International Conference on Concurrency Theory.Springer-Verlag,1993:66-81
[13] De Nicola R,Hennessy M C B.Testing equivalences for proces-ses[J].Theoretical Computer Science,1984,34(1):83-133
[14] Van Glabbeek R J,Weijland W P.Branching time and abstrac-tion in bisimulation semantics[J].JACM,1996,43(3):555-600
[15] Plotkin G.A structural approach to operational semantics[J].Journal of Logic and Algebraic Programming,2004(60):17-139
[16] Chen Tao-lue.Clocks,dice and processes[D].Dutch:Universiteit van Amsterdam,2009
[17] 王精明,虞慧群.基于安全进程代数的非演绎安全模型的分析与验证[J].计算机科学,2012,9(2):56-58

No related articles found!
Full text



[1] LEI Li-hui and WANG Jing. Parallelization of LTL Model Checking Based on Possibility Measure[J]. Computer Science, 2018, 45(4): 71 -75, 88 .
[2] XIA Qing-xun and ZHUANG Yi. Remote Attestation Mechanism Based on Locality Principle[J]. Computer Science, 2018, 45(4): 148 -151, 162 .
[3] LI Bai-shen, LI Ling-zhi, SUN Yong and ZHU Yan-qin. Intranet Defense Algorithm Based on Pseudo Boosting Decision Tree[J]. Computer Science, 2018, 45(4): 157 -162 .
[4] WANG Huan, ZHANG Yun-feng and ZHANG Yan. Rapid Decision Method for Repairing Sequence Based on CFDs[J]. Computer Science, 2018, 45(3): 311 -316 .
[5] SUN Qi, JIN Yan, HE Kun and XU Ling-xuan. Hybrid Evolutionary Algorithm for Solving Mixed Capacitated General Routing Problem[J]. Computer Science, 2018, 45(4): 76 -82 .
[6] ZHANG Jia-nan and XIAO Ming-yu. Approximation Algorithm for Weighted Mixed Domination Problem[J]. Computer Science, 2018, 45(4): 83 -88 .
[7] WU Jian-hui, HUANG Zhong-xiang, LI Wu, WU Jian-hui, PENG Xin and ZHANG Sheng. Robustness Optimization of Sequence Decision in Urban Road Construction[J]. Computer Science, 2018, 45(4): 89 -93 .
[8] LIU Qin. Study on Data Quality Based on Constraint in Computer Forensics[J]. Computer Science, 2018, 45(4): 169 -172 .
[9] ZHONG Fei and YANG Bin. License Plate Detection Based on Principal Component Analysis Network[J]. Computer Science, 2018, 45(3): 268 -273 .
[10] SHI Wen-jun, WU Ji-gang and LUO Yu-chun. Fast and Efficient Scheduling Algorithms for Mobile Cloud Offloading[J]. Computer Science, 2018, 45(4): 94 -99, 116 .