Equational Characterization of Covariant-Contravariant
Simulation and Conformance Simulation Semantics
Ignacio Fábregas

David de Frutos Escrig

Miguel Palomino

Universidad Complutense de Madrid
Madrid, Spain
Departamento de Sistemas Informáticos y Computación ∗
fabregas@fdi.ucm.es

defrutos@sip.ucm.es

miguelpt@sip.ucm.es

Covariant-contravariant simulation and conformance simulation generalize plain simulation and try
to capture the fact that it is not always the case that “the larger the number of behaviors, the better”.
We have previously studied their logical characterizations and in this paper we present the axiomatizations of the preorders defined by the new simulation relations and their induced equivalences. The
interest of our results lies in the fact that the axiomatizations help us to know the new simulations
better, understanding in particular the role of the contravariant characteristics and their interplay with
the covariant ones; moreover, the axiomatizations provide us with a powerful tool to (algebraically)
prove results of the corresponding semantics. But we also consider our results interesting from a
metatheoretical point of view: the fact that the covariant-contravariant simulation equivalence is indeed ground axiomatizable when there is no action that exhibits both a covariant and a contravariant
behaviour, but becomes non-axiomatizable whenever we have together actions of that kind and either
covariant or contravariant actions, offers us a new subtle example of the narrow border separating axiomatizable and non-axiomatizable semantics. We expect that by studying these examples we will
be able to develop a general theory separating axiomatizable and non-axiomatizable semantics.

1

Introduction and some related work

Simulations are a very natural way to compare systems defined by labeled transition systems or other
related mechanisms based on describing the behavior of states by means of the actions they can execute
[19]. They aim at comparing processes based on the simple premise “you are better if you can do as
much as me, and perhaps some other new things”. This assumes that all the executable actions are
controlled by the user (no difference between input and output actions) and does not take into account
that whenever the system has several possibilities for the execution of an action it will choose in an
unpredictable internal way, so that more possibilities means less control.
In order to cope with these limitations one should consider adequate versions of simulation where
the characteristics of actions and the idea of preferring processes that are less non-deterministic are
taken into account. This leads to two new notions of simulation: covariant-contravariant simulation
and conformance simulation that we roughly sketched in [10] and presented in detail in [12], where we
proved that they can be presented as particular instances of the general notion of categorical simulation
developed by Hughes and Jacobs [14].
Certainly, the distinction between input and output actions or similar classifications is not meant to
be new at all and, for instance, they were present in modal transition systems as early as the end of the
∗ Research

supported by the Spanish projects DESAFIOS10 TIN2009-14599-C03-01, TESIS TIN2009-14321-C02-01 and
PROMETIDOS S2009/TIC-1465. The second author worked in this paper during a visit to Reykjavik University sponsored
through a grant by the ABEL Extraordinary Chair.
L. Aceto, P. Sobociński (Eds.): Seventh Workshop on
Structural Operational Semantics 2010 (SOS ’10)
EPTCS 32, 2010, pp. 1–14, doi:10.4204/EPTCS.32.1

c I. Fábregas, D. de Frutos Escrig & M. Palomino
This work is licensed under the
Creative Commons Attribution License.

2

Equational Characterization of Covariant-Contravariant and Conformance Simulation Semantics

eighties. They also play a central role in I/O-automata [18] and more recently appear as component of
several works on interface automata [7, 15], where one finds the covariant-contravariant distinction when
the guarantees of the specification can only be assumed if the conditions of the specification are satisfied.
Concerning conformance simulation, the first related references are also quite old [17, 21], corresponding to the notion of conformance testing, which is close to failure semantics [4]. However, it is a
bit surprising that in both cases we lack a basic theory where these notions are presented in a simplified
scenario, stressing their main characteristics and properties. We think that the theory of semantics for
processes, and particularly the simulation semantics, is a perfect field in which to develop that basic
theory. This has been already proved in [12], where our new simulation semantics were shown to be
categorical simulations, thus inheriting all their good properties for free.
In [11] we have also briefly presented the logical characterizations of the two semantics. Now that we
already know quite well the behaviour of the two new notions of simulation we can give their algebraic
presentation. By the way, although in our previous works on the unified study of process semantics the
(classical) covariant character of all the actions had several important consequences, mainly represented
by the extremely simple and easy to apply basic axiom for simulation (S) x ⊑ x + y (or equivalently, just
0 ⊑ y), we have been able to borrow from [9, 1, 8] several ideas about the axiomatization of process
semantics that, although not directly applicable due to the special characteristics of the new semantics,
can be adequately adapted.
However, not all of the simple and nice results for the algebraic theory of plain (covariant) simulation
can be extended to the general covariant-contravariant case. In particular, in order to obtain the maximal
genericity, when we defined covariant-contravariant simulations in [12] we admitted not only both covariant and contravariant actions, but also other actions with a bivariant nature. This decision was taken
because when presenting a general theory of categorical simulations in [14], J. Hughes and B. Jacobs
already noticed that bisimulation was a particular (in fact, trivial) example of simulation semantics. It
was also clear that inverse simulation (namely, contravariant simulation) was also another example, and
then we were able to prove that our general covariant-contravariant simulation was another categorical
simulation that smoothly combines bisimulation, plain (covariant) simulation and inverse (contravariant)
simulation.
Obviously, plain bisimulation has a simple axiomatization, as is the case for plain simulation; we will
see in this paper that the preorder defined by our covariant-contravariant simulation can also be finitely
axiomatized. When we considered the induced equivalence, we found indeed a finite axiomatization for
the case in which there are no bivariant actions (actions that can be considered as both input and output)
in our alphabet. The axiomatization and its completeness proof were obtained by adapting the general
techniques in [8, 9] for the covariant case to our more general covariant-contravariant scenario. However,
as soon as a single bivariant action is introduced, and at least one non-bivariant one is also present, then
the equational theory of covariant-contravariant simulation equivalence becomes non-finitely axiomatizable, and in fact the proof of this result is extraordinarily simple.
Even if this is a negative result, we think that it will contribute to enlight the narrow border separating
axiomatizable and non-axiomatizable process theories, which we expect to continue exploring in the
future.
There is a large collection of recent papers where notions close to those studied here are either
developed or applied; a detailed comparison will appear elsewhere. However, we insist on the fact that
we were not able to find a basic study where the main results on process theory had been extended to a
framework containing any contravariant characteristics, although it is true that some small contributions
along this direction can be found in some of these papers. We plan to develop a thorough compilation
of the works on this topic by isolating the places where our foundational study could help to understand

