Research On Observable Covariant-contravariant Simulation And Its Axiomatic System

A core ingredient in process algebra is a notion of behavioural equivalence or refinement relationover process terms. Since traditional behavioural equivalence or refinement relation takes no accountof types of actions, they don’t work well in the situation involving input or output actions. Recently,Fábregas, et al., present the notion of a covariant-contravariant simulation based on classification ofactions. Such notion doesn’t distinguish internal actions from observable actions. This paper intendsto consider some weak versions of covariant-contravariant simulation. Our main work includes thefollowing:（1）A notion of weak covariant-contravariant simulation and its modal logical characterizationare given.（2）We study the notion of observable covariant-contravariant simulation which is the largestprecongruence included in the weak covariant-contravariant simulation. In the framework of EBCCSP,a sound and ground-complete axiomatic systemAX ccfor it is given.（3）In the framework of BCCSP, it is shown that, if the set of bivariant actions is infinite, thenthe axiomatic system AX1BCCSP and AX2BCCSPare complete modulo strongcovariant-contravariant simulation and observable covariant-contravariant simulation, respectively,and hence they are also strongly complete.