Isabel Pita

María Inés

Fernández Camacho

Formal Specification of the Kademlia and the Kad Routing Tables in Maude ⋆

Keywords: Kademlia, Kad, distributed specification, formal analysis, Maude, Real-Time Maude

Kad is the implementation by eMule and aMule of the Kademlia peer-to-peer distributed hash table protocol. Although it agrees with the basic behaviour of the protocol, there are some significant differences. This paper presents the specification of both the Kademlia and the Kad routing tables, using the specification language Maude. As far as we know, this is the first such a formal development. The routing tables present a dynamic behavior in the sense that they should be able to send messages to other peers and they should have a notion of time for raising events and detect no answered messages. Our main contribution is the integration of these dynamic aspects in the protocol specification.

Introduction

Distributed hash tables (DHTs) are designed to locate objects in distributed environments, like peer-to-peer (P2P) systems, without the need for a centralized server. There are a large number of existing DHTs proposals; the best known are: Chord [?], Pastry [?], CAN [?], and Kademlia [?]. However, only Kademlia has been implemented in P2P networks through the eMule [START_REF] Bakhshi | Verification of peer-to-peer algorithms: A case study[END_REF] and aMule2 clients. Kad is the name given to the implementation of Kademlia incorporated to eMule and aMule, and it shows important differences from the original. There are also two BitTorrent overlays that use Kademlia: one by Azureus clients [START_REF] Merz | Towards Verification of the Pastry Protocol using TLA+[END_REF] and one by many other clients including Mainline4 and BitComet [START_REF] Mysicka | Reverse Engineering of eMule. An analysis of the implementation of Kademlia in eMule[END_REF] .

Although the different DHTs have been extensively studied through theoretical simulations and analysis, there is a lack of formal specifications for all of them. Bakhshi and Gurov give in [?] a formal verification of Chord's stabilization algorithm using the π-calculus. Lately Lu, Merz, and Weidenbach [?] have modeled Pastry's core routing algorithms in the specification language TLA + . They consider the complete P2P network and focused their study on the lookup correctness property: the lookup message for a particular key is answered by at most one 'ready' node covering the key. The paper provides a detailed model of the network, the routing table and other Pastry structures, while abstract from an explicit notion of time. Periodic actions are performed non-deterministically. The TLA + model checker is used to check the model and illustrate some open issues related with the algorithm. Finally the TLA + theorem prover is been used to verify the correctness property.

There is a preliminary study of the Kademlia searching process protocol by the first author in [10], and a distributed specification of the protocol in [11]. Based on them, we have identified the need of a detailed study of the routing tables, where each peer stores contact information about others. This information is used in the network look-up process.

The original version of Kademlia differs from the real implementation made in Kad. A Kademlia routing table is a proper binary tree whose leaves are lists of at most k contacts, called k-buckets. A bucket is kept sorted by the time contacts were last seen, and is identified by the common prefix of the IDs it contains. Each bucket is responsible for a range of the node ID space. In fact, Kademlia routing table is a list of buckets. The bucket in the first level contains contacts whose first bit is the opposite to the first bit of the owner of the routing table, while he ID of the owner is in the range of the last bucket. Kademlia uses, when add the contact to the routing table, a tighter splitting rule where it is only allowed to split the bucket with common prefix equal to the one of the routing table owner. A KAD routing table is a left-balanced binary tree, and may be a complete tree up to level 4. The tree nodes are called routing zones, and the buckets, called now routing bins, are placed in the leaf nodes. Kad divides the table structure in levels and index (the horizontal distance in number of routing zones from the leftmost one on the same level) and uses the bitwise exclusive-or of the n-bit quantities (XOR) distance to the owner ID of the routing table, to store contacts in routing bins. Kad has a looser splitting rule that Kademlia, it allows to split a bin if its level is smaller than 4 or its index is smaller than 5, which results in more possible contacts. Kademlia has no specific actions to update its routing table periodically, checking for offline contacts only when inserting into full buckets, while KAD has actual maintenance tasks that run at set periods. Each peer has a creation and expiration time, and also a type has scale from 0 to 4. Type 4 means that the contact is rarely connected and will probably be eliminated at the next occasion.

In this paper we present our specification of the routing table in the formal language Maude, as well as some preliminary results on its properties. The Maude algebraic specification language, is based on rewriting logic [?]. It supports both equational and rewriting logic computations and offers simple and elegant time simulation resources. Since the specifications are directly executable, Maude can be used to prototype the systems as well as to prove properties of them.

Our specification includes features not previously modeled as sending messages to update the Kademlia routing table or raising events for populate and removing offline nodes in the Kad routing table. We have focused our work on the routing tables and abstract from the rest of the network. In order to model maintenance cycles, and eventually other effects of time on the system, we turn to the real time extension of Maude [?]. Our model should allow us to test some correctness properties such as: If there is an alive node in the network and there is space in the routing table, the node will be included in a certain period of time. We are also interested in checking the interleaving of actions that take place at different points in time, and prove consistency properties like: if two bins are consolidated, they do not split again until a certain period of time.

As far as we know there is no other formal specification of the Kademlia and Kad routing tables. Right now the best sources to understand both protocol details are the original paper on the Kademlia DHT and the source code of the Kad implementation. Thus our first contribution is the benefits of having a formal specification of a system that is being consulted by many developers. In addition, the formalization of the routing tables allows us to compare the original version of Kademlia with the real implementation made in Kad.

However, our main contribution is the integration of the dynamic aspects of the routing table in the full protocol specification. The specification includes the ability of the routing tables to send and receive messages autonomously from the node by using different levels of configurations. Detection of non-answered messages is done by assigning a timeout when sending the message and triggering the appropriate action when the time expires. The actions that are performed automatically in Kad periodically, like populate almost empty buckets or remove offline contacts from the buckets, are triggered when their time expires. These actions require having a notion of time defined in different parts of the routing table and allow us to study the interleaving of actions that take place at different points in time.

The structure of the paper is as follows: In Section ?? we give some notions about the Maude language and the Kademlia and Kad DHTs. Sections ?? and ?? present the specification of the Kademlia and the Kad networks respectively. Section ?? defines a Kad routing table and proves some properties about it. Finally Section ?? presents some conclusions and future work.

Preliminaries

We present in this section the basic notions about Maude, Kademlia, and Kad.

Maude

Maude [?] is a formal specification language based on rewriting logic. In Maude, the state of a system is formally specified as an algebraic data type by means of a membership equational specification. We define new types (by means of keyword sort(s)); subtype relations between types (subsort); operators (op) for building values of these types; equations (eq) that identify terms built with these operators; and membership axioms (mb) which specify terms as having a given sort.

Both equations and membership axioms may be conditional (ceq and cmb). Conditions, introduced by the keyword if can be either a single equation, a single membership, or a conjunction of equations and memberships using the binary conjunction connective /\. The equations can be ordinary equations (t = t'), matching equations (t := t'), or abbreviate Boolean equations (t).

The sorts connected by a subtype relationship are grouped into equivalence classes called Kinds. Kinds are implicitly associated with connected components of sorts and are considered as error supersorts. They are written by enclosing the name of one of the connected sorts in square brackets.

The dynamic behaviour of the system is specified by rewrite rules of the form t -→ t ′ if C, that describe the local, concurrent transitions of the system. That is, when a part of a system matches the pattern t and satisfies the condition C, it can be transformed into the corresponding instance of the pattern t ′ .

In object-oriented specifications, classes are declared with the syntax class C | a 1 :S 1 ,. . ., a n :S n , where C is the class name, a i is an attribute identifier, and S i is the sort of the values this attribute can have. An object is represented as a term < O : C | a 1 : v 1 , . . ., a n : v n > where O is the object's name, belonging to a set Oid of object identifiers, and the v i 's are the current values of its attributes. The order of the attributes in an object is irrelevant. Messages are defined by the user for each application (introduced with syntax msg).

In a concurrent object-oriented system the concurrent state, which is called a configuration, has the structure of a multiset made up of objects and messages that evolves by concurrent rewriting. The behaviour associated with the messages is specify by rules of the form:

m 1 . . . m k o 1 . . . o l -→ m ′ 1 . . . m ′ s o ′ 1 . . . o ′ t if C
where the m i are messages of type Msg, and the o i are objects, with their class and attributes. Objects that appear only in the lefthand side of the rule are removed from the configuration, and objects that appear only in the righthand side of the rule are added to the configuration. Regarding the attributes, the only object attributes made explicit in a rule are those relevant for that rule. Attributes mentioned only in the lefthand side of a rule are preserved unchanged, the original values of the attributes mentioned only on the righthand side do not matter, and all attributes not explicitly mentioned are left unchanged. We use Full Maude's object-oriented notation and conventions [?, Part II] throughout the whole paper.

The notion of time is specified by using the real time extension of Maude [?]. In the Real-Time Maude language, one can make explicit the way in which change in a system is dependent on time. The language provides two sorts: GlobalSystem and System to represent the whole system and the state of the system. The whole system is obtained from the state by the constructor {_} : System -> GlobalSystem .. The transitions of the system that are assumed to take zero time are specified over the System sort. The elapse of time in a system is modelled by the tick rule: l : {t} -→ {u} if C . Tick rules must only be applied on the system as a whole, i.e., on terms of sort GlobalSystem, to ensure that time advances uniformly in all parts of the system.

The time domain may be discrete or dense. In particular, we use the discrete time definition with natural numbers, that provides us with a sort Time such that subsort Nat < Time ., a sort extension with the infinite value: subsort Time < TimeInf ., and the infinite value: op INF : -> TimeInf .

Kademlia

Kademlia [?] is a P2P distributed hash table used by the peers to access files shared by other peers. In Kademlia both peers and files are identified with n-bit quantities, computed by a hash function. Information of shared files is kept in the peers with an ID close to the ID file, where the notion of distance between two IDs is defined as the bitwise exclusive-or of the n-bit quantities. Then, the lookup algorithm which is based on locating successively closer nodes to any desired key has O(log n) complexity.

Each node stores contact information about others in what is called its routing table. In Kademlia, every node keeps a list of: IP address, UDP port, and node ID, for nodes of distance between 2 i and 2 i+1 from itself, for i = 0, . . . , n and n the ID length. Note that each list contains IDs that differ in the ith bit. These lists, called k-buckets, have at most k elements, where k is chosen such that any given k nodes are very unlikely to leave the network within an hour of each other. Buckets are kept sorted by the time contacts were last seen.

The routing table is organized as a binary tree whose leaves are buckets. Each bucket is identified by the common prefix of the IDs it contains. The binary tree in the basic version of Kademlia is a list of buckets, since the only buckets that can be split are those with common prefix equal to the one of the routing table owner. Figure ?? (partially borrowed from [?]) shows a routing table for node 00000000.