I. Fábregas, D. de Frutos Escrig & M. Palomino

3

the different developments, as well as looking for applications and new enhancements to our theory that
could be of use to relate all the disconnected work on the area. In turn, we hope that this will also provide
us with some intuition to understand those results and produce new formal techniques to obtain proofs
of those, or other interesting results in the area. So, simply to give a hint, a sample of those works would
include [2, 3, 16, 20].

2

Preliminaries

In this section we summarize some definitions and concepts from [6, 12] and introduce the notation we
are going to use.
Let us recall our two new simulation notions:
Definition 1 Given P = (P, A, →P ) and Q = (Q, A, →Q ), two labeled transition systems (LTS) for the
alphabet A, and {Ar , Al , Abi } a partition of this alphabet, a (Ar , Al )-simulation (or just a covariantcontravariant simulation) between them is a relation S ⊆ P × Q such that for every pSq we have:
a

a

a

a

• For all a ∈ Ar ∪ Abi and all p −→ p′ there exists q −→ q′ with p′ Sq′ .
• For all a ∈ Al ∪ Abi , and all q −→ q′ there exists p −→ p′ with p′ Sq′ .
We will write p .CC q if there exists a covariant-contravariant simulation S such that pSq.
This definition combines the requirements of plain simulation, for some of the actions, with those of
plain “anti-simulation”, for some of the remaining actions, imposing both on so-called bivariant actions.
Definition 2 Given P = (P, A, →P ) and Q = (Q, A, →Q ) two labeled transition systems for the alphabet
A, a conformance simulation between them is a relation R ⊆ P × Q such that whenever pRq, then:
a

a

• For all a ∈ A, if p −→, then q −→ (this means, using the usual notation for process algebras, that
I(p) ⊆ I(q)).
a

a

a

• For all a ∈ A such that q −→ q′ and p −→, there exists some p′ with p −→ p′ and p′ Rq′ .
We will write p .CS q if there exists a conformance simulation R such that pRq.
The first clause of the definition guarantees that Q has at least all the behaviors of P, allowing to “improve” a process by extending the set of actions it offers, whereas the second clause establishes that a
process can be “improved” by reducing the nondeterminism in it.
Let us recall that the set BCCSP(A) of basic processes for the alphabet A is defined by the BNFgrammar
p ::= 0 | ap | p + p
where a ∈ A. The operational semantics for BCCSP terms is defined by
a

ap −→ p

a

p −→ p′
a
p + q −→ p′

a

q −→ q′
a
p + q −→ q′

With these operators we can only define finite processes; however, it is well known that these operators
capture the essence of any transition system, which can be defined by a system of equations specifying
the behavior of each state. (The axioms for recursive processes, other interesting extensions including
the communication operators, and possibly some others, are left for future work.)

4

3

Equational Characterization of Covariant-Contravariant and Conformance Simulation Semantics

Axiomatization of the new simulation preorders

In this section we present a finite axiomatization of the two preorders for basic finite processes induced
by our new kinds of simulation.

3.1 Covariant-contravariant semantics
We consider a partition {Ar , Al , Abi } of the alphabet A, with actions that have either a covariant nature,
or contravariant, or both at the same time. Contravariant simulation .−1
S is just the inverse of plain
simulation and therefore can be trivially axiomatized by inverting the axiom for plain simulation
(S) x ⊑ x + y,
thus obtaining
(S−1 )

x + y ⊑ x.

In order to produce an axiomatization of covariant-contravariant simulation we need to combine in
an adequate way these two axioms, by constraining each of them to the case in which the added process
y only offers actions with the corresponding covariant or contravariant character. Hence we obtain:
(Sr ) I(y) ⊆ Ar =⇒ x ⊑ x + y.
(S−1,l )

I(y) ⊆ Al =⇒ x + y ⊑ x.

We can omit the conditions in these two axioms by considering two generic actions ar ∈ Ar and al ∈ Al :
(Srp ) x ⊑ x + ar y.
(Slp ) x + al y ⊑ x.
Note that actions in Abi do not appear in the axioms above, although they could be included in the
processes instantiating the variables x and y. This is an immediate consequence of the fact that their
behavior corresponds to that governed by bisimulation, so that we need not add any new axiom to those
capturing the bisimilarity relation:
(B1 ) x + y = y + x.
(B2 ) (x + y) + z = x + (y + z).
(B3 ) x + x = x.
(B4 ) x + 0 = x.
We will use these axioms implicitly in the remainder of this paper.
Proposition 1 The (Ar , Al )-simulation preorder can be axiomatically defined by means of the set of
axioms {B1 , B2 , B3 , B4 , Srp , Slp }.
Proof. First we prove that the axioms (Srp ) and (Slp ) are sound for the (Ar , Al )-similarity relation .CC .
Indeed:
a

