=Paper=
{{Paper
|id=None
|storemode=property
|title=A Rule Format for Rooted Branching Bisimulation
|pdfUrl=https://ceur-ws.org/Vol-1032/paper-05.pdf
|volume=Vol-1032
|dblpUrl=https://dblp.org/rec/conf/csp/CastiglioniLT13
}}
==A Rule Format for Rooted Branching Bisimulation==
https://ceur-ws.org/Vol-1032/paper-05.pdf
A Rule Format for Rooted Branching
Bisimulation
Valentina Castiglioni, Ruggero Lanotte, and Simone Tini
Dipartimento di Scienza e Alta Tecnologia, Università dell’Insubria, Como, Italy
Abstract. SOS rule formats are sets of syntactical constraints over SOS
transition rules ensuring semantical properties of the derived LTS. Given
a rule format, our proposal is to try to relax the constraints imposed by
the format on each single transition rule at the price of introducing some
reasonable constraint on the form of the whole set of rules, obtaining
a new format ensuring the same semantical property and being less de-
manding than the original one. We demonstrate that this can be done by
applying such an idea to a well established rule format ensuring the prop-
erty of congruence for the rooted branching bisimulation equivalence.
1 Introduction
Structural operational semantics [1] (SOS) is a standard framework to provide
process description languages with a semantics. The abstract syntax of a lan-
guage is given through a signature, namely a set of operators together with their
arity. The semantics is given through a labeled transition system (LTS), namely
a set of states that represent processes and that are terms over the signature,
together with a set of transitions between states describing computational steps.
An LTS is defined by means of a transition system specification (TSS), namely a
premises
set of transition rules of the form conclusion , which, intuitively, permit to derive
transitions between processes from transitions between other processes.
To abstract away from information carried by an LTS that may be considered
irrelevant in a given application context, several notions of behavioral equivalence
were defined (see [2, 3]). Some of these equivalences, like weak bisimulation [4]
and branching bisimulation [5], equate LTS states that incorporate so called
silent steps representing internal moves by processes that are not observable by
the external environment, and are referred to as weak equivalences. To ensure
compositional modelling and verification, it is crucial that a given behavioral
equivalence be a congruence w.r.t. all operators of the signature.
Since [6] a transition rule format is a set of syntactical constraints on the rules
of the TSS, aiming to ensure a given property of the LTS. Several rule formats
were developed to ensure the property of congruence for a given behavioral
equivalence (see [7] for a survey). The original formats for weak equivalences
were proposed in [8]. At present, the standard formats are those in [9–11].
Sometimes the syntactical constraints imposed by the formats on the premises
of the transition rules are quite strict. For instance, the rule formats in [9–11]
50 V. Castiglioni, R. Lanotte, S. Tini
prohibit the features of lookahead, namely the ability to test for two consecutive
moves by a process, and double testing for running processes, namely the ability
to test for two different moves by a process. Our idea is that in some cases it
is worth to relax the constraints on the single rules, at the price of introducing
some constraints on the form of the whole set of transition rules in the TSS, pro-
vided these are not too heavy. To demonstrate how this can be done, we consider
the format of [9] for rooted branching bisimulation, we relax the constraints of
this format by admitting both lookahead and double testing, and we add the
reasonable constraint that lookahead and double testing come together with the
ability of testing for an arbitrary number of silent steps, which means introduc-
ing a constraint on the set of rules of the TSS since a single rule is required for
each number of silent steps. A natural extension of our work is to apply the same
strategy to the formats of [10].
The paper is organized as follows: in Section 2, we recall some base notions
on SOS, in Section 3 we recall the format of [9], in Section 4 we present our
congruence format for rooted branching bisimulation and we end with some
conclusions and discussion of related work in Section 5.
2 Preliminaries
In this section we recall some definitions that are standard in the SOS framework.
As usual, we assume that the abstract syntax of a process description lan-
guage is given by a signature, namely a structure Σ = (F, r), where (i) F is
a set of function names, also called language operators, and (ii) r : F → N is
a rank function, which gives the arity of a function name. An operator f ∈ F
is called a constant if r(f ) = 0. We also assume a set of (process) variables
V disjoint from F , and let x, y, z range over V. Let W ⊆ V be a set of vari-
ables. The set of Σ-terms over W , notation T (Σ, W ), is the least set satisfy-
ing: (i) W ⊆ T (Σ, W ), and (ii) if f ∈ F and t1 , · · · , tr(f ) ∈ T (Σ, W ), then
f (t1 , · · · , tr(f ) ) ∈ T (Σ, W ). T (Σ, ∅) is the set of all closed terms, also called pro-
cesses, and abbreviated as T (Σ). T (Σ, V) is the set of all open terms and abbre-
viated as T(Σ). By ≡ we denote the syntactical equality relation between terms.
Finally, Var(t) ⊆ V denotes the set of variables in term t, namely Var(x) = {x}
Sr(f )
and Var(f (t1 , . . . , tr(f ) )) = i=1 Var(ti ).
In SOS framework, the semantic model is that of LTSs.
Definition 1 (Labeled Transition System). A Labeled Transition System
(LTS) is a triple (T (Σ), A, →
− ), where i) Σ is a signature; ii) A is a countable
set of actions; and iii) →
− ⊆ T (Σ) × A × T (Σ) is a transition relation.
a
Following standard notation, we write t −→ t0 for (t, a, t0 ) ∈ →
− . This represents
a computation step of kind a taking process t to process t0 .
LTSs are built by means of transition systems specifications, namely sets of
premises
transition rules of the form conclusion . Here we assume that these rules are in
the ntyft-format [12]. This choice is reasonable since ntyft-format is very general
and for transition system specifications that are complete (see Def. 5 below)
A Rule Format for Rooted Branching Bisimulation 51
it guarantees that bisimilarity equivalence relation is a congruence w.r.t. all
operators in F .
Definition 2 (ntyft-rule, [12]). A ntyft-rule is of the form
aj k b
{tj −−→ yj | j ∈ J} {tk −−→
6 | k ∈ K}
a
f (x1 , . . . , xr(f ) ) −→ t
with J, K at most countable sets of indexes, tj , tk , t ∈ T(Σ), aj , bk , a ∈ A, yj ∈ V,
f ∈ F , x1 , . . . , xr(f ) ∈ V, such that:
– the x1 , . . . , xr(f ) and the yj for j ∈ J are all distinct variables.
aj k b
The expressions tj −−→ yj (resp. tk −−→6 ) above the line are called positive (resp.
negative) premises. Given a rule ρ, we denote the set of positive (resp. negative)
premises by pprem(ρ) (resp. nprem(ρ)), and the set of all premises by prem(ρ) =
a
pprem(ρ) ∪ nprem(ρ). The expression f (x1 , . . . , xr(f ) ) −→ t below the line is
called conclusion, notation conc(ρ), where f (x1 , . . . , xr(f ) ) is called the source of
ρ, notation src(ρ), the xi are the source variables denoted by xi ∈ src(ρ), and
term t is the target of ρ, notation trgt(ρ). We denote the set of variables in ρ by
Var(ρ), free variables by free(ρ) = Var(ρ) \ ({x1 , . . . , xr(f ) } ∪ {yj | j ∈ J}), and
bound variables by bound(ρ) = Var(ρ) \ free(ρ).
Definition 3 (ntyft-TSS, [12]). A ntyft-transition system specification, ntyft-
TSS for short, is a set of ntyft-rules.
Assigning an LTS to a TSS having rules with negative premises is not trivial.
See [7] for a deep discussion. Let us describe the approach we adopt here, namely
that of least three-valued stable model, introduced in [13] in logic programming.
a a
An expression t −→ t0 (resp. t −→ 6 ) is called a positive (resp. negative) literal
where t, t0 ∈ T(Σ) and a ∈ A. So, premises and conclusions in rules are literals.
A substitution is a mapping σV : V → T(Σ). A substitution is closed if it
maps each variable to a closed term in T (Σ). A substitution extends to terms
a
by σV (f (t1 , . . . , tr(f ) )) = f (σV (t1 ), . . . , σV (tr(f ) )), to literals by σV (t −→ t0 ) =
a b b
σSV (t) −→ σV (t0 ) and σV (t −
→6 ) = σV (t) −
→6 , and to ntyft-rules by σV (ρ) =
π∈prem(ρ) σV (π)
σV (conc(ρ)) . A closed substitution instance of a ntyft-rule is called a closed
ntyft-rule. We denote with H N
π a closed ntyft-rule, and with π a closed ntyft-rule
having only negative premises (i.e. all elements in N are negative literals).
Given a set of closed positive literals P , a collection of closed negative literals
b b
N holds for P , denoted P |= N , iff for each t − →
6 ∈ N we have that t − → t0 6∈ P
0
for any t ∈ T (Σ).
Definition 4 (Proof of a closed transition rule). A proof from a TSS T of
a closed transition rule Hπ is an upwardly branching tree in which all upwardly
paths are finite, and the nodes are labeled by closed literals such that:
52 V. Castiglioni, R. Lanotte, S. Tini
– the root is labeled by π;
– if K is the set of the labels of the nodes directly above a node labeled l, then:
• either K = ∅ and l ∈ H;
• or Kl is a closed substitution instance of a transition rule in T .
Given a TSS T , we consider a partitioning of the collection of positive literals
to three disjoint sets: i) the set C of positive literals that are certainly true; ii) the
set U of positive literals for which it is unknown whether or not they are true; and
iii) the set of remaining literals that are false. Such a partitioning, determined
by C and U , constitutes a three-valued stable model, denoted hC , U i, for T if:
– a positive transition π is in C if and only if T proves a closed transition rule
N
π , where N contains only negative literals and C ∪ U |= N ;
– a positive transition π is in C ∪ U if and only if T proves a closed transition
rule Nπ , where N contains only negative literals and C |= N .
Each TSS T allows an (information-)least three-valued stable model hC , U i,
in the sense that the set U is maximal. In [14] two-valued stable models were
studied, which are three-valued stable models for which the set of unknown
positive literals is empty.
Definition 5 (Complete TSS, [15]). A TSS is complete if its least three-
valued stable model is a two-valued stable model.
If a TSS is complete, then it allows only one three-valued stable model, which
is taken as the LTS built from the TSS. Only complete TSSs are considered to
be meaningful. Notice that a TSS that does not contain transition rules with
negative premises is complete for sure.
3 Rooted Branching Bisimulation as a Congruence
Behavioral equivalence relations over processes are usually defined to abstract
away information provided by an LTS which is not considered to be relevant
for a given application context. Here we consider branching bisimulation, one of
those that identify LTS states that incorporate so called silent steps.
In the following we assume that A contains the special silent action τ . The
τ ε
reflexive and transitive closure of relation −→ is denoted with −→. Finally, let us
ε ε ε
introduce notation t −→n t for n ∈ N: we have t −→0 t if t ≡ t0 and t −→n+1 t0
0 0
τ ε ε ε
if t −→ t00 and t00 −→n t0 for some t00 ∈ T (Σ). Hence, −→= n∈N −→n .
S
Definition 6 (Branching bisimulation, [5]). Take a three-valued stable model
hC , U i. A symmetric relation B over T (Σ) is a branching bisimulation with re-
a
spect to C if whenever s B t and s −→ s0 ∈ C we have:
– either a = τ and s0 B t;
ε a
– or t −→ t00 , t00 −→ t0 ∈ C for t0 , t00 ∈ T (Σ) such that s B t00 and s0 B t0 .
A Rule Format for Rooted Branching Bisimulation 53
We call s and t branching bisimilar if there exists a branching bisimulation
relation B such that s B t. The union of all branching bisimulations over T (Σ) is
the greatest branching bisimulation over T (Σ), it is called branching bisimilarity
and it is denoted with ↔bb . Branching bisimilarity is an equivalence relation [16].
A crucial property of process description languages to ensure compositional
modelling and verification is the compatibility of process operators with the
behavioral relation chosen for the application context. In algebraic terms the
compatibility of a behavioral equivalence R with operator f ∈ F is a congruence.
Definition 7 (Congruence). An equivalence relation R over T (Σ) is a con-
gruence if for all f ∈ F , f (s1 , . . . , sr(f ) ) R f (t1 , . . . , tr(f ) ) whenever si R ti for
i = 1, . . . , r(f ).
Branching bisimulation is not a congruence for the nondeterministic choice
a a
operator + defined by rules x1 −→ay1 and x2 −→ay2 , which is offered by most
x1 +x2 −
→ y1 x1 +x2 −
→ y2
of process description languages in the literature. To remedy to this problem the
rootedness condition is usually assumed.
Definition 8 (Rooted branching bisimulation). Take a three-valued stable
model hC , U i. A symmetric relation R over T (Σ) is a rooted branching bisim-
a a
ulation with respect to C if whenever s R t and s −→ s0 ∈ C we have t −→ t0 ∈ C
0 0↔ 0
for t such that s bb t .
We call s and t rooted branching bisimilar if there exists a rooted branching
bisimulation relation R such that s R t. The union of all rooted branching bisim-
ulations over T (Σ) is the greatest rooted branching bisimulation over T (Σ), it is
called rooted branching bisimilarity and it is denoted with ↔rb . Rooted branch-
ing bisimilarity is clearly an equivalence relation.
In the following we recall the rule format RBB-safe [9], which ensures that
rooted branching bisimulation is a congruence for all operators in the TSS.
A patience rule for the i-th argument of a function symbol f ∈ F is a ntyft-
rule of the form
τ
xi −→ yi
τ
f (x1 , . . . , xr(f ) ) −→ f (x1 , . . . , xi−1 , yi , xi+1 , . . . , xr(f ) )
Following [9], we assume that each argument of each function symbol f ∈ F
is labeled either tame or wild. A context, denoted with C[ ], is an open term in
T(Σ) with one occurrence of the context symbol [ ].
Definition 9 (w-nested context, [9]). The collection of w-nested contexts is
defined inductively by:
– [ ] is w-nested;
– if C[ ] is w-nested, and argument i of function symbol f is wild, then also
f (t1 , . . . , ti−1 , C[ ], ti+1 , . . . , tr(f ) ) is w-nested.
54 V. Castiglioni, R. Lanotte, S. Tini
Definition 10 (RBB safe TSS, [9]). A TSS T is called RBB safe, with respect
to a tame/wild labeling of arguments of function symbols in F , if each of its
transition rules is
1. either a patience rule for a wild argument of a function symbol,
2. or a ntyft-rule ρ with source f (x1 , . . . , xr(f ) ) and right-hand sides of positive
premises {yj | j ∈ J}, such that the following requirements are fulfilled:
(a) Variables yj for j ∈ J do not occur in left-hand sides of premises of ρ;
(b) If argument i of f is wild and does not have a patience rule in T , then
xi does not occur in left-hand sides of premises of ρ;
(c) If argument i of f is wild and has a patience rule in T , then xi occurs in
the left-hand side of no more than one premise of ρ, where this premise
i. is positive,
τ
ii. does not contain the relation −→, and
iii. has left-hand side xi ;
(d) Variables yj for j ∈ J and variables xi for i a wild argument of f may
only occur at w-nested positions in the target of ρ.
Theorem 1 (Rooted branching bisimulation as a congruence, [9]). If a
complete TSS is RBB safe, then the rooted branching bisimulation equivalence
that it induces is a congruence.
In [9] several counter-examples are given to show that the syntactic con-
straints of Def. 10 cannot be relaxed in any trivial way. Our aim is to show
that the constraints that prohibit lookahead (constraint 2a) and double testing
for wild arguments of operators (constraint 2c) on the single rules of the TSS
can be relaxed, provided that suitable and reasonable (i.e non too-demanding)
constraints on the whole set of rules of the TSS are introduced. In the following
we assume a TSS T containing the CCS-like sequencing operator · defined by
the rules a for a ∈ A, the CCS-like nondeterministic choice operator +
a·x−
→x
recalled above, the idle process 0 and the unary operators f1 , f2 defined below.
Constraint 2a in Def. 10 prohibits lookahead, namely the ability of testing
for two (or more) subsequent moves by a source argument. An example of rule
violating this constraint is the following rule ρf1 for operator f1 :
a b
x1 −→ y1 y1 −
→ y2
a
f1 (x1 ) −→ 0
Let us consider processes s ≡ a · b · 0 and t ≡ a · τ · b · 0. We have s ↔rb t. However,
a a
6 . Thus f1 (s) ↔
we have f1 (s) −→ 0 while f1 (t) −→ 6 rb f1 (t). In this example the role
of the silent action τ in the definition of t is crucial. On one side, the capability
of performing τ is not discriminating in the evaluation of branching bisimulation
equivalence of processes (see Def. 6). Hence, processes b · 0 and τ · b · 0, which
are reached through action a by s and t, respectively, are branching bisimilar,
thus implying that s ↔rb t. On the other hand, action τ becomes relevant when
we focus on exact process evolution sequences. While process s can immediately
perform b after a, process t cannot, namely after performing a it has to do the
A Rule Format for Rooted Branching Bisimulation 55
action τ to reach a state in which it is able to perform b, and these two different
evolutions are discriminated by the premises of ρf1 . Our proposal is to permit
testing for an a move followed by a b move, provided that this comes together
with the testing for an arbitrary number of τ -moves between these two moves
labeled a and b. This means admitting the following set of rules in the TSS,
provided we introduce the constraint that the TSS contains all of them:
( a b
)
x1 −→ y1 y1 −→n y2 y2 −→ y3
a |n∈N
f1 (x1 ) −→ y3
Let τ n denote the sequence τ · . . . · τ of n actions τ , and sn ≡ a · τ n · b · 0 (notice
a
s ≡ s0 and t ≡ s1 ). We have that f1 (sn ) −→ 0 for all n ∈ N, thus implying that
f1 (sm ) ↔rb f1 (sn ) for all m, n ∈ N.
Constraint 2c in Def. 10 prohibits double testing, namely the ability of testing
for two (or more) moves by a source argument, for arguments labeled as wild.
An example of rule violating this constraint is the second of the rules below:
a a b
x1 −→ y1 x1 −→ y1 x1 −
→ y2
a a∈A c
f2 (x1 ) −→ f2 (y1 ) f2 (x1 ) −
→0
where the argument of f2 has to be wild due to constraint 2d of Def. 10 applied
to the first rule. Let us take processes s ≡ a · (a · 0 + b · 0) and t ≡ a · t0 , with t0
defined with the classical recursive construct as t0 ≡ a · 0 + τ · (b · 0 + τ · t0 ). We
a c a
have s ↔rb t. However, we have f2 (s) −→ f2 (a·0+b·0) − → 0 while f2 (t) −→ f2 (t0 )
and neither f2 (t0 ) nor any process reachable from f2 (t0 ) through any sequence of
τ -moves can make any c move. Thus f2 (s) ↔ 6 rb f2 (t). Here the processes a·0+b·0
and t0 , which are reached through action a by s and t, respectively, are branching
bisimilar. Their difference, sensed by the second rule for f2 , is that a · 0 + b · 0 can
perform both a and b, whereas t0 is not able to reach (through any sequence of τ
moves) any state in which both a and b are enabled, despite it can reach through
τ actions a state where a is enabled and another state where b is enabled. Our
proposal is to permit double testing for moves a and b, provided that these moves
may follow an arbitrary number of τ steps. This means admitting the following
set of rules in the TSS, provided we add the constraint that the TSS contains
all of them:
( a b
)
x1 −→m y1 y1 −→ y2 x1 − →n y3 y3 − → y4
c | m, n ∈ N
f2 (x1 ) −
→0
c c
→ 0 and f2 (t0 ) −
Notice that with these rules we get both f2 (a · 0 + b · 0) − → 0,
thus implying f2 (s) ↔rb f2 (t).
4 Congruence Format for Rooted Branching Bisimulation
As discussed in the previous section, lookahead and double testing can be admit-
ted in the RBB safe format of [9], provided that sets of rules testing for sequences
56 V. Castiglioni, R. Lanotte, S. Tini
of τ moves of different length are all introduced in the TSS. Below we introduce
the notion of meta transition rule, which denotes a set of transition rules that
test for the ability of performing sequences of τ moves of all possible lengths.
Definition 11 (Positive meta premise). A positive meta premise is an ex-
pression of the form
a
t =⇒−→ y
a
The meta premise t =⇒−→ y represents the set
a ε a
Jt =⇒−→ yK := {t −→n y 0 y 0 −→ y} | n ∈ N
a
of countable many sets of premises. Intuitively, t =⇒−→ y holds if there exists an
n ∈ N and a substitution σV such that σV (t) can reach a state able to perform
the action a through a sequence of n τ -actions.
Definition 12 (Meta transition rule). A meta transition rule, notation ρ̃,
is of the form
aj b
k l a
{tj −−→ yj | j ∈ J} {tk −−→
6 | k ∈ K} {zl =⇒−−→ yl | l ∈ L}
a
f (x1 , . . . , xr(f ) ) −→ t
with J, K, L at most countable sets of indexes, tj , tk , t ∈ T(Σ), aj , bk , al , a ∈ A,
yj , zl , yl ∈ V, f ∈ F , x1 , . . . , xr(f ) ∈ V, such that:
– the x1 , . . . , xr(f ) , the yj for j ∈ J and the yl for l ∈ L are all distinct
variables.
A meta transition rule ρ̃ like in Def. 12 represents the set Jρ̃K of all the transition
rules of the form
aj kb
{tj −−→ yj | j ∈ J} {tk −−→
6 | k ∈ K} {µl | l ∈ L}
a
f (x1 , . . . , xr(f ) ) −→ t
l a
such that µl ∈ Jzl =⇒−−→ yl K.
Definition 13 (Meta TSS). A meta TSS is a set of meta transition rules.
The meta TSS T represents the TSS JT K = ∪ρ̃∈T Jρ̃K. Clearly, JT K is a ntyft-TSS.
So all definitions of Section 2 directly lift to meta TSSs.
Now, we are able to extend the RBB safe format of [9] with lookahead and
double testing for running processes.
Definition 14 (Meta RBB safe TSS). A meta TSS T is called meta RBB
safe, with respect to a tame/wild labeling of arguments of function symbols in F ,
if each of its transition rules is
1. either a patience rule for a wild argument of a function symbol;
A Rule Format for Rooted Branching Bisimulation 57
2. or a meta transition rule ρ̃ of the form
aj b
k al
{tj −−→ yj | j ∈ J} {tk −−→
6 | k ∈ K} {zl =⇒−−→ yl | l ∈ L}
a
f (x1 , . . . , xr(f ) ) −→ t
with constraints:
(a) actions al , for l ∈ L, are in A r {τ }, namely they can not be action τ ;
S S
(b) if xi ∈ [ j∈J var(tj )∪ k∈K var(tk )] for i = 1, . . . , r(f ), then i is a tame
argument for f ;
S S
(c) no yj for j ∈ J and yl for l ∈ L occurs in [ j∈J var(tj ) ∪ k∈K var(tk )];
(d) variables xi for i wild argument of f , yj for j ∈ J and yl for l ∈ L may
occur only at w-nested positions in the target t.
Notice that Def. 14 admits lookahead, since for l ∈ L we may have that zl ≡ yj
for some j ∈ J or zl ≡ yl0 for some l0 ∈ L. Double testing for a wild argument i
of an operation f ∈ F is admitted since we may have zl ≡ zl0 ≡ xi for l, l0 ∈ L.
Let us remark that meta rules have been already used in [10], called GSOS
rules with lookahead, with the purpose of observing a partial form of lookahead,
namely a sequence of τ -moves followed by a non silent move.
Notice that in Def. 14 we do not need the constraint 2b of Def. 10, which
imposes that testing for a move by a wild argument for an operator f requires
that there is a patience rule for it. To explain the reason, let us take the operators
a b
x1 −→ y1 x1 −
→ y1
a b
f (x1 ) −→ g(y1 ) g(x1 ) −
→ g(y1 )
that do not respect Def. 10 since the patience rule for the argument of g is
missing, and processes a · b · 0 and a · τ · b · 0. We have a · b · 0 ↔rb a · τ · b · 0
a b
but f (a · b · 0) ↔
6 rb f (a · τ · b · 0) since f (a · b · 0) −→ g(b · 0) −
→ 0 whereby
a b
f (a · τ · b · 0) −→ g(τ · b · 0) −
→6 . Definition 10 requires the patience rule for the
τ b
argument of g, so g(τ ·b·0) −→ g(b·0) − → 0 and, therefore, f (a·b·0) ↔rb f (a·τ ·b·0).
By adopting the meta rules as in Def. 14, we can write
a b
x1 −→ y1 x1 =⇒−
→ y1
a b
f (x1 ) −→ g(y1 ) g(x1 ) −
→ g(y1 )
and the patience rule for the argument of g is no more needed, since we have
a b
→ 0 and, thus, f (a · b · 0) ↔rb f (a · τ · b · 0).
f (a · τ · b · 0) −→ g(τ · b · 0) −
Let us argue that all constraints in Def. 14 cannot be relaxed in any trivial
way. Firstly, let us show why, as in [9], some arguments of functions deserve a
special treatment. These arguments are labeled as wild. The special treatment
consists in constraints 2b and 2d in Def. 14.
58 V. Castiglioni, R. Lanotte, S. Tini
Example 1. Let us consider the transition rules
a a
x1 −→ y1 x1 −→ y1
a a
f (x1 ) −→ y1 g(x1 ) −→ f (y1 )
and processes a.τ.a.0 and a.a.0. We have a.τ.a.0 ↔rb a.a.0. However, we have
a a
g(a.τ.a.0) ↔ 6 rb g(a.a.0). In fact, g(a.τ.a.0) −→ f (τ.a.0) and g(a.a.0) −→ f (a.0),
a a
where f (τ.a.0) ↔ 6 bb f (a.0) since f (τ.a.0) −→
6 and f (a.0) −→ 0. The rule for g has
a
f (y1 ) as target, where y1 occurs in the target of the premise x1 −→ y1 . This
implies that it may happen that when the argument x1 of g is instantiated by
two processes p and p0 with p ↔rb p0 , we have that the argument y1 of f is
instantiated by two a-derivatives, q and q 0 respectively, such that q ↔bb q 0 but
q↔6 rb q 0 . Arguments of operators that may be instantiated with processes related
by ↔bb but not by ↔rb are labeled wild. This is exactly what is required by
constraint 2d in Def. 14. As required by constraint 2b in Def. 14, they cannot
a
be tested by premises of the form x −→ y since these premises are able to
discriminate them.
By next example, we show why meta premises cannot test for τ moves (con-
straint 2a, Def. 14).
Example 2. Let us consider the transition rules
a τ
x1 −→ y1 x1 =⇒−→ y1
a τ
g(x1 ) −→ f (y1 ) f (x1 ) −→ y1
We have a.τ.a.0 ↔rb a.a.0. However, g(a.τ.a.0) ↔ 6 rb g(a.a.0). In fact we have
a τ a a τ
g(a.τ.a.0) −→ f (τ.a.0) −→ a.0 −→ 0, whereby g(a.a.0) −→ f (a.0) −→6 .
By next example, we show why in meta premises we cannot have an arbitrary
term in the left side, and we only allow variable zl .
Example 3. Let us consider the transition rules
a a a
x1 −→ y1 g(x1 ) =⇒−→ y1 x1 −→ y1
a a a
g(x1 ) −→ y1 f (x1 ) −→ y1 h(x1 ) −→ f (y1 )
We have a.a.0 ↔rb a.τ.a.0. However, h(a.a.0) ↔ 6 rb h(a.τ.a.0). In fact we have
a a a a
h(a.a.0) −→ f (a.0) −→ 0, whereby h(a.τ.a.0) −→ f (τ.a.0) −→
6 .
By next example, we show why we cannot allow variables that are targets of
premises or meta premises to be source of classic premises (constraint 2c, Def.
14).
Example 4. Let us consider the transition rules
a a a a
x1 −→ y1 y1 −→ y2 x1 =⇒−→ y1 y1 −→ y2
a a
f (x1 ) −→ y2 g(x1 ) −→ y2
We have a.τ.a.0 ↔rb a.a.0. However, we have that f (a.τ.a.0) ↔6 rb f (a.a.0) since
a a
f (a.τ.a.0) −→6 while f (a.a.0) −→ 0. Analogously, g(a.τ.a.0) ↔6 rb g(a.a.0) since
a a
g(a.τ.a.0) −→6 while g(a.a.0) −→ 0.
A Rule Format for Rooted Branching Bisimulation 59
To prove the congruence result, we have to deal with well-founded rules.
Definition 15 (Well-foundedness). Let H be a set of premises and meta
premises. The variable dependency graph of H is a directed graph GH = (V, E)
given by:
S
– V = h∈H Var(h);
a a
– E = {hx, yi | t −→ y ∈ H and x ∈ Var(t) or x =⇒−→ y ∈ H}.
We say that H is well-founded if any backward chain of edges in GH is finite.
A meta transition rule ρ̃ is called well-founded if the set of all its premises and
meta premises is well-founded. A meta TSS is called well-founded if all its meta
transition rules are well-founded.
Theorem 2. If a complete and well-founded meta TSS T is meta RBB safe,
then the rooted branching bisimulation equivalence that it induces is a congru-
ence.
5 Conclusions
We considered the format of [9], which ensures the congruence property for
rooted branching bisimulation, we relaxed the constraints on the single rules by
allowing both double testing for wild arguments of operators and lookahead, at
the price of constraining these features to come together the testing for an arbi-
trary number of silent steps. We argued that this means introducing a constraint
on the form of the whole set of rules. Our idea can be naturally extended to the
formats in [10, 11].
An example of operator that is captured by our format and that is outside the
formats in [9–11] is the copying operator, originally proposed in [17] for languages
that do not consider silent actions, and defined in [11] by the following rules:
a l r
x1 −→ y1 x1 −
→ y1 x1 −→ y1
a a∈A s
cp(x1 ) −→ cp(y1 ) cp(x1 ) −→ cp(y1 ) k cp(y2 )
where l, r ∈ A are the left and right forking, respectively, s is the split action,
and k is the parallel composition operator. In [11] this operator is admitted in
the format thanks to the two-tiered approach to SOS proposed in [10, 11]. The
idea is to divide function symbols in F into two classes: principal operators and
abbreviations, where an abbreviation can be obtained by grouping together the
arguments of a principal operator. Proofs are given that abbreviations are syn-
tactic sugar and do not have to obey the syntactic restrictions of a congruence
format, provided they abbreviate principal operators that do so. This is an ad-
vantage since if a given equivalence is a congruence w.r.t. an operator f ∈ F that
is outside from a congruence format, one can find an operator f ∗ that is consid-
ered to be principal and abbreviated by f and that obeys the constraints of the
format. In [11] an operator for which cp is an abbreviation is provided that is
captured by the format. Here we do not need to search for such an abbreviation
since cp is already in the format.
60 V. Castiglioni, R. Lanotte, S. Tini
Acknowledgements We are grateful to Wan Fokkink for feedback on a preliminary
version of this paper.
References
1. Plotkin, G.: A structural approach to operational semantics. Report DAIMI FN-
19, Aarhus University (1981)
2. van Glabbeek, R.J.: The linear time - branching time spectrum. In: CONCUR
’90. Volume 458 of LNCS., Springer (1990) 278–297
3. van Glabbeek, R.J.: The linear time - branching time spectrum ii. In: CONCUR
’93. Volume 715 of LNCS., Springer (1993) 66–81
4. Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J.
Assoc. Comput. Mach. 32 (1985) 137–161
5. van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimula-
tion semantics. J. Assoc. Comput. Mach. 43(3) (1996) 555–600
6. de Simone, R.: Higher-level synchronising devices in meije-sccs. Theoret. Comput.
Sci. 37 (1985) 245–267
7. Aceto, L., Fokkink, W.J., Verhoef, C.: Structural operational semantics. In: Hand-
book of Process Algebra. Elsevier (2001) 197–292
8. Bloom, B.: Structural operational semantics for weak bisimulations. Theoret.
Comput. Sci. 146 (1995) 25–68
9. Fokkink, W.J.: Rooted branching bisimulation as a congruence. J. Comput. Syst.
Sci. 60(1) (2000) 13–37
10. van Glabbeek, R.J.: On cool congruence formats for weak bisimulations. Theoret.
Comput. Sci. 412(28) (2011) 3283–3302
11. Fokkink, W.J., van Glabbeek, R.J., de Wind, P.W.: Divide and congruence: From
decomposition of modal formulas to preservation of branching and η-bisimilarity.
Inf. Comput 214 (2012) 59–85
12. Groote, J.F.: Transition system specifications with negative premises. Theoret.
Comput. Sci. 118(2) (1993) 263–299
13. Przymusinski, T.C.: The well-founded semantics coincides with the three-valued
stable semantics. Fundam. Inform. 13(4) (1990) 445–463
14. Gelfond, M., Lifschitz, V.: The stable model semantics for logic programming. In:
5th Conference on Logic Programming, MIT Press (1988) 1070–1080
15. van Glabbeek, R.J.: The meaning of negative premises in transition system speci-
fications ii. In: ICALP’96. Volume 1099 of LNCS., Springer (1996) 502–513
16. Basten, T.: Branching bisimilarity is an equivalence indeed! Inform. Proc. Lett.
58(3) (1996) 141–147
17. Bloom, B., Istrail, S., Meyer, A.: Bisimulation can’t be traced. J. Assoc. Comput.
Mach. 42(1) (1995) 232–268