Kademlia does not have explicit operations to maintain the information of the routing table. When a node receives any message (request or reply) from another node, it updates the appropriate bucket for the sender's node ID. If the sender node exists, it is moved to the tail of the list. If it does not exist and there is free space, it is inserted at the tail of the list. Otherwise, if the bucket has not free space, the node at the head of the list is contacted and if it fails to respond it is removed from the list and the new contact is added at the tail. In the case the node at the head of the list responds, if the bucket can be divided, it is split and the new contact added to the appropriate bucket; if the bucket cannot be divided the first contact is moved to the tail, and the new node is discarded.

The Kad Routing Table

Kad [?] is an implementation of the Kademlia distributed hash table. Its routing tables allow for more contacts than the Kademlia ones. They are not lists anymore, but left-balanced binary trees. The routing tree nodes are called routing zones. The buckets, now called routing bins are located at the leaf nodes and are lists of at most 10 contacts. Routing zones may be identified by their level and their zone index, that is the distance of the node to the leftmost node of its level. Kad has a looser splitting rule that Kademlia, it allows to split a bin if its level is smaller than 4 or its zone index is smaller than 5. Kad has explicit operations to maintain the information of the routing table, and does not rely on receiving messages as Kademlia. The process that adds new contacts to a bin is done once an hour. If the bin has less than three contacts or if splitting is allowed, the process selects a random ID from the bin ID space and starts a search for it. It will find new contacts that will be inserted into the bin. The process that deletes dead contacts from the bin is executed once a minute. It checks if the expire time of the first contact in the bin is ok. Every contact has an expire time variable which holds the time when the contact has to be checked whether it is still alive. If this time has expired, the routing table sends a HELLO-REQ message to the contact, increases a type variable, with values from 0 to 4, that indicates how long the contact has been online, and sets its expire time to 2 minutes. The process also removes all contacts of type 4 from the bin. If the node receives a HELLO-RES message indicating that the contact is alive, it places the contact at the end of the list, re-adjusts the type of the contact and sets a new expire time. If the contact does not reply, it will be removed from the bin when its type raises level 4.

Finally, there is a process that consolidates almost empty bins. It is done on adjacent bins that have the same parent routing zone if they both together have less than 5 contacts. It is run every 45 minutes on the whole routing tree.

The Maude Specification of Kademlia

Kademlia buckets are represented by the sort Bucket{X} as a list of contacts, where the contacts are parameters of the specification, represented by the sort X$Contact. The subsort NeBucket{X} represents non empty buckets.

sorts NeBucket{X} Bucket{X} . subsort NeBucket{X} < Bucket{X} . op empty-bucket : -> Bucket{X} [ctor] . op _!_ : Bucket{X} X$Contact -> [Bucket{X}] [ctor] .
Non-empty k-buckets are bounded and do not have repeated contacts by means of the membership axiom, where the bucketDim constant is set to k:

var T : X$Contact . var B : Bucket{X} . cmb B ! T : NeBucket{X} if length-b(B) < bucketDim /\ not T in B .
We have defined operations to perform all the bucket functions, like moving a contact to the tail, adding contacts, and removing contacts (see [?]).

Routing tables are defined as lists of buckets. We do not consider in this version of the specification the optimizations proposed in [?] that allow keeping more contacts in the routing table, therefore there is no need for a tree of buckets. Notice that routing tables have at least one bucket that cannot be empty. The following membership axiom sets when a list with more than one bucket is a routing table. It checks whether the table does not exceed the maximum size, that the contacts in each bucket are the appropriate and that at least one of the two last buckets is not empty. A single non-empty bucket is a routing table by the previous subsort relationship. op is-RT : [RoutingTable{X}] NzNat BitString -> Bool . eq [is-RT1] : is-RT(B1 !! B2,Nz,prefix) = fix-bucket?(B1,Nz,prefix) and fix-last-bucket?(B2,Nz,prefix) and (not empty-bucket?(B1) or not empty-bucket?(B2)) . eq [is-RT2] : is-RT(B1 !! (B2 !! KR),Nz,prefix) = fix-bucket?(B1,Nz,prefix) and is-RT(B2 !! KR,s Nz,prefix) . eq [is-RT3] : is-RT(B,Nz,prefix) = not empty-bucket?(B) .

We have defined operations to divide a bucket and to compute the nearest contact to a given one among others.

The operation that adds a contact to the routing table checks, when the bucket is full, if the first contact is still alive by sending it a PING message [?]. To encapsulate the behaviour of the routing table in the peer we define the RT attribute of the object Peer as a configuration of a routing table, a message, and a value of sort Time. By means of the rules RT-receive and RT-send the routing table messages are sent out from the peer and the reply messages go inside the routing table. Notice that the reply is captured by the routing table only when a message to that object has been sent before. The add-entry operation receives the contact to be added, the routing table and the contact of the routing table owner. The behaviour is as follows: equation add0 deals with the case in which the bucket is not full and the new entry is added at the tail. If the bucket is full, by rule add1 the routing table puts a PING message in the RT configuration, sets the time to the PT constant value, which represents the maximum time it will wait for a reply before consider the contact offline, and calls the auxiliary function add-entry2 on the routing table. If the first contact is offline, the time value of the configuration will raise zero and rule add2 will remove the offline contact and will add the new contact at the tail of the bucket by means of the add-entry-aux operation. Besides the message is removed from the configuration, and the time is set to the INF value. If the first contact replies, and the bucket is full and it cannot be divided (rule add3), the add-entry-aux operation moves the first contact to the tail of the bucket and discards the new contact. Finally if the bucket can be divided (rule add4), the entry is inserted again after splitting the bucket.

crl [add0] : { add-entry(Z1,R,Z2) + none + T } =>

{ add-entry-aux(Z1,R,1,Z2,true) + none + T } if not full-bucket?(find-bucket(Z1,R,1)) . crl [add1] : { add-entry(Z1,R,Z2) + none + INF } => { add-entry2(Z1,R,Z2) + PING(Z2,first-contact(find-bucket(Z1,R,1)),RPCRemove,1) + PT } if full-bucket?(find-bucket(Z1,R,1)) . rl [add2] : { add-entry2(Z1,R,Z2) + M + 0 } => { add-entry-aux(Z1,R,1,Z2,false) + none + INF } . crl [add3] : { add-entry2(Z1,R,Z2) + PING-REPLY(Z,Z2,T1,0) + T } => { add-entry-aux(Z1,R,1,Z2,true) + none + INF } if B1 := find-bucket(Z1,R,1) /\ equal(Z,first-contact(B1)) /\ full-bucket?(B1) /\ not isLastBucket?(B1,R) /\ T1 > 0 /\ T > 0 . crl [add4] : { add-entry2(Z1,R,Z2) + PING-REPLY(Z,Z2,T1,0) + T } => { add-entry(Z1,conc(R,div-bucket(last-bucket(R),Nz,NBit(Z2,Nz))),Z2) + none + INF } if B1 := find-bucket(Z1,R,1) /\ equal(Z,first-contact(B1)) /\ Nz := num-buckets(R) /\ full-bucket?(B1) /\ isLastBucket?(B1,R) /\ T1 > 0 /\ T > 0 .