a

• For all a ∈ Ar ∪ Abi, if x −→ x′ then x + ar y −→ x′ and x′ .CC x′ .
a

a

a

a

• For all a ∈ Al ∪ Abi , if x + ar y −→ x′ , then x −→ x′ and x′ .CC x′ . Note that a 6= ar since Ar ∩ (Al ∪
Abi ) = 0.
/
• For all a ∈ Ar ∪ Abi, if x + al y −→ x′ then x −→ x′ and x′ .CC x′ as above, because a 6= al again.

I. Fábregas, D. de Frutos Escrig & M. Palomino
a

5
a

• For all a ∈ Al ∪ Abi , if x −→ x′ , then x + al y −→ x′ and x′ .CC x′ .
To prove completeness we consider p .CC q and reason by structural induction on p.
• If p is 0 then I(q) ⊆ Ar , since p cannot simulate any action in Al ∪ Abi . Then q = ∑ ar qr and we
can apply (Srp ) to each summand in turn to get 0 ⊑ q.
• Let us consider p = (∑ ar pr + ∑ al pl + ∑ ab pb ), distinguishing the summands of p which start with
actions in either Ar , Al or Abi . We decompose q in the same way to obtain q = (∑ br qr + ∑ bl ql +
∑ bb qb ). Then:
– For every ar there exists br , with ar = br , such that pr .CC qr and, by induction hypothesis,
pr ⊑ qr . Then ∑ ar pr ⊑ ∑ br qr . It could be the case that some summands of ∑ br qr are never
used to simulate any of the transitions of p, but then we can add all those summand by using
(Srp ), to derive ∑ ar pr ⊑ ∑ br qr .
– For the summands ∑ al pl and ∑ bl ql we can argue in exactly the same way, but starting with
the righhand side and using (Slp ) instead of (Srp ), to conclude now ∑ al pl ⊑ ∑ bl ql .
– Finally, using standard arguments for bisimulation, we can establish a full correspondence
between the summands ∑ ab pb and ∑ bb qb , having ab = bb and pb .CC qb , and by induction
hypothesis we prove ∑ ab pb ⊑ ∑ bb qb , thus concluding the proof. 2

3.2 Conformance semantics
Conformance simulation combines in a curious manner the features of both ordinary (covariant) and
inverse (contravariant) simulation: the addition of new capabilities is always considered beneficial but,
when an action is already offered, new ways to execute it are avoided since this leads to a more nondeterministic process.
To capture the first situation we need a variant of the axiom (S) characterizing ordinary simulation:
(SCS ) I(p) ∩ I(q) = 0/ =⇒ p ⊑ p + q.
For the latter, we instantiate the axiom (S−1 ) obtaining
−1
(SCS
) I(q) ⊆ I(p) =⇒ p + q ⊑ p,

which can be equivalently stated as
−1
(SCS,p
) ap + aq ⊑ ap.

There is, however, an important drawback: conformance simulation is not a precongruence because
it is not always preserved by +. Indeed, 0 .CS ab and ac .CS ac, but not ac .CS ab + ac. Fortunately,
to obtain a satisfactory algebraic treatment of the conformance order it is enough to consider the weakest precongruence contained in it, as is done for weak bisimulation and the corresponding observation
congruence. Let us simply replace the axiom (SCS ) by its guarded version
(SCS,g ) I(p) ∩ I(q) = 0/ =⇒ ap ⊑ a(p + q).
p
Definition 3 We define the conformance precongruence relation p .CS
q by
p
p .CS
q ⇐⇒ (p .CS q and I(p) ⊇ I(q)).

6

Equational Characterization of Covariant-Contravariant and Conformance Simulation Semantics

Note that the condition I(p) ⊇ I(q) is not imposed recursively but just on the initial states of the
processes, which corresponds to the fact that the (once) guarded axiom (SCS,g ) becomes sound for the
p
classical substitution calculus, in order to characterize the conformance precongruence .CS
.
p
is the coarsest
Proposition 2 If the set of actions A is infinite, then the precongruence relation .CS
precongruence contained in .CS .
p
Proof. Obviously, we have .CS
⊆ .CS . If there were a larger precongruence, there would exist p and
a·b

q with p .CS q but I(q) 6⊆ I(p): then, taking a ∈ I(q) \ I(p) and b ∈ A such that q 6−→ we would have
ab + p 6.CS ab + q (since ab 6.CS q).
p
:
Finally, both the prefix operator and + preserve .CS
a

a

p
p
• If p .CS
q, then ap .CS
aq since I(ap) = I(aq) = {a}, and for aq −→ q we have ap −→ p with
p
p .CS q.
a

p
p
aq + r since I(ap + r) = I(aq + r) = I(r) ∪ {a}, and for aq + r −→ q
q, then ap + r .CS
• If p .CS
a

b

b

p
we have ap + r −→ p with p .CS
q and, whenever aq + r −→ r′ with r −→ r′ , we trivially have
b

