Computer Science ›› 2014, Vol. 41 ›› Issue (11): 99-102.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!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!