The Kademlia specification is written in 7 modules and it defines about 60 operations over the defined sorts. It makes use of 6 rewriting rules to simulate the routing table interaction with the node. ( http://maude.sip.ucm.es/kademlia [?]) 4 Kad Processes in Maude.

The Kad processes responsible for the routing table maintenance are executed from periodically, instead of relying on the occurrence of an event as in the Kademlia routing table. For this reason time values are present all over the routing table specification, since contacts, bins, and the routing table must keep the time left to perform their actions.

We define the moment at which a process must occur with a constant value that is decreased as the time passes. When the value reaches zero the process is executed and the time is reset to the initial value. Time is expressed in seconds.

The Kad specification is written in 17 modules and it defines about 80 operations over the defined sorts. It makes use of 8 rewriting rules to simulate the routing table interaction with the node. ( http://maude.sip.ucm.es/kademlia [?])

The Kad Routing Table

The routing table representation in Kad differs from the one in Kademlia. Since Kad routing tables may be a complete tree up to level 4, the specification is no more a list of buckets, but a binary tree. Besides this, it is necessary to keep the time left for the processes to run.

Kad routing tables are non-empty binary trees of sort RoutingZone together with the contact information of the routing table owner and the time left to execute the consolidation process, which is performed on the whole tree. Routing bins are defined as lists of contacts of length K. Each contact, besides its identifier, IP address, and UDP port, keeps the time it has been active and the time remaining for checking whether it is still active. The time a contact has been active is the only time value that is increased time passes. The RoutingZone sort represents a Kad routing tree. Subtrees are represented in the Kind, since the level and zone index values of their leaves do not correspond to a complete tree. A subtree may only be one routing bin, together with its level, zone index, and the time to populate and to remove the offline contacts. Both processes are performed in each bin independently. The routing zone may also be the composition of its two subtrees together with the time to populate and the time to remove offline contacts. Kad uses the time to populate in the internal tree nodes during the consolidation process to define the population time for the new node that consolidates the two old ones. We maintain the time to remove offline contacts because it is in the Kad implementation, although it is not used in our specification. There is no need in the specification to maintain the level and zone index values in the internal tree nodes.

op rz : [RoutingZone] [RoutingZone] Time Time -> [RoutingZone] [ctor] .

A membership axiom defines which of the binary trees formed with the previous constructors are Kad routing trees. In particular it checks whether the routing bin (with its level, zone index, and time values) is the root of the tree, that is, if its level and zone index are both zero or if it is a tree with more than one bin that has the correct tree structure, and the appropriate contacts in each bin.

mb(rb(B,0,0,T1,T2)) : RoutingZone . cmb(rz(KR1,KR2,T1,T2)) : RoutingZone if is-subRT(0,0,rz(KR1,KR2,T1,T2)) /\ is-RT(rz(KR1,KR2,T1,T2)) .

A Kad Peer

The Kad routing table can request the node to send messages and start a lookingfor process. Therefore, the routing table specification needs to consider other parts of the node. In the specification a node/peer is an object of class Peer, with four attributes: the routing table, defined in Section ??; the search manager, which is a list of the keys the peer is looking for; a list of the messages to send; and a list of events, that simulates the list of events in the Kad implementation and is used to go over the bins looking for the process that its time to execute.

class Peer | CroutingTable : RoutingTable, CSearchManager : List{vKEY}, CMessages : MsgList, CEventMap : EventMap . subsort Kad-Contact < Oid .

The Passage of Time

The passage of time is defined by the functions delta and mte. The delta function spreads the passage of time to all time values of the specification as follows: if CF =/= none and CF' =/= none . eq delta(< Z1 : Peer | CroutingTable : RT, ... >,TC) = < Z1 : Peer | CroutingTable : delta(RT,TC), ... > . eq delta(rt(R,Z1,T2), TC) = rt(delta(R,TC),Z1,T2 monus TC) . eq delta(rb(B,N1,N2,T1,T2),TC) = rb(delta(B,TC),N1,N2,T1 monus TC,T2 monus TC) . eq delta(rz(KR1,KR2,T1,T2),TC) = rz(delta(KR1,TC),delta(KR2,TC),T1 monus TC,T2 monus TC) . eq delta(empty-bin,TC) = empty-bin . eq delta(B ! c(S,ip,udp,CT,T1,T2),TC) = delta(B,TC) ! c(S,ip,udp,CT,T1 plus TC,T2 monus TC) .

while the mte function computes the time that passes in each step as the minimum of all the time values in the system. op minTime : RoutingTable -> Time . op minTime : RoutingZone -> Time . eq minTime(rt(R,Z2,T2)) = min(minTime(R),T2) . eq minTime(rb(B,N1,N2,T1,T2)) = min(T1,T2) . eq minTime(rz(KR1,KR2,T1,T2)) = min(minTime(KR1),minTime(KR2)) .

The time values of the internal nodes that appear in the last equation are not taken into account in the minimum time computation, because they are not directly associated with any process.

The Populate Process

The population process is done in each routing bin when the time defined by the constant POPULATE-TIME-BIG in each routing bin reaches zero and the number of contacts in the bin is less than 20% of the bin size, or it is a bin that can be split. It is also required to be this the next bin in the event map attribute of the node. The process adds a random contact to the search process; and resets the population time of the bin. where:

-changePop changes the population time of the bin to the given value.

append(L, randomKey(N1,N2)) appends a new look-up for a random key value to the search manager. -timePop checks whether the time to populate in the bin is set to zero.

-getNumContacts obtains the number of contacts of a bin.

-getRZ gets the routing zone of a level and zone index.

The Remove Offline Contacts Process

The remove offline contacts process is done in each routing bin when the time defined by the constant NEXT-REM in each routing bin reaches zero.

Kad classifies contacts in five groups: type 0: very good contact, known for at least two hours; types 1 and 2: less good contact; type 3: newly inserted contact; type 4: the contact has not responded and will be removed in the next process. In addition each contact keeps two time values: the creation time, which is the time to determine how long the contact has been known, and the expire time, which is the time to check if the contact is still alive.

The process checks the first contact of the bin. If its expire time is not zero, the process removes type 4 contacts from the bin; push to the bottom the first contact (by the operation changeRem1); and puts a new remove time in the bin. where the rem4 operation removes all contacts with type 4 in the bin.

If the expire time of the first contact in the bin is zero, the process: removes type 4 contacts from the bin; increases the first contact type; puts the expire time of the first contact to 2 minutes (OFFLINE-CHECK constant) by means of the changeRem2 operation; and sends a HELLO-REQ message to the first contact. If the first contact answers, it will be moved to the tail of the bin, in other case it will be declared of type 4 and removed from the routing table in 2 minutes.

The Consolidation Process

The consolidation process is done in the routing tree when its time defined by the constant CONSOLIDATE-TIME of the routing table, reaches zero. The consolidation of a routing tree, done by the consolidate function is a recursive process. The first equation: con1 defines the case of a subtree with one bin, which cannot be consolidated. The equation con2 defines the recursive case when at most one of the subtrees is a leaf. Equations con3 and con4 define the cases where the two subtrees are leaves. If the number of contacts of the two bins is less than half the size of the bin, bins are aggregated (con3). Otherwise no consolidation is needed for these bins (con4).

eq [con1] : consolidate(rb(B,N1,N2,T1,T2)) = rb(B,N1,N2,T1,T2) . ceq [con2] : consolidate(rz(KR1,KR2,T1,T2)) = rz(consolidate(KR1),consolidate(KR2),T1,T2) if not isLeaf?(KR1) or not isLeaf?(KR2) . ceq [con3] : consolidate(rz(rb(B1,N3,N4,T1,T2),rb(B2,N3,N6,T3,T4),T5,T6)) = rb(add-bins(B1,B2),sd(N3,1),N4 quo 2,POPULATE-TIME,T6) if getNumContacts(rz(rb(B1,N3,N4,T1,T2),rb(B2,N3,N6,T3,T4),T5,T6)) < K quo 2 /\ N6 == N4 + 1 . ceq [con4] : consolidate(rz(KR1,KR2,T5,T6)) = rz(KR1,KR2,T5,T6) if isLeaf?(KR1) /\ isLeaf?(KR2) /\ getNumContacts(rz(KR1,KR2,T5,T6)) >= K quo 2 .

Case Study

We define a routing table with 4 levels and 26 contacts over 7 routing bins (Figure ??). The maximum number of contacts in a bin is set to 10. Node IDs are abbreviated to 8 bits. Contacts are of different types, from 0 to 4 and we consider realistic time values for the different process. The specification, initial terms and results of each case study can be found in http://maude.sip.ucm.es/kademlia. The owner of the routing table is supposed to have the ID 01110000. The contacts of the routing bin at level 3 and zone index 0, that are shown below, are at distance less or equal to 31 from the owner ID. This means that the three most significant bits of the contacts in the bin should agree with the ones of the routing table owner.

rz(rb(empty-bin ! c(0 ; 1 ; 1 ; 1 ; 1 ; 0 ; 1 ; 0,ip,udp,type0,40000,7200) ! c(0 ; 1 ; 1 ; 0 ; 0 ; 0 ; 1 ; 0,ip,udp,type1,30000,5400) ! c(0 ; 1 ; 1 ; 0 ; 1 ; 0 ; 1 ; 0,ip,udp,type4,15000,60) ! c(0 ; 1 ; 1 ; 1 ; 0 ; 0 ; 1 ; 1,ip,udp,type2,20000,3600) ! c(0 ; 1 ; 1 ; 1 ; 1 ; 1 ; 0 ; 1,ip,udp,type3,0,1) ! c(0 ; 1 ; 1 ; 0 ; 1 ; 0 ; 0 ; 1,ip,udp,type3,0,1),3,0,3000,48) There are two contacts of type 3 and one contact for types 0, 1, 2, and 4. The last two contacts have just joined the network since their creation time is set to 0 and their expire time is set to 1 second. The expire time of the first four contacts varies from 1 minute to 2 hours. The population time of the bin is set to 50 minutes and its time to remove offline contacts to 48 seconds. Now, we can explore, for example, the shortest and the longest time it takes to reach a desired state using the find earliest and find latest commands of real-time Maude.

The syntax of these commands is as follows:

( where:

-initState is a real-time system of sort GlobalSystem. Values are obtained by enclosing a system, in our specification a configuration of objects and messages, between brackets. -searchPattern is the description of the global system we are looking for.

For example, we are interested in the maximum time a type 4 contact will be in the table. Thus, we obtain the time it takes to remove all type 4 contacts from the initial configuration. The property is important since having offline contacts in the table prevent new contacts to access it, limiting the chances of finding information.

We execute the command:

(find earliest { < c(0 ; 1 ; 1 ; 1 ; 0 ; 0 ; 0 ; 0,ip,udp,type0,68760,5400) : Peer | CroutingTable : RT1, CSearchManager : nil , CEventMap : (< 3 ; 0 > < 4 ; 2 > < 4 ; 3 > < 2 ; 1 > < 2 ; 2 > < 3 ; 6 > < 3 ; 7 > < 0 ; 0 > , CMessages : nilMsgL > } =>* C:Configuration} such that (num-type4(C:Configuration) == 0) .)

where the num-type4 operation computes the number of contacts of type 4 in a routing table.

The find earliest command explores in parallel all possible executions from the given configuration until one of them reaches a configuration that fulfills the given conditions. This means, that all the actions that can take place in the given configuration will be explored. In particular, type 4 contacts are removed from a bin when the time to execute the remove offline process is reached.

The result includes the reached configuration and the time it takes to obtain it. As we are interested only in the time value, we do not show the value of the node attributes.

Result: {< c(0 ; 1 ; 1 ; 1 ; 0 ; 0 ; 0 ; 0,ip,udp,type0,68760,5400): Peer | CEventMap : ..., CMessages : ..., CroutingTable : ...>} in time 48

Notice that, in this example, we have changed the OFFLINE-CHECK constant value to a big number to prevent the remove offline contacts process from generating new type 4 contacts.

Conclusions and Ongoing Work

We have developed a formal specification of the Kademlia and the Kad routing tables that can be used by other system developers to use or update their DHTs. The specification includes a notion of time that allows for triggering events and detecting messages timeouts.

The specification will allow us to verify properties of the protocol. In particular properties that include time aspects, like the ones mentioned in the introduction. In this paper we have shown how to obtain the time it takes to remove offline contacts from a table. Similar properties, that will ease us the study of the behavior of the routing table are, for example to obtain the time it will take to execute the next populate process, or which will be the next bin to be populate, under different conditions.

As future work we plan to complete the study of the behavior of the routing table as time goes on, specially on the aspects related with the routing table correctness and the order in which the processes take place. We would also like to integrate the routing table specifications in a distributed system specification using the Maude sockets, and introduce the strategy language of Maude to control the execution of Kad processes.

Fig. 1 .

 1 Fig. 1. Kademlia and Kad Routing table structures.

  Figure ?? shows a Kad routing table.

  sort RoutingTable{X} . subsort NeBucket{X} < RoutingTable{X} . op _!!_ : Bucket{X} [RoutingTable{X}] -> [RoutingTable{X}] [ctor] .

  var KR :[RoutingTable{X}] .vars B B1 B2 : Bucket{X} . cmb KR : RoutingTable{X} if num-buckets(KR) > 1 /\ num-buckets(KR) <= length(give-contact(KR)) /\ atLeastOne?(KR) /\ is-RT(KR,1,peer-prefix(KR)) .

op

  Peer : -> Cid . op RT :_ : Configuration -> Attribute [ctor] . op {_+_+_} : RoutingTable{X} Msg TimeInf -> Configuration [ctor] . var R : RoutingTable{X} . var P : Oid . vars Z1 Z2 : X$Contact . vars T1 T2 T3 T4 : Time . var T : TimeInf . rl [RT-send] : < P : Peer | RT : { R + PING(Z1,Z2,T1,T2) + INF } > => PING(Z1,Z2,T1,T2) < P : Peer | RT : { R + PING(Z1,Z2,T1,T2) + T1 } > . crl [RT-receive] : PING-REPLY(Z1,Z2,T1,T2) < P : Peer | RT : { R + PING(Z2,Z1,T3,T4) + T } > => < P : Peer | RT : { R + PING-REPLY(Z1,Z2,T1,T2) + T } > if T =/= INF .

  sort RoutingTable . op rt : RoutingZone Kad-Contact Time -> RoutingTable [ctor] .

sorts

  NeRoutingBin RoutingBin . subsort NeRoutingBin < RoutingBin . op empty-bin : -> RoutingBin [ctor] . op _!_ : RoutingBin Kad-Contact -> [NeRoutingBin] [ctor] . var T : Kad-Contact . var B : RoutingBin . cmb B ! T : NeRoutingBin if getSize(B) < K /\ not T in B .

  sort Kad-Contact . op c : BitString128 IP UDP Contact-types Time Time -> Kad-Contact [ctor] .

  op rb : RoutingBin Nat Nat Time Time -> [RoutingZone] [ctor] .

  op delta : Configuration Time -> Configuration [frozen (1)] . op delta : RoutingTable Time -> RoutingTable . op delta : RoutingZone Time -> RoutingZone . op delta : RoutingBin Time -> RoutingBin . vars CF CF' : Configuration . vars T T1 T2 TC : Time . var Z1 : Kad-Contact . var R : RoutingZone . var B : RoutingBin . vars KR1 KR2 : [RoutingZone] . var : RT : RoutingTable . var S : BitString128 . var ip : IP . var udp : UDP . var CT : Contact-types . vars N1 N2 : Nat . eq delta(none,T) = none . ceq delta(CF CF', T) = delta(CF,T) delta(CF',T)

  op mte : Configuration -> TimeInf [frozen (1)] . eq mte(none) = INF . ceq mte(CF CF') = min(mte(CF), mte(CF')) if CF =/= none and CF' =/= none . eq mte(< Z1 : Peer | CroutingTable : RT ,...>) = minTime(RT) .

  crl [populate1] : < Z : Peer | CroutingTable : rt(R1,Z2,T2), CSearchManager : L , CEventMap : (< N1 ; N2 > EM) , ...> => < Z : Peer | CroutingTable : rt(changePop(R1,N1,N2,POPULATE-TIME-BIG),Z2,T2) , CSearchManager : append(L, randomKey(N1,N2)) , CEventMap : (EM < N1 ; N2 >) , ... > if (N1 =/= 0 or N2 =/= 0) /\ timePop(R1,N1,N2) /\ (N2 < KK or N1 < KBASE or getNumContacts(getRZ(R1,< N1 ; N2 >)) <= (K * 2) quo 10 ) .

  crl [del-dead1] : < Z : Peer | CroutingTable : rt(R1,Z2,T2), CEventMap : < N1 ; N2 > EM ,. > => < Z : Peer | CroutingTable : rt(changeRem1(R1,N1,N2),Z2,T2), CEventMap : EM < N1 ; N2 > ,...> if (N1 =/= 0 or N2 =/= 0) /\ timeRem(R1,N1,N2) == 1 . eq [cr11] : changeRem1(rb(B1,N3,N4,T1,T2),N1,N2) = rb(pushToBottom(first-contact(rem4(B1)),rem4(B1)),N3,N4,T1,NEXT-REM) . ceq [cr12] : changeRem1(rz(KR1,KR2,T5,T6),N1,N2) = rz(changeRem1(KR1,sd(N1,1),N2),KR2,T5,T6) if 2 ^sd(N1,1) > N2 . ceq [cr13] : changeRem1(rz(KR1,KR2,T5,T6),N1,N2) = rz(KR1,changeRem1(KR2,sd(N1,1),sd(N2,2 ^sd(N1,1))),T5,T6) if 2 ^sd(N1,1) <= N2 .

  crl [del-dead2] :< Z : Peer | CroutingTable : rt(R1,Z2,T2), CMessages : LM , CEventMap : (< N1 ; N2 > EM) ,... > => < Z : Peer | CroutingTable : rt(changeRem2(R1,N1,N2),Z2,T2) , CMessages : append(LM, HELLO-REQ(Z2,first-contact-bucket(R1,N1,N2),T2,1)) , CEventMap : EM < N1 ; N2 >,...> if (N1 =/= 0 or N2 =/= 0) /\ timeRem(R1,N1,N2) == 2 . eq [cr21] : changeRem2(rb(B1,N3,N4,T1,T2),N1,N2) = rb(change-first(rem4(B1),OFFLINE-CHECK),N3,N4,T1,NEXT-REM) . op changeRem2 : RoutingZone Nat Nat -> RoutingZone . ceq [cr22] : changeRem2(rz(KR1,KR2,T5,T6),N1,N2) = rz(changeRem2(KR1,sd(N1,1),N2),KR2,T5,T6) if 2 ^sd(N1,1) > N2 . ceq [cr23] : changeRem2(rz(KR1,KR2,T5,T6),N1,N2) = rz(KR1,changeRem2(KR2,sd(N1,1),sd(N2,2 ^sd(N1,1))),T5,T6) if 2 ^sd(N1,1) <= N2 .

  rl [consolidate1] : < Z : Peer | CroutingTable : rt(R,Z2,0), ... > => < Z : Peer | CroutingTable : rt(consolidate(R),Z2,CONSOLIDATE-TIME),.. > .

Fig. 2 .

 2 Fig. 2. Routing tree example.

http://www.amule.org

http://azureus.sourceforge.net

http://www.bittorrent.com

http://www.bitcomet.com

⋆ Research supported by MEC Spanish project DESAFIOS10 (TIN2009-14599-C03-01) and Comunidad de Madrid program PROMETIDOS (S2009/TIC1465). 1 http://www.emule-project.net


David Romero Hernández

David De Frutos
email: defrutos@sip.ucm.es

Escrig Dpto

Distances Between Processes: a Pure Algebraic Approach ⋆

Recently, we have presented operational and denotational definitions for distances between processes corresponding to any semantics in the ltbt-spectrum. In this paper, we develop a general algebraic framework to define distances between terms from any arbitrary signature. We apply this framework obtaining a new algebraic characterization of our previous distances. Moreover, we prove the generality of our approach developing an algebraic characterization of the distances based on the (bi)simulation game by other authors.

Introduction

In order to define an (abstract) semantics for processes, we need just to define an adequate equivalence relation, ≡, relating the processes in some universe, P roc. Then, the values of this semantics are just the corresponding equivalence classes, and two processes have the same semantics if and only if they are equivalent. Once we have fixed such a semantics we can compare two processes, but the output of this comparison is just a Boolean value. In particular, when two processes are not equivalent, we do not have a general way to measure "how far away" they are from being equivalent.

There are several papers which introduce several distances between processes based on the (bi)simulation game -see e.g. [START_REF] Chen | Game characterizations of process equivalences[END_REF][START_REF] Fahrenberg | The quantitative linear-timebranching-time spectrum[END_REF]-. Even before, Ying and Wirsing studied approximate bisimilarity, following similar but simpler ideas [START_REF] Ying | Approximate bisimilarity[END_REF][START_REF] Ying | Topology in process calculus -approximate correctness and infinite evolution of concurrent programs[END_REF]. Our work started by considering those distance games, where one essentially plays the (bi)simulation game, but with the "defender" having the possibility of replying a move of the "attacker" without matching exactly his move. In such a case, he should pay to the attacker some quantity, depending on the mismatch (distance) between the two involved actions.

It is well-known the use of equivalence relations to formalize the notion of implementation: a process implements some specification (given by another process) when they are equivalent w.r.t. the adequate semantics. But, if we follow this approach, we have no flexibility at all: our process has to satisfy in a precise way all the constraints imposed by the specification, or it will not be a correct implementation. Instead, in the real world, we often find other more flexible quality requirements, where the specification establishes the ideal behavior of the system, but some (limited) deviations from it are allowed, without invalidating the adequateness of the implementation.

We need a notion of distance between processes to make precise how far away two processes are from being equivalent w.r.t. some given semantics. It is true that metrics have been used for a long time to formalize the semantics of infinite processes, by means of (the limit of) those of their finite approximations. But these metrics were just a very particular case that only cared for "the first" disagreement between the compared processes. Instead, now we look for more general distances, which moreover should be applicable to any syntactic process algebra (i.e., to any signature Σ) and any semantics (based, for instance, on the axiomatization of the desired semantics).

We have already introduced the basic operational ideas of our approach in [START_REF] Romero-Hernández | Defining distances for all process semantics[END_REF]. It is true that the most flexible way to capture a semantics for processes, L, is based on the use of an adequate preorder ⊆ L , and not just an equivalence relation ≡ L .

However, we prefer to start our presentation in Section 2 using just the better known equational calculus. Next, in Section 3 we will see that a simple modification of the proof system defining the classical equational calculus (see e.g. [START_REF] Hennessy | Algebraic theory of processes[END_REF]), produces a general algebraic framework to define distances between processes w.r.t. any semantics. In particular, in Section 4 we study in detail the case of the bisimulation semantics. Later, in Section 5, we will see how we can easily generalize all our algebraic presentation to the inequational framework. Moreover, we define our distances for the rest of the semantics in the ltbt-spectrum. To show the flexibility of our approach, in Section 6 we see how the classic distances based on the (bi)simulation game, can be also defined in our algebraic framework. We conclude with our conclusions and some future work.

Preliminaries

A careful presentation of the equational calculus with application to the (testing) semantics of processes can be found in [START_REF] Hennessy | Algebraic theory of processes[END_REF]. Next, we will only remind the definitions of the main concepts needed to develop that theory. Definition 1. 1. A signature, Σ, is a set of formal functional symbols. Each functional symbol has associated a natural number which is its arity. We use Σ n to denote the set of symbols in Σ of arity n. 2. If Σ is a signature, a Σ-algebra is a pair A, Σ A where A is a set, the domain or support of the algebra, and Σ A is a set of internal functions. A Σ-algebra is simply an interpretation of each operation in Σ, respecting of course its arity. 3. There is a particularly important Σ-algebra, called the term algebra for Σ, and denoted by T Σ , whose support is the set of terms freely generated by Σ.

Some particular collections of Σ-algebras can be singled out by means of equations. An equation is determined by a pair of terms which may contain variables. We consider an (arbitrary) set of variables, X, and the set of terms with variables T Σ (X) . T Σ (X) can be obtained by extending the signature Σ adding these variables with null arity. In fact T Σ (X) is just an algebra, where Σ(X) is the classic notation for the signature Σ ∪ X which add to Σ each x ∈ X as a new function symbol of arity 0.

Given an equation t ≡ t ′ with t, t ′ ∈ T Σ (X), we say that a Σ-algebra A, Σ A satisfies it, when the values of both t and t ′ under any valuation, which assigns values in A to the variables x ∈ X, are the same. Given a set of equations E, C(E), is the class of Σ-algebras satisfying the equations E. The initial algebra of C(E) can be presented as a quotient algebra T Σ / ≡ E for some particular congruence ≡ E . We can obtain this congruence by means of the equational deduction system DED(E ) in Fig. 1 whereby the equations in E may be used to derive statements of the form t ≡ t ′ , with t, t ′ ∈ T Σ .

1. Reflexivity t ≡ t 2. Symmetry t ≡ t ′ t ′ ≡ t 3. Transitivity t ≡ t ′ t ′ ≡ t ′′ t ≡ t ′′ 4. Substitution t1 ≡ t ′ 1 , . . . , t k ≡ t ′ k f (t1, . . . , t k ) ≡ f (t ′ 1 , . . . , t ′ k )
for every f ∈ Σ of arity k.

5. Instantiation t ≡ t ′ tρ ≡ t ′ ρ for every substitution ρ.

6. Equations t ≡ t ′ for every equation t, t ′ ∈ E Fig. 1. The proof system DED(E ) in [START_REF] Hennessy | Algebraic theory of processes[END_REF] We write ⊢ E t ≡ t ′ if we can derive t ≡ t ′ ; and then, we say that t ≡ t ′ is a theorem of DED(E ). Obviously, we can see each derivable theorem as the pair of a relation ≡ E , which due to 1-3 is an equivalence relation, and as a result of 4 a Σ-congruence.

As we have said, the idea in this paper is to define distance between processes. Then, we need to extend the concept of Σ-algebra with a notion of distance. This distance allows us to measure how far away is a process p of being equivalent to another process q.

In [START_REF] Romero-Hernández | Defining distances for all process semantics[END_REF] we have considered as processes the terms generated by the free (0, Act, +)algebra, which correspond to the classic domain of BCCSP (Act) processes. Definition 2. Given a set of actions Act, the set BCCSP (Act) of processes is that defined by the BNF-grammar: p ::= 0 | ap | p + q. The very well known operational semantics of BCCSP [START_REF] Van Glabbeek | The linear time-branching time spectrum I: the semantics of concrete, sequential processes[END_REF][START_REF] De Frutos-Escrig | On the unification of process semantics: equational semantics[END_REF] is defined by:

(1) ap a → p (2) p a → p ′ p + q a → p ′ (3) q a → q ′ p + q a → q ′
Based on this operational semantics we can define all the semantics in the ltbt-spectrum [START_REF] Van Glabbeek | The linear time-branching time spectrum I: the semantics of concrete, sequential processes[END_REF]. In particular, we have studied the case of the finest of these semantics, that is the bisimulation semantics.

Definition 3 (Bisimulation).

A bisimulation between processes is a relation B such that, whenever pBq, we have:

• for every a ∈ Act, if p a → p ′ there exists some q ′ , with q a → q ′ and p ′ Bq ′ .

• for every a ∈ Act, if q a → q ′ there exists some p ′ , with p a → p ′ and p ′ Bq ′ .

We have defined distances between processes corresponding to any semantics defined by a preorder ⊆ L , this covering in particular the case of equivalence relations, such as bisimulation . Both are defined in an operational way based on transformations between processes, and in a denotational way, using SOS-rules. Next, we recall this second definition Definition 4 ( [START_REF] Romero-Hernández | Defining distances for all process semantics[END_REF]). Given a semantics L, defined by a preorder ⊆ L , coarser than bisimulation, we say that a process q is at distance at most m ∈ N of being better than some other p, w.r.t. the semantics L and the distance between actions d, and then we write d L d (p, q) ≤ n, if we can infer p ⊑ L n q, by applying the following rules:

(1) p ⊆ L q p ⊑ L n q (2) p ⊑ L n q ap ⊑ L n+d(b,a) bq (3) p ⊑ L n p ′ p + q ⊑ L n p ′ + q (4) p ⊑ L n q q ⊑ L n ′ r p ⊑ L n+n ′ r
For instance, for the bisimulation semantics, we have ∼ in the place of ⊆ L and we simply write = d for the obtained collection of distance relations, that in this case are all symmetric.

The rest of the paper is devoted to the development of a pure algebraic framework that allows us to define those distances in an algebraic way. Once we have it, we could use all the algebraic techniques and general results from the area, on the study of those distance relations.

From algebraic semantics to algebraic distances

We will see in this section how the basic concepts appearing in the definition of algebraic semantics can be adequately modified in a natural way to obtain an algebraic theory of distances between processes. It can be used to get algebraic characterizations of all the distances previously presented in [START_REF] Romero-Hernández | Defining distances for all process semantics[END_REF].

We start with the notion of Σ-algebra with distances, whose definition will be a resetting of the definition of quotient Σ-algebra.

. f ∈ Σ, ar(f ) = k, a i ≡ di b i for all i ∈ 1..k ⇒ f (a) ≡∼ f (d1,...,d k ) f (b),
where ∼ f is a function associated to f that combines the distances between the components of its arguments and satisfies ∼ f (0) = 0.

Remark 1. In the previous definition we have only directly stated reflexivity of ≡ 0 in (1). However, applying these rules we can infer (1 ′ ) a ≡ d a for all a ∈ A and all d ∈ D, by combining (1) and (3). Another possibility is to take (1 ′ ) instead of (1), and then by combining it with (4), we get the monotonicity rule (3), which therefore could be removed.

Let us discuss and justify one by one all the ingredients of Def. 5. We have introduced a collection of relations ≡ d , that intuitively describe the balls of radius d of the topology induced by our distance notion. The classical properties of distances correspond to 1-4. Note how the transitivity of equivalence relations is substituted by the triangular inequality 4.

We have said that we are generalizing the notion of quotient algebra, and not just that of (plain) algebra, because we allow that ≡ 0 will be any Σ-congruence, and not just the equality relation. Note that in that particular case the triangular inequality becomes transitivity, because 0 + 0 = 0, and then ≡ 0 has to be first an equivalence relation, but also a Σ-congruence, by applying 5.

We have preferred to be quite general w.r.t. the constraints imposed to the combination functions ∼ f . Certainly ∼ f = + for all f ∈ Σ, will be the most interesting case. In Section 6 we will see how taking ∼ f = max, we obtain the algebraic characterization of other noticeable distances. Now we can get our deduction systems for distances, dDED(E D ), by resetting the clauses that define DED(E ), again in a very natural way. Definition 6. A deduction system for distances, dDED( E D ), between terms in T Σ (X), is a collection of rules including:

1. Reflexivity: t ≡ d t. 2. Symmetry: t ≡ d t ′ ⇒ t ′ ≡ d t. 3. Triangular transitivity: t ≡ d t ′ , t ′ ≡ d ′ t ′′ ⇒ t ≡ d+d ′ t ′′ . 4. Substitution: t 1 ≡ d1 t ′ 1 , . . . , t k ≡ d k t ′ k ⇒ f (t 1 , . . . , t k ) ≡∼ f (d1,...,d k ) f (t ′ 1 , . . . , t ′ k )
for every f ∈ Σ of arity k and the corresponding ∼ f composing distances. 5. Instantiation: t ≡ d t ′ ⇒ tρ ≡ d t ′ ρ, for every substitution ρ.

A set of distance equations E

D = {t i ≡ di t ′ i | i ∈ I}.
Since variables are useful to get compact (possibly finite) axiomatizations, they are typically used when defining deduction systems. We have followed the same idea when defining dDED(E D ), that gives us distance pairs not only between closed processes, but also between open processes. Of course, we expect that any such derivable pair will reflect a universal information, which is formalized by the instantiation rule.

The roles of reflexivity, symmetry and that of the triangular transitivity, were already commented when defining the algebras with distances. Moreover, the substitution rule states the homomorphic character of the obtained distances. Of course, we have a different deduction system for each collection of composing functions ∼ f | f ∈ Σ , however, we prefer to maintain this small abuse of notation. Finally, we have again adopted quite a general point of view when defining dDED(E D ) based on an arbitrary set of distance equations E D . But, once more it is interesting to discuss which are the most natural sets of equations, in which we are specially interested. The role of DED(E ) is to generate the induced set of derived equations from the set E. When we start from the axiomatization of any semantics (e.g. the bisimulation semantics), the related closed processes are exactly those having the same semantics (e.g. those bisimilar).

As explained above, ≡ 0 just reflects the quotient algebra on top of which we will define our distance relations. As a matter of fact the following result tells us that, when E does only contain equations on ≡ 0 , we just obtain a system totally equivalent to an ordinary deduction system. Proposition 1. If E D is a system that only contains equations on ≡ 0 , then the system dDED(E D ) is "essentially" equivalent to DED( E), where

E = {t ≡ t ′ | t ≡ 0 t ′ ∈ E D }. This means that ⊢ ED t ≡ d t ′ ⇔ ⊢ E t ≡ t ′ , ∀d ∈ D.
Proof. This is an immediate consequence of the following facts: (1) The triangular transitivity becomes plain transitivity when d 1 + d 2 = 0; (2) The impossibly to infer facts about ≡ 0 using other ones ≡ d , with d = 0.

⊓ ⊔ Therefore, in order to have a useful deduction system for distances we need to start with a collection of equations E D containing a set of non-trivial non-zero distance axioms t 0 ≡ d t ′ 0 with d > 0. This subset is the "algebraic basis" on top of which E D will derive the induced distance pairs in

⊢ ED t ≡ d t ′ . Proposition 2. Given a system of distance equations E D , if we define E 0 D = {t ≡ d t ′ | d = 0} and we consider the set of ordinary equations E = {t ≡ t ′ | t ≡ 0 t ′ ∈ E 0
D }, then we can see the family of distance relations induced by ⊢ ED as a family of distance relations between the equivalence classes induced by ⊢ E ,

[t] ≡ d [t ′ ] ::= ⊢ ED t ≡ d t ′
Proof. We only need to apply the triangular transitivity rule.

⊓ ⊔ In the following section we apply this algebraic approach, defining a distance for the bisimulation semantics.

An algebraic distance for bisimulation

As stated above, to define our processes, we use the signature including the choice operation with arity 2, and the prefix operators a• ∈ Act with arity 1, together with the constant null, 0. We expand this signature including variables in a set X to obtain the BCCSP (Act, X) syntactic algebra. Then, the corresponding compositional approach to the definition of distances between processes in BCCSP (Act, X) includes the rules:

• If we have p ≡ d p ′ and q ≡ d q ′ , then p + q ≡ d p ′ + q ′ . • If we have p ≡ d q, then ap ≡ d aq.
Moreover, the equations characterizing the bisimulation axioms are turned into distance equations getting:

(B1) x + y ≡ 0 y + x (B2) x + x ≡ 0 x (B3) (x + y) + z ≡ 0 x + (y + z) (B4) z + 0 ≡ 0 z
Finally, we need to add the collection of equations that will work as seed for the computation of distances in an algebraic way. The idea is that we want to pay a tax for each punctual change. Since we are working under a function d defining the distance between actions in Act, we introduce the family of axioms with a, b ∈ Act, which can be considered as a single axiom scheme if we see a and b as generic action: ax ≡ d(a,b) bx. Putting everything together we obtain the following algebraic definition of the bisimulation distance.

Definition 7. Given a function distance d between the actions in Act, producing values in D, and two processes p, q ∈ BCCSP (Act, X), we can say that p is at most d ≥ 0 far away of being bisimilar to q, if and only if p ≡ d q can be derived using the set of rules:

) p ≡ d1 p ′ , q ≡ d2 q ′ ⇒ p + q ≡ d1+d2 p ′ + q ′ . (ii) p ≡ d q ⇒ ap ≡ d aq for all a ∈ Act, d, d 1 , d 2 ∈ D and p, p ′ , q, q ′ ∈ P roc. 5. p ≡ d p ′ ⇒ pρ ≡ d p ′ ρ, for every substitution ρ. 6. (i) ax ≡ d(a,b) bx for all a, b ∈ Act. (ii) x + y ≡ 0 y + x. (iii) x + x ≡ 0 x. (iv) (x + y) + z ≡ 0 x + (y + z). (v) z + 0 ≡ 0 z.
Remark 2. 1. The definition above only considers finite terms in BCCSP (Act, X), but we can extend the application of these rules to infinite processes. However, this extension will only produce distances for the case of pairs of processes that are bisimilar up to the change of finitely many actions (e.g., a ω ≡ d(a,b) ba ω ). In Section 7 we will discuss how we can get other more interesting distances in the infinite case.

2. Once we use addition as the composition function of distance for the choice operator, we could substitute rule 4(i) in Def. 7 by the simpler rule p ≡ d p ′ ⇒ p + q ≡ d p ′ + q. We immediately obtain the original rule by combining this with the triangular transitivity rule 3.

By combining that simplified rule with rule 4(ii) is easy to prove that for any linear context C(x) we have the preservation rule

p ≡ d p ′ ⇒ C(p) ≡ d C(p ′ ).
This will not be true for any arbitrary non-linear C, where in principle if x appears k times in C, then we will have

C(p) ≡ k * d C(p ′ ) but not C(p) ≡ d C(p ′ ).
Obviously, this is an important difference to what happens in DED(E ).

There we can modify the global substitution rule 4 in Fig. 1

⇒            ab0 ≡1 ac0 (Def.7.4) ∧ bb0 ≡1 bc0 (Def.7.4) ∧ bc0 ≡1 cc0 (by Def.7.5, 7.6)    (Def.7.3) ⇒ bb0 ≡2 cc0
and finally applying Def. 7.4 we can conclude ab0 + bb0 ≡ 3 ac0 + cc0.

We developed in [START_REF] Romero-Hernández | Defining distances for all process semantics[END_REF] our operational and our denotational approaches to the definition of distance relations without considering variables. However we can easily extend both of them to cover the full set BCCSP (Act, X). In particular, for the denotational approach that we are using here, we can extend Def. 4 by first extending the preorder ⊆ L to open terms in the classic way, and simply applying the rest of the rules also to these open terms. Now it is immediate to check that if we can derive p(x) = d q(x), using this extension of Def. 4, where the variables in x are those appearing in either p or q, then we can also derive any instance p(r) = d q(r). Here we have used the classical notation p(r), to denote the application of the instantiation of each variable x i in p(x) by the corresponding term, r i .

Lemma 1. If we can derive p(x) = d q(x), then we can also derive any instance of it, p(r) = d q(r).

Proof. By induction on the derivations of p(x) = d q(x) 1. p(x) ∼ q(x) ⇒ p(r) ∼ q(r), by definition of bisimulation. 2. and 3. The application of (2) and (3) in Def. 4, is immediate because instantiation satisfies the homomorphic rules:

(ap(r)) = a(p(r)) and (p + q)(r) = p(r) + q(r).

4. Finally, by a direct application of (4) in Def. 4, from p(r) = n s(r) and s(r) = n ′ q(r) it produces p(r) = n+n ′ q(r). ⊓ ⊔ Next we prove the equivalence between this algebraic definition of the distance relations and the extension of the denotational definition in Def. 4.

Theorem 1. For all p,q ∈ BCCSP (Act, X) we have p ≡ d q ⇔ p = d q Proof. ⇐ | We want to show that if p = d q then p ≡ d q. We use induction over the depth of derivations.

1. p ∼ q p = d q . If p ∼ q, then we can prove it using the set of axioms for bisimulation that are mimicked by the last four axioms in Def. 7.6. So that we have p ≡ 0 q, and then by Def. 7.1 we have q ≡ d q, and finally applying Def. 7.3 we get p ≡ d q as we wanted to show. 3.

p = d p ′ p + q = d p ′ + q
. We have, by the i.h., that p ≡ d p ′ . Trivially q ≡ 0 q using Def. 7.1. Then, we can conclude applying 7.4 (i) that p + q ≡ d p ′ + q.

4. p = d r r = d ′ q p = d+d ′ q . Immediate, using the i.h. and Def. 7.3.

⇒ | By induction on the derivation of p ≡ d q. p ′ = d2 p ′′ , and applying Def. 4.4 we conclude p = d1+d2 p ′′ . 4. (i)p ≡ d1 p ′ , q ≡ d2 q ′ ⇒ p + q ≡ d1+d2 p ′ + q ′ . By the i.h. we get p = d1 p ′ and q = d2 q ′ using Def. 4.3 and 4.4 we get p + q = d1+d2 p ′ + q ′ . (ii)p ≡ d q ⇒ ap ≡ d aq. Immediate, applying the i.h. and Def. 4. (ii)-(iv). Immediate, applying 4.1. ⊓ ⊔ Remark 3. Certainly, we could also remove variables from the algebraic presentation simply expanding every axiom, including instead of it, all its closed instances. Obviously the instance rules will not be necessary after that. But, of course the role of variables in any algebraic presentation is crucial in order to obtain finite axiomatizations where we reflect by a single action an infinity of facts.

Algebraic distances for other semantics

Once we have studied in detail the algebraic definition of the distance for the case of bisimulation, we will briefly discuss the case of the rest of the semantics which are collected in the ltbt-spectrum [START_REF] Van Glabbeek | The linear time-branching time spectrum I: the semantics of concrete, sequential processes[END_REF]. These semantics are not induced by an equivalence relation but by a preorder. Hennessy also presented in [START_REF] Hennessy | Algebraic theory of processes[END_REF] a theory of Σ-po algebras, A, ≤ A , Σ A , which are endowed with a partial order. Now for each f in Σ of arity k, there is a monotonic function

f A : A k → A.
You can find in [START_REF] Hennessy | Algebraic theory of processes[END_REF] all the details about this theory of ordered algebras which smoothly extends that of plain algebras. In particular, Hennessy purposes the proof system DED(I ), in Fig. 2, where I is now a set of inequations.

1. Reflexivity t ≤ t 2. Transitivity t ≤ t ′ t ′ ≤ t ′′ t ≤ t ′′ 3. Substitution t1 ≤ t ′ 1 , . . . , t k ≤ t ′ k f (t1, . . , t k ) ≤ f (t ′ 1 , . . . , t ′ k )
, for every f ∈ Σ of arity k.

4. Instantiation t ≤ t ′ tρ ≤ t ′ ρ , for every substitution ρ.

5. Equations t ≤ t ′ , for every inequation t ≤ t ′ ∈ I As in Section 4 we can adapt this theory of ordered algebras, obtaining an algebraic theory which allows us to measure the distance between processes w.r.t. a given semantics L (in)equationally defined by axioms on an order ⊆ L . So, we define the following ordered deduction system with distances dDED(I ). Definition 8. Given a semantics L algebraically defined by means of an axiomatization I on ≤ L , and a distance d over the set of actions Act, we will say that a process p is at most d ≥ 0 far away of being better than another process q, w.r.t. the preorder ≤ L , if and only if we have ⊢ dDED(I) p ≤ L d q. dDED(I) is the following deduction system:

1. p ≤ L d p, for all d ∈ D. 2. p ≤ L d1 p ′ and p ′ ≤ L d2 p ′′ ⇒ p ≤ L d1+d2 p ′′ . 3. (i) p ≤ L d1 p ′ q ≤ L d2 q ′ ⇒ p + q ≤ L d1+d2 p ′ + q ′ . (ii) p ≤ L d q ⇒ ap ≤ L d aq, for all a ∈ Act. 4. p ≤ L d p ′ then pρ ≤ L d p ′ ρ, for every substitution ρ. 5. ax ≤ L d(a,b) bx. t ≤ L d t ′
, for every inequation t ≤ L t ′ ∈ I. Remark 4. 1. By the way, the only difference between the proof systems DED(E ) and DED(I ) is that in this second case we are defining a preorder and not an equivalence relation, therefore symmetry is lost. The same happens in dDED(I ) by means of which we measure "how far away" a process is to be better than another process w.r.t. the corresponding order ⊆ L . 2. Once we are defining an order and not an equivalence it is natural to consider asymmetric distances d, where d(b, a) denotes what we have to add to b to obtain (at least) a. For instance if a = 1e and b = 2e we could have d(a, b) = 1 but d(b, a) = 0. We have developed our operational distances in [START_REF] Romero-Hernández | Defining distances for all process semantics[END_REF] including this generalization, and it can be also introduced here simply changing the symmetric distance d by an asymmetric distance d.

It is easy to translate the results in Section 4 to this more general framework. In particular, we can prove that each denotational distance, obtained by application of Def.4, is equivalent to the corresponding algebraic distance, obtained by application of Def. 8.

Characterizing the bisimulation distance game

The classic approaches to the definition of distances between processes are based on valued versions of the (bi)simulation game [START_REF] Stirling | Modal and temporal logics for processes[END_REF][START_REF] Fahrenberg | Distances for weighted transition systems: Games and properties[END_REF][START_REF] Cerný | Simulation distances[END_REF]. Definition 9. (Bisimulation game) Given two LTSs, L 1 and L 2 , we call configurations the pairs (p, q), with p ∈ L 1 and q ∈ L 2 . The bisimulation game is played by two players: the attacker A and the defender D. The initial configuration of the game deciding if p 0 ∼ q 0 , is just the pair (p 0 , q 0 ). A round of the game, when the current configuration is (p, q), proceeds as follows:

1. A chooses either p or q. 2. Assuming it chooses p, he next executes a transition in L 1 : p a → p ′ . 3. D must choose a transition with the same label at the other side of the board, i.e., it must execute an a-move in L 2 : q a → q ′ . If A plays at L 2 , then D replies at L 1 . 4. The game proceeds in the same way from the new configuration (p ′ , q ′ ).

The bisimulation game can be turned into the "classical" bisimulation distance game [START_REF] Cerný | Quantitative simulation games[END_REF], by allowing to reply any a-move by some b-move with b = a. However, in this case the defender should pay d(b, a) to the attacker for the mismatch. The value of the game, V(p,q), provides the "classical" bisimulation distance between p and q, d ∼ (p, q). In order to illustrate the generality of our algebraic approach to the definition of distances between processes, next we present an algebraic characterization of that bisimulation game distance.

Definition 10. We define the algebraic bisimulation game collection of relations, {≡ g d , d ∈ D}, as the set of tuples p ≡ g d q which can be derived by applying the following set of rules: , q ≡ g d2 q ′ ⇒ p + q ≡ g max{d1,d2} p ′ + q ′ . (ii) p ≡ g d q ⇒ ap ≡ g d aq for all a ∈ Act, d, d 1 , d 2 ∈ D and p, p ′ , q, q ′ ∈ P roc. 5. p ≡ g d p ′ ⇒ pρ ≡ g d p ′ ρ, for every substitution ρ. As we did for our bisimulation distance, there is still a third equivalent denotational characterization of the bisimulation game distance.

6. (i) ax ≡ g d(a,b) bx for all a, b ∈ Act. (ii) x + y ≡ g 0 y + x. (iii) x + x ≡ g 0 x. (iv) (x + y) + z ≡ g 0 x + (y + z). (v) z + 0 ≡ g 0 z.
Definition 11. We define the denotational bisimulation game collection of relations, {= g d , d ∈ D}, as the set of tuples p = g d q which can be derived by applying the following set of rules:

(1) p ∼ q p = g n q

(2) p = g d q ap = g d+d(b,a) bq

(3) p = g d1 p ′ q = g d2 q ′ p + q = g max{d1,d2} p ′ + q ′
We have proved in [START_REF] Romero-Hernández | Defining distances for all process semantics[END_REF] that the relations defined by Def. 11 remain the same if we add the transitivity rule (4) p = g d1 q q = g d2 r p = g d1+d2 r so further in this paper we consider Def. 11 including this rule. Then, it is easy to get the following theorem based on the proof of Th. 1 Theorem 2. p ≡ g d q ⇔ p = g d q. Proof. Immediate, just substituting + by max in the reasoning related to the application of Def. 4.3 and Def. 7.4.

⊓ ⊔ Remark 6. Although rule (3) in Def. 4 has not +, we can see applying transitivity that this rule is equivalent to

(3 ′ ) p = L n1 p ′ q = L n2 q ′ p + q = L n1+n2 p ′ + q ′ which
produce a simpler proof than the given in Th. 1 when we use 4.3.

Next, we see that the original definition of the distances by means of the distance bisimulation game is also equivalent to these. We start proving two lemmas that provide us some properties of the denotational characterization and of the values of the distance bisimulation game.

Lemma 2 (Prefix lemma). Given two processes P = ap and Q = bq, we have ap = g d bq if and only if there exists some

d ′ such that d = d ′ +d(a, b) with p = g d ′ q.
Proof. ⇐ | Immediate, since if we have Def. 11.2 to p = g d ′ q we get the result. ⇒ | We will prove a more general result. It says that i∈I a i p i = g d j∈J b j q j implies (∀ i ∈ I ∃ j ∈ J p i = g d-d(ai,bj ) q j ). So, the result of this theorem will be just the particular case of this result when we have only one element in the sum. We use induction over the derivation of p = g d q taking p = i∈I a i p i and q = j∈J b j q j .

1.

p ∼ q p = g d q

.

If p ∼ q then we have for each i ∈ I such that a i p i ai -→ p i there exists some j ∈ J with b j q j bj -→ q j where b j = a i and p i ∼ q j . Then we have p i = g d q j and using the rule (2) we can conclude that a i p i = g 0 b j q j as we wanted to show, since d(a i , b j ) = 0.

2. p = g d-d(b,a) q ap = g d-d(b,a)+d(b,a) bq
. Then we have a single summand at both sides, and the premise of the last set of the derivations exactly expresses the thesis to be proved.

3. If we have p = p ′ + p ′′ , q = q ′ + q ′′ and p ′ = g d ′ q ′ p ′′ = g d ′′ q ′′ p = g d=max{d ′ ,d ′′ } q . We will have p ′ = i∈I ′ a i p i , p ′′ = i∈I ′′ a i p i , q ′ = j∈J ′ b j q j , and q ′′ = j∈J ′′ b j q j with I = I ′ ∪ I ′′ and J = J ′ ∪ J ′′ . Then, by applying the i.h. we have ∀i ∈ I ′ ∃j ∈ J ′ with p i = g d ′ -d(ai,bj ) q j and ∀i ∈ I ′′ ∃j ∈ J ′′ with p i = g d ′′ -d(ai,bj ) q j . As d = max{d ′ , d ′′ } we immediately conclude the result applying the triangular transitivity(rule (3)).

4.

p = g d r r = g d ′ q p = g d+d ′ q . We take r = k∈K c k r k and r k = g d ′ -d(c k ,bj ) q j , so applying the i.h. we get ∀i ∈ Proof. That α = g d β is immediate by iterated application of the triangular transitivity rule. We prove the second negative result by induction on n. n = 0| We have d = 0 and then the result is trivial.

I ∃k ∈ K p i = g d-d(ai,c k ) r k (and ∀k ∈ K ∃j ∈ J r k = g d ′ -d(c k ,bj ) q j ). Then, applying the triangular inequality (d(a i , b j ) ≤ d(a i , c k ) + d(c k , b j )) we get that ∀i ∈ I ∃j ∈ J such that p i = g d+d ′ -d(ai,bj ) q j . ⊓ ⊔ Corollary 1. d(α, β) = d(a i
n > 0| Applying the Prefix Lemma -Lemma 2-we should have α ′ = g d ′ -d(a1,b1) β ′ with α ′ = a 2 . . . a n and β ′ = b 2 . . . b n . But, if d ′ < n i=1 d(a i , b i ) then we have d ′ -d(a 1 , b 1 ) < n i=2 d(a i , b i
) contradicting the i.h. for the shorter sequences α ′ and β ′ ⊓ ⊔ Lemma 3. V (p, q) ≤ V (p, r) + V (r, q) for all processes p,q and r.

Proof. We use induction over the depth of processes. For all i ∈ I there exists some k ∈ K with V (p i , r k ) = V (p, r)d(a i , c k ). For all k ∈ K there exists some j ∈ J with V (r k , q j ) = V (r, q) -d(c k , b j ). Combining both, we obtain: For all i ∈ I there exists some j ∈ J and k ∈ K with

V (p i , r k ) + V (r k , q j ) = V (p, r) + V (r, q) -d(a i , c k ) -d(c k , b j ).
and then by applying the i.h. and the triangular inequality for d, we obtain:

∀i ∈ I ∃j ∈ J with V (p i , q j ) ≤ V (p, r) + V (r, q) -d(a i , b j ).
In a symmetric way, we prove that For all j ∈ J there exists some i ∈ I with V (p i , q j ) ≤ V (p, r) + V (r, q) -d(a i , b j ). Applying the definition of the value of the distance game for bisimulation we conclude: V (p, q) ≤ V (p, r) + V (r, q). ⊓ ⊔ The value of the bisimulation game between two processes p and q, V (p, q), gives us "the" distance between them d ∼ (p, q). Next we will see that our denotational definition gives us all the bounds of this distance.

Theorem 3. d ∼ (p, q) = min d {p = g d q}; i.e. p = g d ′ q iff d ∼ (p, q) ≤ d ′ . Proof. In order to simplify our notation we denote simply by d(p, q) the distance between these two processes. We use induction on the depth of p and q. ⊇ | We have that p = g v q and we want to check that d(p, q) ≤ v. We prove it by induction on the derivation of p = g v q. 1.

p ∼ q p = g v q

. If p ∼ q then the value of the bisimulation game is 0, because all along a game we can reply an a-move of p by an a-move of q, and d(a, a) = 0, and conversely.

2. p = g v q ap = g v+d(b,a) bq

. By applying the induction hypothesis we have d(p, q) ≤ v.

Then, the definition of the bisimulation game, produces d(ap, bq) = d(p, q) + d(a, b) ≤ v + d(b, a) as we wanted to see.

3. p = g v q p ′ = g v ′ q ′ p + p ′ = g max{v,v ′ } q + q ′ . By applying the induction hypothesis we have d(p, q) ≤ v and d(p ′ , q ′ ) ≤ v ′ . Now, any a-move on the p-side (resp. p ′side) of p + p ′ can be replied by some b-move on the q side (resp. q ′ -side) of q + q ′ guaranteeing a payment less or equal than v (resp. v ′ ), and conversely. Thus concluding that d(p + p ′ , q + q ′ ) ≤ max{v, v ′ }.

4.

p = g v r r = g v ′ q p = g v+v ′ q

. By applying the induction hypothesis we have d(p, r) ≤ v and d(r, q) ≤ v ′ . Now, applying Lemma 3 we conclude d(p, q) ≤ v + v ′ .

⊆ | The proof is by induction on the depth of the processes. If it is 0 the result is trivial. Therefore, let us consider decomposition of the two involved processes p = a i p i and q = b j q j . Applying the definition of the bisimulation game, from d(p, q) = v we obtain that for all i ∈ I there exists some j i ∈ J such that d(p i , q ji ) + d(a i , b ji ) ≤ d(p, q). Reciprocally, for all j ∈ J there exists some i j ∈ I such that d(p ij , q j ) + d(a ij , b j ) ≤ d(p, q). Now, by applying the induction hypothesis we have ∀i ∈ I p i = d(pi,qj i ) q ji and ∀j ∈ J p ij = d(pi j ,qj ) q j .

From which applying Def. 11.2 we obtain ∀i ∈ I a i p i = d(pi,qi j )+d(ai,bj i ) b ji q ji and ∀j ∈ J a ij p ij = d(pi j ,qj )+d(ai j ,bj ) b j q j , that applying the monotonicity of the bounds computed by Def. 11 produces ∀i ∈ I a i p i = d(p,q) b ji q ji and ∀j ∈ J a ij p ij = d(p,q) b j q j . These two can be combined applying Def. 11.3 to produce p = a i p i = d(p,q) i∈I b ji q ji and j∈J a ij p ij = d(p,q) b j q j = q. We only need to combine these two again using Def. 11.3 and the idempotency of bisimilarity, to conclude p = d(p,q) q, as we wanted to show. ⊓ ⊔

Conclusions and future work

We have presented an algebraic framework to define distances between processes.

In particular those associated to the semantics that are axiomatizable. Although a part of our definitions and properties could be applied to arbitrary processes, most of them are based on the consideration of finite image processes. It can be syntactically represented by a (finite) term of a certain signature. Currently we are working on the extension of our results to the infinite case. Following [START_REF] Hennessy | Algebraic theory of processes[END_REF] the idea is to approximate processes by their finite approximations and compare them level by level. Then, we would state that p ≡ d q if and only if we have p n ≡ d q n ∀n ∈ N. But whenever Act is finite, or the non-null values of d(b, a) are low bounded, we could only obtain a finite distance p ≡ d q for some d ∈ D, when q can be obtained from p by a finite number of applications of the rules in Def. 7; that is, whenever p and q are bisimilar up to a finite number of changes of the actions occurring in them.

In order to obtain a more general distance that also produces finite values for pairs of processes which cannot be transformed one into the other by a finite number of transformations, we would need to adopt a discounting function. The idea is that the weights of the disagreements between the two compared processes decrease with the depth they occur. This is easily formalized in our algebraic framework, simply changing our rule 4 ii) in Def. 7 by a discounted rule p ≡ d q ⇒ ap ≡ αd aq where α > 1. As a matter of fact this is another instantiation of our Def. 5. In such a case it would be immediate to check that when d(b, a) = 1 and α = 1 2 , we would have a ∞ ≡ 2 b ∞ .

We are also working on the definition of these distances by applying a coinductive approach that avoids the consideration of finite approximations to obtain the distances between infinite processes.

We have used the algebraic developments in [START_REF] Hennessy | Algebraic theory of processes[END_REF] to base our algebraic theory on distances. We did that, not only due to the simplicity and clarity of its presentation of the theory, but also because of its detailed study of the testing semantics. We hope indeed that most, if not all, of the concepts and results on this semantics will be transferable to the distance scenario. So, we will obtain a nice theory of approximated pass of test both producing a distance for the induced semantics, and an interesting new concept to be applicable in practice.

Appendix: On the operational definition of the distances between processes

It is well known that the set of (unordered) finite trees labelled in their arcs by actions in Act: F T ree(Act), constitute an initial model for the theory of bisimulation. A similar result can be obtained, adding variables in X, for the set F T ree(Act, X) of trees which besides the constants in Act also can have variables in X labeling their leaves. By applying Def. 7 and Prop. 2, we immediately obtain a family of distance relations on both F T ree(Act) and F T ree(Act, X). In other words these two algebras become a (D, Σ)-algebra and a (D, Σ(X))-algebra, respectively, when considering these two families of distance relations. Next, we present in detail the corresponding operational definition, already studied in [START_REF] Romero-Hernández | Defining distances for all process semantics[END_REF]. Later, we develop the proof of its equivalence with the denotational and algebraic characterizations, that were proved to be equivalent each other at Section 4. Definition 12. We say that an unordered tree p is at most at distance d from another tree q, w.r.t. the symmetric distance between actions d, and then we write d d (p, q) ≤ d, if and only if:

• (C1) p = ap ′ , q = bp ′ , and d ≥ d(a, b), or • (C2) p = p ′ + r, q = q ′ + r, and d ≥ d d (p ′ , q ′ ), or • (C3) p = ap ′ , q = aq ′ , and d ≥ d d (p ′ , q ′ ), or • (C4) d ≥ 0 and q can be obtained from p by application of (B1)-(B4), or Definition 13. We define p 1 d q if and only if 1. ap ′ 1 d bp ′ and d ≥ d(a, b), or 2. p ′ + r 1 d q ′ + r and p ′ 1 d q ′ , or 3. ap ′ 1 d aq ′ and p ′ 1 d q ′ , or 4. d ≥ 0 and q can be obtained from p by application of (B1)-(B4). Definition 16. We define p | d p ′ if and only if we have p 1 d p ′ , or there exists some q such that p | d1 q q | d2 p ′ , where d 1 + d 2 = d. Proof. We want to prove that p d q ↔ p = d q.

⇒ | We use induction over the length of the path generating p d q. We also use induction on the derivation of p 1 d to prove this basic case. 1. p 1 d p ′ with p = ap ′′ and p ′ = bp ′′ and d ≥ d(a, b). We only need to apply rule (2) in Def. 4 to get that ap ′′ = d bp ′′ . 2. p ′ + r 1 d q ′ + r with p 1 d p ′ . The i.h. now produces that p ′ = d q ′ , and then applying rule (3) in Def. 4 we get that p ′ + r = d q ′ + r. We can apply the i.h. obtaining p = d1 p ′′ and p ′′ = d2 p ′ , and now applying rule (4) in Def. 4 we get p = d1+d2 p ′ , i.e., p = d p ′ , as we wanted to show.

⇐ | Now we proof p = d q ⇒ p d q, by induction on the derivation of p = d q.

1.

p ∼ q p = d q . Trivially if p ∼ q then p d q with d ≥ 0, applying Def. 13.4.

2.

p = d-d(b,a) q ap = d bq . By applying the induction hypothesis we have p d-d(a,b) q and applying the structural lemma we obtain bq d-d(a,b) bq, from where using Def. 13.1 and Def. 15 we can conclude that ap d bq.

3.

p = d p ′ p + q = d p ′ + q . Again, by applying the induction hypothesis we have p d p ′ , and applying the structural lemma we conclude p + q d p ′ + q.

4. p = d q q = d ′ r p = d+d ′ r . By the i.h. we have p d q and q d ′ r. So, applying Def. 15 and Prop. 3 we get p d+d ′ r.

⊓ ⊔

Definition 5 .

 5 Let D be an adequate domain for distance values (e.g. N, R + , Q + ) and Σ a (classic) signature. A (D, Σ)-algebra is a Σ-algebra A, Σ A and a collection of relations ≡ d , d ∈ D , ≡ d ⊆ D × D, such that: 1. a ≡ 0 a, for all a ∈ A.

2 .

 2 a ≡ d b ⇔ b ≡ d a, for all a, b ∈ A and all d ∈ D. 3. d ≤ d ′ , a ≡ d b ⇒ a ≡ d ′ b, for all a, b ∈ A and all d, d ′ ∈ D. 4. (a ≡ d b ∧ b ≡ d ′ c) ⇒ a ≡ d+d ′ c, for all a, b, c ∈ A and all d, d ′ ∈ D. 5

Example 1 .

 1 by a local substitution, where only an argument of f is substituted. It is possibly to do it without obtaining nothing new due to the presence of the transitivity rule. For instance, let us take Act = {a, b, c} and define d(a, b) = 1, d(a, c) = 2 and d(b, c) = 1. Now we will show that ab0 + bb0 ≡ 3 ac0 + cc0: b0 ≡1 c0 (Def.7.5, 7.6)

  2.p = d q ap = d+d(b,a) bq. By the i.h. we have p ≡ d q. We use the equation ax ≡ d(a,b) bx, Def. 7.1 and 7.5 to get ap ≡ d(a,b) bp. Moreover, applying Def. 7.4 (ii) and the i.h. we get bp ≡ d bq; and finally by the triangular transitivity rule (7.3) we can conclude ap ≡ d+d(a,b) bq.

2 . 5 .

 25 p ≡ d p ′ ⇒ pρ ≡ d p ′ ρ, for every substitution ρ. Trivially, applying Lemma 1. 6. (i) ax ≡ d(a,b) bx, applying 4.2 and 4.1.

Fig. 2 .

 2 Fig. 2. The proof system DED(I )

Remark 5 .

 5 Note that the definition of the algebraic bisimulation distance by means of the collection {≡ d , d ∈ D} in Def. 7, and that of the algebraic bisimulation game distance by means of {≡ g d , d ∈ D}, are nearly the same. We only modify the composition rule 4 (i), where the composition function ∼ f -see Def. 5.5-was initially + and now it becomes max.

  , b i ) where α = a 1 . . . a n and β = b 1 . . . b n . This means that we have α = g d β with d = n i=1 d(a i , b i ), and for all d ′ < d we have α = g d ′ β.

  • (C5) There exist r, d ′ and d ′′ s.t. d ′ ≥ d d (p, r), d ′′ ≥ d d (r, q) and d ≥ d ′ + d ′′ .

Proposition 3 .Lemma 4 ( 1 dn 1 di+1 1 d1 ap 1 1 d2 ap 2 1Theorem 4 .

 34111124 Def. 14,15, 16 are obviously equivalent.Proof. Routine well known induction.⊓ ⊔ Structural lemma). If p d q then (1) ap d aq and (2) p+r d q + r.Proof. (1)| If p 1d q then trivially we have ap 1 d aq applying Def. 13.3. If p d q then we use induction over the path length. Similarly, if we have p = p n = p ′ with d = d i , we will get ap i ap i+1 for all i < n. So that, we haveap = ap 0 d3 • • • 1 dn ap n = ap ′ with d = d ithus proving ap d1 ap ′ .(2)| Analogous to[START_REF] Cerný | Quantitative simulation games[END_REF]. ⊓ ⊔ The operational definition of distance relations, d , and the denotational one, defining the family = d , are equivalent.

3 . ap 1 d

 31 ap ′ with p 1 d p ′ . One more time, the i.h. produces p = d p ′ , and applying rule (2) in Def. 4 we get ap = d ap ′ . 4. p 1 d p ′ with d ≥ 0 and p ′ can be obtained from p by application of (B1)-(B4). As p ∼ p ′ trivially we have using rule (1) in Def. 4 that p = d p ′ . 5. p d p ′ if and only if ∃ p ′′ p d1 p ′′ p ′′ d2 p ′ with d = d 1 + d 2 .

  ≡ d1 p ′ and p ′ ≡ d2 p ′′ ⇒ p ≡ d1+d2 p ′′ . By the i.h. we get p = d1 p ′ , and

1. p ≡ d p. Obviously, we have p ∼ p and then by Def. 4.1 we get p = d p. 2. p ≡ d p ′ ⇒ p ′ ≡ d p. By the i.h. we get p = d p ′ , and it is immediate to check, by induction on the derivation of p = d p ′ that we can generate a symmetric derivation concluding p ′ = d p. We use that ∼ is an equivalence relation in Def. 4.1, and d is a symmetric relation in Def. 4.2. 3. p

  1. p ≡ g d p for all d ∈ D and p ∈ P roc. 2. p ≡ g d p ′ ⇒ p ′ ≡ g d p for all d ∈ D and p, p ′ ∈ P roc. 3. p ≡ g d1 p ′ and p ′ ≡ g d2 p ′′ ⇒ p ≡ g d1+d2 p ′′ for all d 1 , d 2 ∈ D and p, p ′ , p ′′ ∈ P roc.

	4. (i) p ≡ g d1 p ′

  Definition 14. We define p d p ′ if and only if there exist p 1 , . . . , p n such that Definition 15. We define p * d p ′ if and only if we have p 1 d p ′ , or there exists some p ′′ such that p 1 d1 p ′′ and p ′′ * d2 p ′ , where d = d 1 + d 2 .

	p 1 d1 p 1	1 d2 p 2	1 d3 • • • 1 dn p

n = p ′ , where d i = d.

⋆ Partially supported by the Spanish projects TESIS (TIN2009-14312-C02-01), DE-SAFIOS10 (TIN2009-14599-C03-01) and PROMETIDOS S2009/TIC-1465.