ap + r −→ r′ . 2
−1
} is complete for the conformance
Proposition 3 The set of axioms ACS = {B1 , B2 , B3 , B4 , SCS,g , SCS,p
p
precongruence relation .CS .
p
p
Proof. We show by induction on the depth of p that, whenever p .CS
q (resp. bp .CS
bq), we have
ACS ⊢ p ⊑ q (resp. ACS ⊢ bp ⊑ bq).
p
−1
• If 0 .CS
q, then also q = 0 and 0 ⊑ 0 using (SCS,p
).
p
• If b0 .CS
bq, then we can apply (SCS,g ) with p = 0.

Let us now consider p = ∑ai ∈I(p) ai pi j and q = ∑ai ∈I(q) ai qik .
p
• If p .CS
q then I(p) = I(q) and p .CS q, so for each qik there is some pi j with pi j .CS qik and
therefore we can apply the second induction hypothesis to conclude that ai pi j ⊑ ai qik . It is possible
that some summands pi j will be paired with no qik in the step above, but then we can apply the
−1
axiom (SCS,p
) to them to conclude the proof.
p
p
• Assume that bp .CS
bq. If I(p) = I(q) then we also have p .CS
q and this corresponds to the
situation above. However, in this case we could have I(p) ( I(q); then q = q′ + r, with r the
p
q′ and hence p ⊑ q′ . Now, we conclude the
summands ∑ai ∈I(q)\I(p) ai qik , I(p) = I(q′ ), and p .CS
proof by applying the axiom (SCS,g ) to q′ and r. 2

4

Axiomatization of the new simulation equivalences

Next we discuss the axiomatizability of the equivalences induced by covariant-contravariant and conformance simulations, obtaining a finite axiomatization for the latter, and also for the first, but only when
the set Abi of bivariant actions is empty. Instead, we also present the impossibility result proving that
covariant-contravariant simulation is not axiomatizable if we have Abi 6= 0/ and Ar ∪ Al 6= 0.
/

I. Fábregas, D. de Frutos Escrig & M. Palomino

7

4.1 Covariant-contravariant simulation
r,l
induced by
Let us first consider the case in which Abi = 0.
/ In order to axiomatize the equivalence ≡CC
r
l
(A , A )-simulation we apply the general procedure introduced in [9, 1, 8], based on the characterization

p ≡S p + q ⇐⇒ q .S p .
Thus we obtain:
(S1r,l
≡ ) ar (x + br y) = ar (x + br y) + ar x.
(S2r,l
≡ ) ar x = ar x + ar (x + bl y).
Obviously, the characterization above becomes unsound when contravariant prefixes appear because the
pure contravariant simulation satisfies
−1
q ≡−1
S p + q ⇐⇒ q .S p .

Therefore, we must reverse the inequalities above to obtain the adequate axioms for contravariant prefixes:
(S3r,l
≡ ) al x = al x + al (x + br y).
(S4r,l
≡ ) al (x + bl y) = al (x + bl y) + al x.
≡ = {B , B , B , B , S1r,l , S2r,l , S3r,l , S4r,l } to axiomatize
Now we would expect the set of axioms ACC
1
2
3
4
≡
≡
≡
≡
r
l
(A , A )-simulation equivalence. Certainly, all the axioms in this set are sound; in order to prove completeness in the absence of actions Abi , we start by stating the following lemma that gives us two useful
derived axioms.
Lemma 1 The following equalities are derivable:
r,l
{S1r,l
≡ , S2≡ } ⊢ ar (x + pr ) = ar (x + pr ) + ar (x + pl )
r,l
{S3r,l
≡ , S4≡ } ⊢ al (x + pl ) = al (x + pl ) + al (x + pr )

(DS1r,l
≡)
r,l
(DS2≡ )

where pr (resp. pl ) denotes any process prefixed by actions in Ar (resp. Al ); more formally, pr = ∑i∈I air pi
j
(resp. pl = ∑ j∈J al p j ).
Proof. We only show the case of (DS1r,l
≡ ). We start by proving that ar (x + pr ) = ar (x + pr ) + ar x by
induction over the size |I| of I.
• If |I| = 0, the result is trivial.
• If |I| = 1, we immediately obtain the result by applying the axiom (S1r,l
≡ ).
• For |I| > 1, we take I = I ′ ∪ {i} with |I ′ | = |I| − 1. Note that ar (x + pr ) = ar ((x + p′r ) + air pi ) so
that, applying axiom (S1r,l
≡ ), we obtain
ar (x + pr ) = ar ((x + p′r ) + air pi ) + ar (x + p′r ) = ar (x + pr ) + ar (x + p′r ).
Using the induction hypothesis with the term ar (x + p′r ) leads to
ar (x + pr ) = ar (x + pr ) + ar (x + p′r ) + ar x,
and, reusing the equality ar (x + pr ) + ar (x + p′r ) = ar (x + pr ) above, we obtain
ar (x + pr ) = ar (x + pr ) + ar x
as desired.

(1)

8

Equational Characterization of Covariant-Contravariant and Conformance Simulation Semantics

Now, we can analogously prove the equality
ar x = ar x + ar (x + pl ).

(2)

Replacing ar x in equation 1 by the righthand side of equation 2 produces
ar (x + pr ) = ar (x + pr ) + ar x + ar (x + pl )
and, applying equation 1 again, we finally obtain (DS1r,l
≡ ):
ar (x + pr ) = ar (x + pr ) + ar (x + pl ).
2
For the main proof we have to adapt the classic technique for the completeness of the axiomatization
of the plain simulation semantics (p .S q implies AS ⊢ q = p + q), taking into account the difference
between covariant and contravariant actions. For technical reasons we need to consider a “free” arbitrary
term r.
Proposition 4 If p .CC q then, for all processes r:
≡
ACC
⊢ ar (q + r) = ar (q + r) + ar (p + r)

and
≡
ACC
⊢ al (p + r) = al (p + r) + al (q + r).

Proof. We proceed by induction on the depth of p. We start by decomposing both p and q as follows:
p = pr + pl , q = qr + ql , where pr = ∑i∈Ipr air pi , pl = ∑i∈Ip ail pi , qr = ∑i∈Iqr air qi and ql = ∑i∈Iq ail qi .
l
l
Then, it is clear that the depths of both pr and pl are less or equal than the depth of p and besides we
have p .CC q ⇐⇒ pr .CC qr ∧ pl .CC ql .
Next, let us consider pr .CC qr : this is an instance of the hypothesis of the statement to prove, which
corresponds to the particular case in which I(p) ∪ I(q) ⊆ Ar . Then, we need to prove both
≡
ACC
⊢ ar (q + r) = ar (q + r) + ar (p + r)

and
≡
ACC
⊢ al (p + r) = al (p + r) + al (q + r).

Let us consider in detail the second statement.
≡ ⊢ a r = a r + a (q + r) by an application of the equation (DS2r,l ), with
• If p = 0, it follows that ACC
l
l
l
≡
pl = 0, x = r, and pr = q.

• If p = ∑i∈I air p′i and q = ∑i∈J air p′i , from p .CC q it follows, without loss of generality, that I ⊆
J = I ∪ J ′ and then we take J = I ∪ J ′ with J ′ chosen such that J ′ ∩ I = 0,
/ with p′i .CC q′i for all
≡ ⊢ ai q′ = ai q′ + ai p′ . Next we obtain A ≡ ⊢
i ∈ I. Now, by induction hypothesis, ACC
∑i∈I air q′i =
r i
r i
r i
CC
′
≡
′
i
i
∑i∈I ar qi + p and hence, by adding ∑i∈J′ ar qi to both sides, ACC ⊢ q = q + p, by congruence, we
≡ ⊢ q + r = q + p + r. Now, by applying (DS2r,l ) with x = p + r, p = 0, and p = q, we
have ACC
l
r
≡
≡ ⊢ a (p + r) = a (p + r) + a (p + r + q) which, combined with the previous equation,
obtain ACC
l
l
l
≡ ⊢ a (p + r) = a (p + r) + a (q + r).
finally leads to ACC
l
l
l

I. Fábregas, D. de Frutos Escrig & M. Palomino

9

The first statement above is proved in a similar way, and the ones arising from pl . ql can be dealt
with analogously.
To conclude, we consider the general case p .CC q. By applying the results obtained above, starting
from both pr .CC qr and pl .CC ql , we have
≡
ACC
⊢ ar (qr + r) = ar (qr + r) + ar (pr + r)

and
≡
ACC
⊢ ar (ql + r) = ar (ql + r) + ar (pl + r).

In particular, making r equal to ql + r′ in the first equality:
≡
ACC
⊢ ar (qr + ql + r′ ) = ar (qr + ql + r′ ) + ar (pr + ql + r′ ).

(It is at this point that the “free” variable r in the statement is needed, so as to be able to proceed by
instantiating it in a suitable manner). Now, instantiating r with pr + r′ in the second derived equation:
≡
⊢ ar (pr + ql + r′ ) = ar (pr + ql + r′ ) + ar (pr + pl + r′ ).
ACC

If we now combine the last two equations we can obtain
≡
ACC
⊢ ar (qr + ql + r′ ) = ar (qr + ql + r′ ) + ar (pr + pl + r′ ),

and, since r′ is arbitrary, we finally get
≡
ACC
⊢ ar (q + r) = ar (q + r) + ar (p + r).

We can proceed in a similar way for al , thus obtaining
≡
ACC
⊢ al (p + r) = al (p + r) + al (q + r).

And this concludes the proof. 2
The main theorem is now at hand.
≡ = {B , B , B , B , S1r,l , S2r,l , S3r,l , S4r,l } is
Theorem 1 Whenever A = Ar ∪ Al , the set of axioms ACC
1
2
3
4
≡
≡
≡
≡
complete for (Ar , Al )-simulation equivalence.
≡ ⊢ p = q. The proof will follow by induction on the depth of
Proof. Let p ≡CC q: we need to prove ACC
p.

• If p = 0 we obviously have q = 0.
• Let p = ∑i∈I air pir + ∑ j∈J alj plj and q = ∑i∈I ′ air qir + ∑ j∈J′ alj qlj . Then,
′

′

– for each i ∈ I, there exists some i′ ∈ I ′ with air = air and pir .CC qir , and
′′
′
′′
′
– for each i′ ∈ I ′ there exists some i′′ ∈ I with air = air and qir .CC pir .
Obviously, it could be the case that i 6= i′′ . Then, we could repeat the same argument with i1 = i′′ ,
and with i2 = i′′1 , . . . , to obtain a sequence (i, i1 , i2 , . . .). Since |I| < ∞, eventually we will find
im = in and, hence,
′

′′

′

′′

′

– for each i ∈ I we obtain i′ ∈ I ′ and i′′ ∈ I such that air = air = air , pir .CC qir and pir ≡CC qir .

10

Equational Characterization of Covariant-Contravariant and Conformance Simulation Semantics
Of course, we can repeat the same reasoning starting with i′ ∈ I ′ as well as for the contravariant
summands in a dual way, to obtain the following decompositions:
p = ∑ air pir +

∑ akr pkr + ∑

akl pkl +

∑ air qir + ∑ akr qkr + ∑

akl qkl +

i∈I

and,
q=

′

i′ ∈I ′

k∈K

′

k′ ∈K ′

′

k∈K

′

k′ ∈K ′

∑ aml pml

m∈M

′

′

∑

′

m
am
l ql

′

m′ ∈M′

where:
–
–
–
–
–
–

for all i ∈ I, there exists k ∈ K such that air = akr and pir .CC pkr ; and
m
k′
k′
for all m ∈ M, there exists k′ ∈ K ′ such that am
l = al and pl .CC pl ; and
′
′
for all i′ ∈ I ′ , there exists k ∈ K such that air = akr and qir .CC qkr ; and
′
m
k′
k′
for all m′ ∈ M ′ , there exists k′ ∈ K ′ such that am
l = al and ql .CC ql ; and
for all k ∈ K, pkr ≡CC qkr ; and
′
′
for all k′ ∈ K ′ , pkl ≡CC qkl .
′

′

Then we can apply the induction hypothesis to any pair (pkr , qkr ) and also to any pair (pkl , qkl ). To
conclude the proof we only need to apply Proposition 4, taking r = 0, to any such pairs (pir , pkr )
′
and (pkl , pm
l ), and analogously for the components of q. 2
The addition of bivariant actions (assuming that there are already other actions present) changes the
picture completely. Now, it is no longer possible to axiomatize the equivalence.
Theorem 2 If Abi 6= 0/ and Ar ∪ Al 6= 0,
/ then (Ar , Al )-simulation equivalence is not finitely axiomatizable.
Proof. Let us take abi ∈ Abi and, without loss of generality, ar ∈ Ar . We consider the two families of
processes
pn = ar anbi ar 0 and qn = ar anbi ar 0 + ar anbi 0,
where, as usual, we denote by anbi (with n ≥ 0) the repeated application of the prefix operator abi (n
times).
It is easy to check that pn ≡CC qn . On the one hand, pn .CC qn trivially; on the other hand, checking
n
that qn .CC pn simply amounts to checking that 0 .CC ar . (However, note that taking p−
n = abi ar 0 and
−
−
−
−
n
n
−
qn = abi ar 0 + abi 0 does not lead to pn ≡CC qn ; indeed, pn 6.CC qn because if we start with the first abi
n−1
n−1
from the second summand of q−
n then abi ar 0 6.CC abi 0.) Now, for any finite axiomatization A , let n
be bigger than the depth of any term appearing in A ; we are going to show that if A is sound for ≡CC
then we cannot have A ⊢ pn = qn .
We will show that if we start with pn and obtain a sequence of equivalent terms pn = p1n = p2n = . . .,
where each term is obtained from the previous one by an application of a single axiom in A , then no
j
pn can be qn . If we apply an axiom to pn in a position different from its root, then we are transforming
′
a subprocess p′ = am
bi ar 0, with m ≤ n, into some equivalent process q ≡CC p . If we define q ↓ m as the
process obtained by “pruning” q at depth m, the result will be bisimilar to am
bi 0, since q cannot execute
any other action until it executes the prefix abi m times and, moreover, it cannot stop in the meantime. In a
similar way, from q ≡CC p′ we also infer that q ↓ (m + 1) ∼ p′ ↓ (m + 1) and then the obtained p1n satisfies
p1n ↓ (n + 2) ∼ pn . The same argument can be applied starting from any pnj such that pnj ↓ (n + 2) ∼ pn ,
so that this invariant is preserved as long as there is no application of an axiom in A at the root of any
pnj .

I. Fábregas, D. de Frutos Escrig & M. Palomino

11

Therefore, the only possible way to break this invariant, that obviously is not satisfied by qn , is
to apply an axiom from A at the root of some pnj . In that case, the lefthand side of such an axiom
would match several prefixes of the process ar am
bi 0 and then, following [13], it is easy to see that the
j
corresponding axiom has to be correct under bisimulation, too. As a consequence, the process pn+1
j
resulting after the application of the axiom also satisfies pn+1
↓ (n + 2) ∼ pn . Therefore by repeated
application of the axioms in A we will never reach a term such as qn , thus concluding A 0 pn = qn . 2
Note that the proof would remain valid even if we allowed conditional axioms whose conditions only
observed the process locally, since the key fact in the proof above is that in order to generate the choice
at qn we need to “see from the top” that the two branches below, even if different from each other, can
be joined to obtain a process equivalent to pn . But the branches cannot be joined bottom up, in a step
−
by step fashion, since p−
n 6≡CC qn . Therefore, a conditional axiomatization whose conditions observe the
processes locally would suffer the same problems as a purely equational one.

4.2 Conformance simulation
p
As before, we start by applying to the axioms characterizing .CS
the general procedure presented in
[9, 1, 8]. In this case we obtain the following two axioms:

(SCS
/ =⇒ ap = ap + a(p + q).
≡ ) I(p) ∩ I(q) = 0
(S−1,CS
) I(q) ⊆ I(p) =⇒ a(p + q) = a(p + q) + ap.
≡
Note that we have used the contravariant version of the procedure because once we compare two
p
processes offering the same set of actions the behavior of .CS
is contravariant since we have
p
ap &CS
ap + aq.

Therefore, we cannot apply the general results in [9, 8] to prove the completeness of the proposed axiomatization. However, a beautiful variant of the classical proof for plain simulation will do the job.
≡ = {B , B , B , B , SCS , S−1,CS } is a complete axiomatization for the
Theorem 3 The set of axioms ACS
≡
1
2
3
4 ≡
simulation equivalence ≡CS .
p
Proof. First note that p ≡CS q implies I(p) = I(q) and p ≡CS
q, and therefore we can use either ≡CS or
p
≡CS
, indistinctly. It is also routine to check the correctness of the axioms for ≡CS . To prove completeness,
p
≡ ⊢ p = p + q. Obviously, then we are done because p ≡
we show that p .CS
q implies ACS
CS q implies
p
p
p .CS q and q .CS p.
We proceed by induction on the depth of p:

• p = 0 implies q = 0 trivially.
a

a

a

a

p
q with p −→. Then we also have q −→ and for all q′ with q −→ q′ there exists p −→ p′
• Let p .CS
p
q′ since it is possible that I(p′ ) I(q′ ),
such that p′ .CS q′ . Note that we cannot conclude p′ .CS
p
′
′′
′′
′
but then we can write q = q + r with I(q ) = I(p ) and I(r) ∩ I(q′′ ) = 0.
/ It is clear that p′ .CS
q′′ ,
≡ ⊢ p′ = p′ + q′′ . Then, we have A ≡ ⊢ ap′ = a(p′ +
so that by induction hypothesis we obtain ACS
CS
−1,CS
′′
≡
′
′
≡ ⊢ ap′ = ap′ + aq′′ . Now,
q ) and applying (S≡ ), ACS ⊢ ap = a(p + q′′ ) + aq′′ , and then ACS
≡
′′
′′
′′
≡
′
′
′
by applying (S,CS
≡ ) we have ACS ⊢ aq = aq + a(q + r), to conclude that ACS ⊢ ap = ap + aq
≡
and therefore ACS ⊢ p = p + q. 2

12

Equational Characterization of Covariant-Contravariant and Conformance Simulation Semantics

Note that (S−1,CS
) is the axiom characterizing the ready simulation equivalence, from which we
≡
conclude that ≡RS ⊆ ≡CS . Obviously, the reverse inclusion is false since (SCS
≡ ) is not sound for ≡RS .
For instance, ab =CS ab + a(b + c), but a(b + c) 6.RS ab. In fact, we also have a(b + c) 6.S ab, proving
that ≡CS * ≡S . In order to obtain ≡RS from ≡CS we should strengthen the definition of the latter by
considering ready conformance simulations defined as plain conformance simulations, but only allowing
pairs of processes satisfying I(p) = I(q). If we denote by .RCS the generated preorder we have the
following result.
−1
Proposition 5 .RCS = .−1
RS , and therefore ≡RCS = ≡RS and .RS ⊆ .CS .

Since (S−1,CS
) is the axiom that defines ready simulation equivalence, it can be presented in an
≡
equivalent way avoiding the condition and thus obtaining a pure algebraic axiom. However, it is not
clear whether axiom (SCS
≡ ) allows such a finite pure algebraic presentation, and in fact the same happens
with the axiom (SCS ) in the axiomatization of the conformance preorder. Hence, it could be the case that
both the conformance preorder and the induced equivalence are not finitely axiomatizable using pure
equational axioms, as is the case for ready trace semantics.

5

Conclusions

We have continued with the study of covariant-contravariant simulation and conformance simulation
semantics started in [12, 11] by considering the axiomatization of the preorders and equivalences that
they define.
We have showed that the desired axiomatizations can be obtained from that of the plain simulation preorder, whose completeness proof can be adapted in a simple, but elegant manner to obtain the
completeness of the new axiomatizations. Also, by applying a suitable variation of our “ready to preorder” techniques [9] we have obtained the axiomatizations of the corresponding conformance simulation equivalence. Surprisingly, we also succeeded in axiomatizating the equivalence for covariantcontravariant simulations but only in the particular case where Abi = 0;
/ otherwise, we proved that the
covariant-contravariant simulation equivalence has turned out to be the second known example of a semantics whose defining preorder can be finitely axiomatized, but the induced equivalence cannot. The
first example of such a borderline situation can be found in [5]. It is curious to notice that although the
two semantics are completely different (the semantics here is quite simple since it is a plain semantics,
while the one in [5] is much more complicated), and in our case it is clear that the difficulties stem from
the interference between bivariant and monovariant actions, the structure of the considered “counterexamples” in both cases is essentially the same: there is a choice betweeen two quite long branches which
can be can joined into a single one, but this should be done in a single step because the choice cannot
be delayed at all, even if the beginnings of the two branches are the same. Therefore, in order to capture
the equivalence, we would need an axiom able to “see” the (too far away) ends of the two branches,
but this is of course impossible with a finite number of axioms since the lengths of the branches in the
counterexamples can be arbitrarily long.
We expect our work on the subject to contribute to a better understanding of all the complex situations
that arise when covariant and contravariant concepts coexist. This, for example, is the case in all the
recent works on modal, input-output or interface formalisms, that try to clarify the relationships betwen
specifications and implementations. In fact, it is our intention to continue with this line of research by
trying to discover, and take benefit from all the connections between our work and those cited in this
paper.

I. Fábregas, D. de Frutos Escrig & M. Palomino

13

References
[1] Luca Aceto, Wan Fokkink, and Anna Ingólfsdóttir. Ready to preorder: get your BCCSP axiomatization
for free! In Till Mossakowski, Ugo Montanari, and Magne Haveraaen, editors, Algebra and Coalgebra in
Computer Science. Second International Conference, CALCO 2007, Bergen, Norway, August 20–24, 2007.
Proceedings, volume 4624 of Lecture Notes in Computer Science, pages 65–79. Springer, 2007.
[2] Adam Antonik, Michael Huth, Kim Larsen, Ulrik Nyman, and Andrzej Wasowski. 20 Years of Mixed and
Modal Specifications. Bulletin of the European Association for Theoretical Computer Science, May 2008.
[3] Nikola Benes, Jan Kretı́nský, Kim Guldstrand Larsen, and Jirı́ Srba. On determinism in modal transition
systems. Theoretical Computer Science, 410(41):4026–4043, 2009.
[4] Stephen D. Brookes and A. W. Roscoe. An improved failures model for communicating processes. In
Stephen D. Brookes, A. W. Roscoe, and Glynn Winskel, editors, Seminar on Concurrency, volume 197 of
Lecture Notes in Computer Science, pages 281–305. Springer, 1984.
[5] Taolue Chen and Wan Fokkink. On the axiomatizability of impossible futures: preorder versus equivalence.
In Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008,
24-27 June 2008, Pittsburgh, PA, USA, pages 156-165. 2008.
[6] Corina Cı̂rstea. A modular approach to defining and characterising notions of simulation. Information and
Computation, 204(4):469–502, 2006.
[7] Luca de Alfaro and Thomas A. Henzinger. Interface automata. In ESEC / SIGSOFT FSE, pages 109–120,
2001.
[8] David de Frutos-Escrig, Carlos Gregorio-Rodrı́guez, and Miguel Palomino. On the unification of process
semantics: Equational semantics. Electronic Notes in Theoretical Computer Science, 249:243–267, 2009.
[9] David de Frutos-Escrig, Carlos Gregorio-Rodrı́guez, and Miguel Palomino. Ready to preorder: an algebraic
and general proof. J. Log. Algebr. Program., 78(7):539–551, 2009.
[10] David de Frutos-Escrig, Fernando Rosa Velardo, and Carlos Gregorio-Rodrı́guez. New bisimulation semantics for distributed systems. In John Derrick and Jüri Vain, editors, Formal Techniques for Networked and
Distributed Systems — FORTE 2007, 27th IFIP WG 6.1 International Conference, Tallinn, Estonia, June
27-29, 2007, Proceedings, volume 4574 of Lecture Notes in Computer Science, pages 143–159. Springer,
2007.
[11] Ignacio Fábregas, David de Frutos-Escrig, and Miguel Palomino. Logics for contravariant simulations.
In John Hatcliff and Elena Zucca, editors, FMOODS/FORTE 2010, Lecture Notes in Computer Science.
Springer. To appear.
[12] Ignacio Fábregas, David de Frutos-Escrig, and Miguel Palomino. Non-strongly stable orders also define
interesting simulation relations. In Alexander Kurz, Marina Lenisa, and Andrzej Tarlecki, editors, CALCO,
volume 5728 of Lecture Notes in Computer Science, pages 221–235. Springer, 2009.
[13] Jan Friso Groote. A new strategy for proving omega-completeness applied to process algebra. In Jos C. M.
Baeten, and Jan Willem Klop, editors, CONCUR, volume 458 of Lecture Notes in Computer Science, pages
314–331. Springer, 1990.
[14] Jesse Hughes and Bart Jacobs. Simulations in coalgebra. Theoretical Computer Science, 327(1-2):71–108,
2004.
[15] Kim Guldstrand Larsen, Ulrik Nyman, and Andrzej Wasowski. Interface input/output automata. In Jayadev
Misra, Tobias Nipkow, and Emil Sekerinski, editors, FM, volume 4085 of Lecture Notes in Computer Science,
pages 82–97. Springer, 2006.
[16] Kim Guldstrand Larsen and Bent Thomsen. A modal process logic. In LICS, pages 203–210. IEEE Computer
Society, 1988.
[17] Guy Leduc. A framework based on implementation relations for implementing LOTOS specifications. Computer Networks and ISDN Systems, 25(1):23–41, 1992.

14

Equational Characterization of Covariant-Contravariant and Conformance Simulation Semantics

[18] Nancy Lynch. I/o automata: A model for discrete event systems. In 22nd Annual Conference on Information
Sciences and Systems, pages 29–38, 1988.
[19] David Park. Concurrency and automata on infinite sequences. In Peter Deussen, editor, Theoretical Computer
Science, 5th GI-Conference, Karlsruhe, Germany, March 23-25, 1981, Proceedings, volume 104 of Lecture
Notes in Computer Science, pages 167–183. Springer, 1981.
[20] Jean-Baptiste Raclet, Eric Badouel, Albert Benveniste, Benoı̂t Caillaud, Axel Legay, and Roberto Passerone.
Modal interfaces: unifying interface automata and modal specifications. In EMSOFT ’09: Proceedings of
the seventh ACM international conference on Embedded software, pages 87–96, New York, NY, USA, 2009.
ACM.
[21] Jan Tretmans. Conformance testing with labelled transition systems: Implementation relations and test generation. Computer Networks and ISDN Systems, 29(1):49–79, 1996.

