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 demanding than the original one. We demonstrate that this can be done by applying such an idea to a well established rule format ensuring the property of congruence for the rooted branching bisimulation equivalence.
Structural operational semantics [
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 de ned (see [
Since [
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]
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 di erent 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,
provided these are not too heavy. To demonstrate how this can be done, we consider
the format of [
The paper is organized as follows: in Section 2, we recall some base notions
on SOS, in Section 3 we recall the format of [
In this section we recall some de nitions that are standard in the SOS framework.
As usual, we assume that the abstract syntax of a process description language 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 2 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 variables. The set of -terms over W , notation T ( ; W ), is the least set satisfying: (i) W T ( ; W ), and (ii) if f 2 F and t1; ; tr(f) 2 T ( ; W ), then f (t1; ; tr(f)) 2 T ( ; W ). T ( ; ;) is the set of all closed terms, also called processes, and abbreviated as T ( ). T ( ; V) is the set of all open terms and abbreviated 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) = fxg and Var(f (t1; : : : ; tr(f))) = Sri(=f1) Var(ti).
In SOS framework, the semantic model is that of LTSs.
De nition 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. Following standard notation, we write t !a t0 for (t; a; t0) 2 !. This represents a computation step of kind a taking process t to process t0.
LTSs are built by means of transition systems speci cations, namely sets of
transition rules of the form cpornecmluissieosn . Here we assume that these rules are in
the ntyft-format [
De nition 2 (ntyft-rule, [
aj ftj
{ the x1; : : : ; xr(f) and the yj for j 2 J are all distinct variables. The expressions tj a!j yj (resp. tk b !k6 ) 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( ) = pprem( ) [ nprem( ). The expression f (x1; : : : ; xr(f)) !a 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 2 src( ), and term t is the target of , notation trgt( ). We denote the set of variables in by Var( ), free variables by free( ) = Var( ) n (fx1; : : : ; xr(f)g [ fyj j j 2 J g), and bound variables by bound( ) = Var( ) n free( ).
De nition 3 (ntyft-TSS, [
Assigning an LTS to a TSS having rules with negative premises is not trivial.
See [
An expression t !a t0 (resp. t !a6 ) is called a positive (resp. negative) literal where t; t0 2 T( ) and a 2 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 by V (f (t1; : : : ; tr(f))) = f ( V (t1); : : : ; V (tr(f))), to literals by V (t !a t0) = SV (2tVp)r(ecmo!(anc)( V))V( ()t.0)AancldoseVd(stub!b6sti)tu=tionVi(nts)ta n!b6ce, oafnad nttoyfnt-tryuflte-ruislecsalbleyd aV (clo)se=d ntyft-rule. We denote with H a closed ntyft-rule, and with N 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 N holds for P , denoted P j= N , i for each t !b6 2 N we have that t !b t0 62 P for any t0 2 T ( ).
De nition 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 nite, and the nodes are labeled by closed literals such that: { 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 2 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 j= 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 j= 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 [
De nition 5 (Complete TSS, [
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
Behavioral equivalence relations over processes are usually de ned 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
re exive and transitive closure of relation ! is denoted with !". Finally, let us
introduce notation t !"n t0 for n 2 N: we have t !"0 t0 if t t0 and t !"n+1 t0
if t ! t00 and t00 !"n t0 for some t00 2 T ( ). Hence, !"= Sn2N !"n.
De nition 6 (Branching bisimulation, [
A crucial property of process description languages to ensure compositional modelling and veri cation 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 2 F is a congruence. De nition 7 (Congruence). An equivalence relation R over T ( ) is a congruence if for all f 2 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 operator + de ned by rules x1x+1x2!a!ay1y1 and x1x+2x2!a!ay2y2 , which is o ered by most of process description languages in the literature. To remedy to this problem the rootedness condition is usually assumed.
De nition 8 (Rooted branching bisimulation). Take a three-valued stable model hC ; U i. A symmetric relation R over T ( ) is a rooted branching bisimulation with respect to C if whenever s R t and s !a s0 2 C we have t !a t0 2 C for t0 such that s0 $bb t0.
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 bisimulations over T ( ) is the greatest rooted branching bisimulation over T ( ), it is called rooted branching bisimilarity and it is denoted with $rb . Rooted branching bisimilarity is clearly an equivalence relation.
In the following we recall the rule format RBB-safe [
A patience rule for the i-th argument of a function symbol f 2 F is a ntyftrule of the form
xi ! yi f (x1; : : : ; xr(f)) ! f (x1; : : : ; xi 1; yi; xi+1; : : : ; xr(f))
Following [
De nition 9 (w-nested context, [
Theorem 1 (Rooted branching bisimulation as a congruence, [
In [
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: Let us consider processes s a b 0 and t a b 0. We have s $rb t. However, we have f1(s) !a 0 while f1(t) !a6 . Thus f1(s) $6rb f1(t). In this example the role of the silent action in the de nition 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 action to reach a state in which it is able to perform b, and these two di erent 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: ( x1 !a y1
y1 !n y2 f1(x1) !a y3 y2 !b y3 j n 2 N ) Let n denote the sequence : : : of n actions , and sn a n b 0 (notice s s0 and t s1). We have that f1(sn) !a 0 for all n 2 N, thus implying that f1(sm) $rb f1(sn) for all m; n 2 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: where the argument of f2 has to be wild due to constraint 2d of Def. 10 applied to the rst rule. Let us take processes s a (a 0 + b 0) and t a t0, with t0 de ned with the classical recursive construct as t0 a 0 + (b 0 + t0). We have s $rb t. However, we have f2(s) !a f2(a 0+b 0) !c 0 while f2(t) !a 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) $6rb 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 di erence, 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: ( x1 !m y1 y1 !a y2 x1 !n y3 y3 !b y4 f2(x1) !c 0 j m; n 2 N ) Notice that with these rules we get both f2(a 0 + b 0) !c 0 and f2(t0) !c 0, thus implying f2(s) $rb f2(t). 4
As discussed in the previous section, lookahead and double testing can be
admitted in the RBB safe format of [
t =) !a y The meta premise t =) !a y represents the set
a Jt =) ! yK :=
ft !"n y0 y0 !a yg j n 2 N of countable many sets of premises. Intuitively, t =) !a y holds if there exists an n 2 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.
De nition 12 (Meta transition rule). A meta transition rule, notation ~, is of the form ftj aj ftk with J; K; L at most countable sets of indexes, tj ; tk; t 2 T( ), aj ; bk; al; a 2 A, yj ; zl; yl 2 V, f 2 F , x1; : : : ; xr(f) 2 V, such that: { the x1; : : : ; xr(f), the yj for j 2 J and the yl for l 2 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 ftj ! yj j j 2 J g ftk bk !6 j k 2 Kg f l j l 2 Lg such that l 2 Jzl =) a!l ylK.
De nition 13 (Meta TSS). A meta TSS is a set of meta transition rules. The meta TSS T represents the TSS JT K = [~2T J ~K. Clearly, JT K is a ntyft-TSS. So all de nitions of Section 2 directly lift to meta TSSs.
Now, we are able to extend the RBB safe format of [
De nition 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; 2. or a meta transition rule ~ of the form ftj aj ftk
Notice that Def. 14 admits lookahead, since for l 2 L we may have that zl yj for some j 2 J or zl yl0 for some l0 2 L. Double testing for a wild argument i of an operation f 2 F is admitted since we may have zl zl0 xi for l; l0 2 L.
Let us remark that meta rules have been already used in [
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 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 but f (a b 0) $6rb f (a b 0) since f (a b 0) !a g(b 0) !b 0 whereby f (a b 0) !a g( b 0) !b6 . De nition 10 requires the patience rule for the argument of g, so g( b 0) ! g(b 0) !b 0 and, therefore, f (a b 0) $rb f (a By adopting the meta rules as in Def. 14, we can write b 0). f (x1) !a g(y1) and the patience rule for the argument of g is no more needed, since we have f (a b 0).
b 0) !b 0 and, thus, f (a b 0) $rb f (a
Let us argue that all constraints in Def. 14 cannot be relaxed in any trivial
way. Firstly, let us show why, as in [
By next example, we show why meta premises cannot test for straint 2a, Def. 14). moves (conExample 2. Let us consider the transition rules We have a: :a:0 $rb a:a:0. However, g(a: :a:0) $6rb g(a:a:0). In fact we have g(a: :a:0) !a f ( :a:0) ! a:0 !a 0, whereby g(a:a:0) !a 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 We have a:a:0 $rb a: :a:0. However, h(a:a:0) $6rb h(a: :a:0). In fact we have h(a:a:0) !a f (a:0) !a 0, whereby h(a: :a:0) !a f ( :a:0) !a6 .
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 We have a: :a:0 $rb a:a:0. However, we have that f (a: :a:0) $6rb f (a:a:0) since f (a: :a:0) !a6 while f (a:a:0) !a 0. Analogously, g(a: :a:0) $6rb g(a:a:0) since g(a: :a:0) !a6 while g(a:a:0) !a 0.
To prove the congruence result, we have to deal with well-founded rules. De nition 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: { V = Sh2H Var(h); { E = fhx; yi j t !a y 2 H and x 2 Var(t) or x =) !a y 2 Hg. We say that H is well-founded if any backward chain of edges in GH is nite. 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 congruence. 5
We considered the format of [
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 [