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