Andrés F Ocampo
email: andres.ocampop@udea.edu.co

Juliver Gil-Herrera
email: juliver.gil@udea.edu.co

Pedro H Isolani
email: pedro.isolani@uantwerpen.be

Miguel C Neves
email: mcneves@inf.ufrgs.br

Juan F Botero
email: juanf.botero@udea.edu.co

Steven Latré
email: steven.latre@uantwerpen.be

Lisandro Zambenedetti

Marinho P Barcellos
email: marinho@inf.ufrgs.br

Luciano P Gaspary

Optimal Service Function Chain Composition in Network Functions Virtualization

Keywords: Network Function Virtualization, Virtual Network Functions, Service Function Chain, VNFs Chain Composition

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Network Functions Virtualization is an emerging network management framework for service deployment, which allows Network Functions to be allocated onto general purpose servers [START_REF] Beck | Scalable and coordinated allocation of service function chains[END_REF]. It enables to dynamically compose chains of Virtual Network Functions and embed them anywhere in the network according to a predefined objective. For instance, network functions such as firewalls, load balancers, and deep packet inspection systems can be placed at the most appropriate location in the network to support users demand, Quality of Service (QoS) requirements, or management needs. NFV has grabbed the attention from industry because it has the potential to reduce both CAPEX and OPEX, by the dynamic deployment of VNFs to commodity hardware, avoiding vertically integrated solutions. In academia, NFV has been a hot topic because there are interesting technical challenges to be overcome [START_REF] Beck | Coordinated allocation of service function chains[END_REF][START_REF] Beck | Scalable and coordinated allocation of service function chains[END_REF][START_REF] Elias | Efficient orchestration mechanisms for congestion mitigation in nfv: Models and algorithms[END_REF], such as the NFV allocation problem [START_REF] Faizul Bari | On orchestrating virtual network functions[END_REF][START_REF] Gil-Herrera | Resource allocation in nfv: A comprehensive survey[END_REF].

To better understand our proposed model in later sections, we introduce the most important terms used throughout this paper.

Network Service (NS): It is an offering provided by an operator that is delivered using one or more network functions. Network service is a complete, end-toend functionality provided by the network operator, such as network protection. A network service may comprise one or more VNFs, for example, a firewall, a deep packet inspector (DPI), and a data monitor, as in the case of a network protection system.

Virtual Network Function (VNF): It is a function responsible for a specific treatment of data flows. A VNF can act at various network layers of the protocol stack. As a logical component, a VNF can be realized as a virtual element or be embedded in a physical network appliance. One or more VNFs can be embedded in the same physical element.

Service Function Chain (SFC): It is an ordered or partially ordered set of VNFs. The implied order may not be a straight line, since the architecture allows SFCs that send traffic to more than one branch, and also allows cases where there is flexibility in the order in which VNFs need to be applied. SFCs may be unidirectional or bidirectional, depending on the state requirements of the network functions. Many common functions such as DPI and firewalls often require bidirectional chaining in order to ensure that the flow state is consistent. An SFC, in ETSI's terminology, is called VNF Forwarding Graph (VNF-FG) 4 .

Efficient network services require the optimal allocation of resources in NFV (NFV-RA), a challenging problem [START_REF] Gil-Herrera | Resource allocation in nfv: A comprehensive survey[END_REF]. A chain of VNFs must be intelligently composed and allocated to the infrastructure to provide end-to-end QoS guarantees for the applications. However, given the VNFs dependencies, the allocation is extremely challenging.

The above mentioned NFV-RA problem can be sub-divided into three subproblems: (i) SFC composition, (ii) SFC embedding and (iii) SFC scheduling. Due to the fact that several chains can fulfill the same NS, the order of VNFs is often flexible; that is, some VNFs have to be placed in a specific order (e.g., the network flow first has to be decrypted before it can be further processed), while others are flexible in that regard (i.e. they dont depend from one another). Therefore, the composition of the best possible chain (SFC composition) for each NS is very important for the operator. However, SFC composition has been so far overlooked by the scientific community, typically taken as an assumption. Besides, to the best of our knowledge, previous solutions are heuristic in nature and, therefore, do not guarantee optimal solutions.

In this paper, our contributions are twofold: 1) we propose a way to formally describe network services as a set of VNFs considering the dependences among them and how they can be concatenated in SFCs and 2) we propose an ILPbased approach to optimally solve this sub-problem by characterizing the service requests in terms of virtual network functions and solving the SFC composition problem.

The remainder of this paper is organized as follows. In Section 2, we describe the main approaches tackling the NFV-RA problem. In Section 3, we define the SFC composition problem. Section 4 specifies our ILP formulation in detail. Section 5 presents the performance evaluation of our proposed approach. Finally, in Section 6, we conclude the paper with final remarks and perspectives for future work.

Related Work

The majority of current NFV-RA approaches starts from the assumption that the chain of VNFs has been already composed, i.e., the important stage of SFC composition is taken for granted. Few approaches have been proposed to solve the SFC composition stage so far. Mehraghdam et al. [START_REF] Mehraghdam | Specifying and placing chains of virtual network functions[END_REF] formulate a context-free language for formalizing chaining requests. They propose a greedy heuristic that tries to minimize the total data rate of the resulting chain by composing first the VNF that reduces the data rate of the flows in each step. Recently, Beck and Botero [START_REF] Beck | Coordinated allocation of service function chains[END_REF] proposed a scalable recursive heuristic that, at each step, composes a VNF in the service chain and, at the same time, embeds it in the substrate network (SN) trying to rapidly find a feasible solution.

Most of the existing NFV-RA approaches deal just with the embedding stage as they consider the VNF-FG as a given input of the problem [START_REF] Gil-Herrera | Resource allocation in nfv: A comprehensive survey[END_REF]. For instance, Bari et al. [START_REF] Faizul Bari | On orchestrating virtual network functions[END_REF] propose exact Integer Linear Programming (ILP) and heuristic based approaches trying to minimize the OPEX caused by the SFC embedding. Also, Elias et al. [START_REF] Elias | Efficient orchestration mechanisms for congestion mitigation in nfv: Models and algorithms[END_REF] formulate the SFC embedding as a non-linear integer optimization model where the objective function is to minimize the network congestion.

The aforementioned review shows that, up to now, little research has been performed in the composition stage of the SFC problem. Current solutions are heuristic-based and no optimal solution for the problem has been proposed so far. An optimal solution results in the best possible composition of the service chain with regard to a predefined objective. In this paper, we propose an optimal approach to solve the problem based on Integer Linear Programming.

The SFC Composition Problem

When allocating resources for a given NS, service providers receive a chain of VNFs and apply an embedding strategy for placing and linking these functions on the physical substrate. Despite being automatic, this process is rigid for clients and service providers, respectively. While clients must deal with complex function dependencies when specifying services, providers are not able to structure the chains in order to find the best fit for their infrastructure. The result is the allocation of suboptimal chains, which may require many more VNF instances or network bandwidth than necessary, leading to high costs and expenditures.

Although some dependencies and connections among VNFs in a service must be considered, the order of the VNFs (i.e., the structure of the chain) is often flexible. For example, normally there is no explicit dependency between a leakage prevention system and a traffic shaper or between a proxy server and a WAN optimizer. As a consequence, it is possible for several different chains to fulfill the same service. We call the problem of finding the most appropriate VNF chain, given a network service specification and a set of resource constraints, the SFC composition problem.

Figure 1(a) shows our proposal on how a network service specification (i.e., a Virtual Network Functions Request -VNFR) looks like. Instead of providing the VNF chain structure as a whole, clients have to inform only the necessary information for allowing network service providers to derive the best chain according to some predefined goal (e.g., to minimize the number of NF instances or the bandwidth demand). Essentially, a VNFR has five elements: (i) the initial data rate of the network flow (r init ), (ii) the set of VNFs that compose the service, each one with their respective processing requirement (d rel ), (iii) the VNFs where the flow initiates (n init ) and terminates (n term ), (iv) a number of outgoing links (solid purple arrows) at each VNF, and (v) mandatory dependencies (dotted blue arrows).

Outgoing links can be used to represent scenarios where traffic is split (e.g., bifurcations). If a VNF has more than one outgoing link, then it splits the traffic flow into the same number of sub-flows. For example, consider a load balancer or a DPI server separating TCP and non-TCP traffic. Each sub-flow has a relative traffic rate (r rel ), which can be higher than 100% if the function replicates or encodes traffic.

Dependencies, in turn, may be of two different types: between a VNF and an outgoing link, or between two distinct VNFs. Outgoing link dependencies represent VNFs that should selectively be placed on one of the sub-flows (e.g., a firewall that succeeds an anomaly-based IDS only for suspicious traffic). Dependencies between VNFs, on the other hand, indicate that the dependent function must be present in each and every sub-flow in the chain (e.g., the cache servers succeeding a load balancer).

In Figure 1(b), we represent two possible chains for the service described in Figure 1(a). Notice that VNFs 2 and 3 selectively appear in the sub-flows of VNF 1, while VNF 4 is present in both subpaths. Moreover, bandwidth and processing demands are determined according to the relative traffic of each outgoing link. Although structurally similar, the left chain (i.e., VNF-FG 1) requires less network and computing resources, which at the end results in lower costs for both clients and providers. As an outcome of the SFC composition problem, VNF-FG 1 would be sent for embedding in the provider infrastructure.

Table 1 details the notation used in the model proposed in the following section. The first part of the table introduces the parameters of a Network Service Request. The second part explains the sets of nodes of an augmented graph used to build the ILP model. Finally, the table shows the ILP variables.

Before jumping into the next section, it is worth mentioning that the outcome of the chain composition stage is one complete service chain (VNF-FG) with regard to one predefined objective and that the amount of required capacities depends on the amount of data handled by that VNF instance.

SFC Composition Problem Formulation

Augmented Graph

To solve the SFC composition problem, we propose an ILP model that is built based on an augmented graph created from the VNFR as follows:

-For the first VNF (n init ) of the VNFR, one node is placed in the augmented directed graph G ext = (V ext , L ext ); -For each of the remaining VNFs, we create as many nodes as the maximum number of instances that a VNF may have. For example, in Figure 2, the maximum number of instances is 2, as the VNF 1 splits the traffic in two subflows. To ease the notation, the node i m ∈ V ext denotes the m-th instance of the node i ∈ V ; -Then, we place directed links between each pair of nodes of the graph except for:

• Instances of the same VNFs: Binary variable that says whether the path p ∈ P is used in the augmented network Figure 2, where n init =VNF1, shows how an augmented graph (see Figure 2b 5 ) is created from a VNFR (see Figure 2a).

(i m , j n ) ∈ L ext , ∀i m ∈ V ext , j n ∈ V ext ⇐⇒ i = j; • Links directed to n init : (i m , j n ) ∈ L ext , ∀i m ∈ V ext , j n ∈ V ext ⇐⇒ j = n init .
Our ILP model is based on the fact that any possible chaining is a subgraph of the augmented graph, so the ILP variables (cf. Table 1) mainly denote which nodes and links of the augmented graph are considered to be parts of the chain, and the demands they will have due to the chosen chaining. Figure 3a shows two possible chains that can be created out of VNFR in Figure 2a, and how they are present in the augmented graph (see Figure 3b).

ILP Formulation

The following is the ILP formulation of the chain composition problem. That is to say, the ILP that models how to insert a VNFR in the augmented graph with respect to a predefined objective (e.g. minimize the number of VNF instances of the resulting VNF-FG).

Constraints:

Link Mapping Constraints:

y i,b i m ,j n ≤ p∈P y i,b,p i m ,j n : (i m , j n ) ∈ Lext, (i, b) ∈ L (1) H • y i,b i m ,j n ≥ p∈P y i,b,p i m ,j n : (i m , j n ) ∈ Lext, (i, b) ∈ L (2) y i,b,p i m ,j n ≤ δ p i m ,j n : (i m , j n ) ∈ Lext, (i, b) ∈ L, p ∈ P (3)
Equations 1, 2, and 3 indicate the relationship between variables y i,b i m ,j n and y i,b,p i m ,j n (here H is a big number that enforces the binary constraint). They indicate that the augmented link (i m , j n ) ∈ L ext can map the outgoing link (i, b) ∈ L when it is mapped using a predefined path p ∈ P . Remember that the same outgoing link (i, b) ∈ L may be mapped in several links (i m , j n ) ∈ L ext . For example, in Figure 1a, in the VNFR, the outgoing link of VNF 4 is mapped in two different links between VNF 4 and VNF 5 in the VNF-FG 1 (see Figure 1b).

Equations to ensure that if a path p is mapped to the augmented graph, all its links have to be assigned.

(i m ,j n )∈L ext (i,b)∈L y i,b,p i m ,j n ≤ H • u p : p ∈ P ( 4
) (i,b)∈L y i,b,p i m ,j n ≥ δ p i m ,j n • u p : (i m , j n ) ∈ Lext, p ∈ P (5)
Equation 4 ensures that if a path is not mapped in the augmented graph, then variable y i,b,p i m ,j n should be zero for all links belonging to that path. Equation 5 ensures that if path is mapped in the augmented graph, then the variable y i,b,p i m ,j n should be one for all links belonging to that path. Equation 6ensures that an outgoing link (i, b) ∈ L of the VNFR should be mapped in an augmented link of the augmented graph just for one path:

p∈P y i,b,p i m ,j n ≤ 1 : (i m , j n ) ∈ Lext, (i, b) ∈ L (6)
Establishment of y i m ,j n :

y i m ,j n = (i,b)∈L y i,b i m ,j n ≤ 1 : (i m , j n ) ∈ Lext ( 7
)
y i m ,j n ≤ x m i : (i m , j n ) ∈ Lext ( 8
)
y i m ,j n ≤ x n j : (i m , j n ) ∈ Lext (9)
Constraints 7, 8, and 9 establish the belonging of a link of the augmented graph (i m , j n ) ∈ L ext to the resulting service chain (VNF-FG).

Node Mapping Constraints:

Establishment of x m i :

x m i = (i m ,j n )∈L ext y i,b i m ,j n : i ∈ V k , 1 ≤ m ≤ M i , (i, b) ∈ L i out (10)
Lower bound in the possible number of instances for i:

M i m=1 x m i ≥ M I(i) : i ∈ V k (11)
Constraints 10 and 11 establish the belonging of a node i m ∈ V ext in the resulting service chain (VNF-FG).

Dependencies fulfillment constraints:

(i m ,j, n )∈L ext y i,b i m ,j n ≥ 1 : l ∈ V k , l = ninit, (i, b) ∈ req(l) (12)
Constraint 12 ensures that for each node l ∈ V , all the dependencies are mapped.

Position constraints:

y i,b,p i m ,j n • P os p i m ≤ P os p l r : l ∈ V k , l = ninit, (i, b) ∈ req(l), l r ∈ Vext, (i m , j n ) ∈ Lext, p ∈ P, δ p i m ,j n = 0 (13) l r ∈V ext p∈P :l r ∈P (i m ,j n )∈L ext y i,b,p i m ,j n ≥ 1 : l ∈ V k , l = ninit, (i, b) ∈ req(l) (14)
Constraint 13 ensures the precedence of the dependencies. If one VNF instance l ∈ V is mapped in the augmented graph, then the set of its dependent links should be mapped in a prior position in the path going from n init to l. Constraint 14 ensures that the path being used to map the VNF's dependencies also contains an instance of the VNF.

Incoming links for each x m i :

(j n ,i m )∈L ext y j n ,i m ≥ x m i : i ∈ V k , 1 ≤ m ≤ M i , i = ninit ( 15
) (j n ,i m )∈L ext y j n ,i m ≤ H • x m i : i ∈ V k , 1 ≤ m ≤ M i (16)
Equations 15 and 16 state that if a link of the augmented graph is part of the resulting service chain (VNF-FG) then the end nodes of this link should be part of the chain too.

The following Equations to establish z i,b i m ,j n linearize the following product

z i,b i m ,j n = T D i m (BW ) • y i,b i m ,j n . z i,b i m ,j n ≤ y i,b i m ,j n • H : (i m , j n ) ∈ Lext, (i, b) ∈ L (17) z i,b i m ,j n ≤ T D i m (BW ) : (i m , j n ) ∈ Lext, (i, b) ∈ L (18) z i,b i m ,j n ≥ T D i m (BW ) -(1 -y i,b i m ,j n ) • H : (i m , j n ) ∈ Lext, (i, b) ∈ L (19)
Constraints to set demands:

LD i,b i m ,j n (BW ) = r rel (i, b)z i,b i m ,j n : (i m , j n ) ∈ Lext, (i, b) ∈ L (20) LD i m ,j n (BW ) = (i,b)∈L LD i,b i m ,j n (BW ) : (i m , j n ) ∈ Lext (21) T D j n (BW ) = (i m ,j n )∈L ext LD i m ,j n (BW ) : j n = ninit ∈ Vext (22) T D n 1 init (BW ) = rinit • x n 1 init ( 23
) (i m ,j n )∈L ext LD i m ,j n (BW ) = T D i m (BW ) • r rel (i) : i m ∈ Vext, i / ∈ Nterm (24)
These set of equations simply set the bandwidth demand of each link in the augmented graph and also the complete load received by each node in the augmented graph. Here, H is just a big number to force binary variables to take 0 or 1 values.

Performance Evaluation

In this section, a performance evaluation of the ILP is presented. Our evaluation focuses primarily on minimizing the total bandwidth demanded by the constructed service chain (VNF-FG). Three scenarios are configured in order to analyze our ILP model following typical cases for service chaining [START_REF] Will | Service function chaining (sfc) general use cases[END_REF].

Simulation Scenario

The ILP model for SFC composition presented in the previous section was implemented in the Gurobi solver [START_REF]Gurobi optimizer reference manual[END_REF] which provides an exact solution. To the best of our knowledge, just one work [START_REF] Mehraghdam | Specifying and placing chains of virtual network functions[END_REF] has dealt separately with the composition phase of NFV-RA. This work heuristically tries to allocate those VNFs with flexible order following an ascending order according to their ratio of outgoing to incoming data rate. Here, we compare our ILP-based exact model with this heuristic proposal.

Simulations are performed for three VNFRs based on typical use cases of networks chains [START_REF] Will | Service function chaining (sfc) general use cases[END_REF]. Figure 4 illustrates the simulation settings for each scenario. The first request VNFR 1 is given for service with NAT64 functions where the traffic is processed by a subchain (composed of VNF 1, VNF 2 and VNF 3), then the NAT function (VNF 4) for IP capabilities (e.g., mapping from IPv6 to IPv4), and then processed by another subchain (VNF 5). The first subchain could have VNFs with optional order, so a good planning of such functions in the final VNF-FG would impact the entire network performance.

The second scenario (VNFR 2) follows the structure of a service chain used to split service paths where service providers enable content awareness. VNF 1 splits the traffic into two sub-flows through two outgoing links. On the one In order to validate the effectiveness of our solution, we compare it with the heuristic mentioned before, in terms of the total bandwidth demanded by VNF-FG, that is, the sum of all bandwidth demands on each link of the VNF-FG. Figure 5 shows the comparison between the ILP model and the heuristic in the aforementioned scenarios. On the one hand, for scenarios where the traffic is split out into several links (e.g. VNFR 2), our solution yields better results than the VNF-FG of the heuristic, demanding around 5 Mbps less of the total bandwidth. On the other hand, for scenarios such as VNFR 1 as well as on each bifurcation of VNFR 3, where all the possible chains are disposed in a monotonic order, i.e., following and straight concatenation, both solutions yields same results in terms of demanded bandwidth.

For VNFRs splitting the traffic into several bifurcations (e.g., scenarios VNFR 2 and VNFR 3), the ILP model would be able to obtain VNF-FGs with more than one instance of the same VNF for those cases in which such function must be performed by each sub-flow. This is the case of VNFR 2: for instance, where VNF 4 has to be performed by each sub-flow, our solution establishes that it must be implemented in two separately instances (one per sub-flow). Thus, the load of traffic arriving at VNF 4 is divided requiring less processing device capabilities into the physical network before the embedding process. As shown in Figure 6b, VNF 4 in our ILP solution VNF 4 is created with two instances with incoming traffic loads of 400 Mbps and 600 Mbps respectively whereas the heuristic solution maps VNF 4 to the same instance for both sub-flows processing an incoming load traffic of 1Gbps. The fact that VNFs are created in more than one instance would facilitate the subsequent embedding phase of NFV-RA.

Similarly, in VNFR 3, VNF 7 has to be located after all three sub-flows. Our ILP solution generates two instances of this function; instance 1 receives a load traffic of 400 Mbps from one sub-flow, while instance 2 receives a traffic load of 600-Mbps from two sub-flows, as shown in figure 6c.

In VNFR 1 where the VNF-FG in any combination is a monotonic graph without bifurcations, only one instance of each function is mapped. Summarizing, results show that, for the simulated scenarios, our ILP model always performs better or equal than the evaluated heuristic proposal [START_REF] Mehraghdam | Specifying and placing chains of virtual network functions[END_REF]. Specifically, the proposed ILP model provides better behavior when VNFRs present traffic bifurcations as it results in less total demanded bandwidth than the heuristic approach. Also, our solution creates several instances per VNF when bifurcation is present in the VNFR which would ease the subsequent embedding phase of NFV-RA as instances with less arriving bandwidth are easier to be embedded in the substrate network. The mean run time of our model considering all performed scenarios was 1.33 seg, in comparison to the heuristic with a mean run time of 0.028sec. Also, it is important to note that the objective function of our ILP was restricted here to the minimization of the total link bandwidth in the resulting VNF-FG (to be comparable with the existing heuristic). However, this objective may change depending on the operator's goals to several ones, such as: minimization of the number of created instances, minimization of the total processing capacities, etc.

Conclusion and Future Work

This paper introduces a novel approach to optimally solve the SFC composition problem based on Integer Linear Programming. Evaluation results indicate that the proposed approach outperforms existing heuristic-based approaches. Specially, when bifurcation of VNFs is present in the VNFR, the proposed ILP model reduces the total incoming bandwidth and creates lighter instances of VNFs in the VNF-FG in order to facilitate the subsequent embedding phase.

Scalability issues of the proposed approach are still to be tested. Simulation scenarios were based in current IETF drafts that show only small VNFRs. A evaluation on larger scenarios to test the scalability of the approach is left for future work. Also, the extension of the ILP model to include the embedding phase of NFV-RA is an exciting branch of future research. In this way, a coordinated model including SFC composition and embedding may be created to optimally solve the two phases of NFV-RA.

Fig. 1 :

 1 Fig. 1: VNF chain composition

V

  N F R(V, L) Is the service request formed by V VNFs and L VNF links V Set of VNFs L Set of VNF links; this is the set of all links coming out the different VNFs belonging to the VNFR L i out ⊂ L Determines the (outgoing) VNF links of the VNF i ∈ V ; a VNF with multiple links splits the network flow into several sub-flows Sets N term ⊂ V VNFs where the service terminates r init : Z Z Z Initial data rate of the VNFR r rel (i) : V → Z Z Z Total traffic (in percentage) departing from node i ∈ V n init ∈ V Initial VNF of the service d rel (i) : V → R R R Relative processing capacity demands of the VNF i ∈ V r rel (i, b) : L → Z Z Z Relative link traffic rate of link (i, b) ∈ L, here i ∈ V identifies the link source VNF and b is the link number of i Virtual Network Functions Request (VNFR) req(i) : V → L * Dependencies of the VNF i ∈ V ; defined as the incoming edges of a VNF and refer to outgoing links of other VNFs. This allows the specification of VNFs that get selectively deployed on specific sub-flows. An assignment of a VNF instance is only valid if traffic has first been routed through instances of all the required VNFs. Parameters M I(i) Minimum number of instances of the VNF i ∈ V in the VNF-FG G ext = (V ext , L ext ) This augmented graph is created from the VNFR. The final service chain (VNF-FG) will be a subgraph of G a V ext Set of nodes of the augmented graph, each node in V may have one or more instances in V ext L ext Set of links of the augmented graph Sets P Set of paths from the node in V ext that correspond to the instance of n init ∈ V to the set of instances of the terminating nodes N term in the augmented graph i m ∈ V ext : i ∈ N term P os p i m Position of the augmented node i m ∈ V ext in path p ∈ P , if i m is not part of the path, then 0 Augmented Graph δ p i m ,j n Binary parameter that indicates if augmented link (i m , j n ) ∈ L ext is part of path p Parameters y i,b i m ,j n Binary variable that says whether the link (i, b) ∈ L is mapped in the link (i m , j n ) ∈ L ext of the augmented network y i m ,j n Binary variable that says whether the link (i m , j n ) ∈ L ext of the augmented network is chosen as a part of the resulting VNF-FG x m i Binary variable that says whether the instance i m ∈ V ext of the augmented network is part of the resulting VNF-FG LD i,b i m ,j n (BW ) Bandwidth required by link (i, b) ∈ L assigned to (i m , j n ) ∈ L ext in the augmented network LD i m ,j n (BW ) Total bandwidth required by (i m , j n ) ∈ L ext in the augmented network T D i m (BW ) Total bandwidth arriving to node (i m ) in the augmented network z i,b i m ,j nAuxiliary variable to perform the following product between variables z iBinary variable that says whether the link (i, b) ∈ L : i ∈ V k is mapped in the link (i m , j n ) belonging to the path p of the augmented network u p

  Fig. 2: VNFR and Augmented Graph

Fig. 3 :

 3 Fig. 3: VNFR and Augmented Graph

Fig. 5 :

 5 Fig. 5: Total bandwidth demanded by VNF-FG

3 Fig. 6 :

 36 Figure5shows the comparison between the ILP model and the heuristic in the aforementioned scenarios. On the one hand, for scenarios where the traffic is split out into several links (e.g. VNFR 2), our solution yields better results than the VNF-FG of the heuristic, demanding around 5 Mbps less of the total bandwidth. On the other hand, for scenarios such as VNFR 1 as well as on each bifurcation of VNFR 3, where all the possible chains are disposed in a monotonic order, i.e., following and straight concatenation, both solutions yields same results in terms of demanded bandwidth.For VNFRs splitting the traffic into several bifurcations (e.g., scenarios VNFR 2 and VNFR 3), the ILP model would be able to obtain VNF-FGs with more than one instance of the same VNF for those cases in which such function must be performed by each sub-flow. This is the case of VNFR 2: for instance, where VNF 4 has to be performed by each sub-flow, our solution establishes that it must be implemented in two separately instances (one per sub-flow). Thus, the load of traffic arriving at VNF 4 is divided requiring less processing device capabilities into the physical network before the embedding process. As shown in Figure6b, VNF 4 in our ILP solution VNF 4 is created with two instances with incoming traffic loads of 400 Mbps and 600 Mbps respectively whereas the heuristic solution maps VNF 4 to the same instance for both sub-flows processing an incoming load traffic of 1Gbps. The fact that VNFs are created in more than one instance would facilitate the subsequent embedding phase of NFV-RA.Similarly, in VNFR 3, VNF 7 has to be located after all three sub-flows. Our ILP solution generates two instances of this function; instance 1 receives a load traffic of 400 Mbps from one sub-flow, while instance 2 receives a traffic load of 600-Mbps from two sub-flows, as shown in figure6c.In VNFR 1 where the VNF-FG in any combination is a monotonic graph without bifurcations, only one instance of each function is mapped. Figure6a

Table 1 :

 1 SFC Composition Inputs and Variables

http://www.etsi.org/deliver/etsi gs/NFV/001 099/003/01.02.01 60/gs NFV003v010201p.pdf

For the sake of clarity, directed links are drawn with arrows, so a link with arrows in its extremes a and b represents a pair of directed links; one from a to b, and the other from b to a

Acknowledgment

This work has been funded by COLCIENCIAS, the University of Antioquia and by the Flemish fund for scientific research (FWO) and the EMD and 5GUARDS project, co-funded by imec and VLAIO.

Finally, VFNR 3 is given for scenarios in the Gi Interface for mobile network environments. We define an scenario with seven VNFs disposed as follows: VNF 1 is the initial function to be performed, this function divides the incoming traffic into three sub-flows through three links with relative bandwidth demands of 20%, 40% and 40% respectively. VNF 2 depends on the first sub-flow while VNFs 3 and 4 depend on the second sub-flow and VNFs 5 and VNF 6 depend on the last sub-flow. Finally, Each sub-flow must to be processed by the terminal function VNF 7.

Results

The solution of our model is given in terms of a VNF-FG to be embedded on the physical network. The main objective is to find a VNF-FG with the minimal bandwidth demand on its links. Therefore, the objective function of our ILP is to minimize:

(i m ,j n )∈L ext LD i m ,j n (BW ) (25)


Noha Xue

Hårek Haugerud

Anis Yazidi

Towards a Hybrid Cloud Platform Using Apache Mesos

Keywords: Opensource Hybrid Cloud, Apache Mesos, Data Segmentation, Fault Tolerance

Hybrid cloud technology is becoming increasingly popular as it merges private and public clouds to bring the best of two worlds together. However, due to the heterogeneous cloud installation, facilitating a hybrid cloud setup is not simple. Despite the availability of some commercial solutions to build a hybrid cloud, an open source implementation is still unavailable. In this paper, we try to bridge the gap by providing an open source implementation by leveraging the power of Apache Mesos. We build a hybrid cloud on the top of multiple cloud platforms, private and public.

Introduction

The use of cloud computing is becoming more common, bringing along the advantages of flexibility and abundance of available resources, but also a higher degree of complexity along with privacy and security concerns. The concepts of multicloud and hybrid cloud are not new and several companies explore and capitalize these concepts. Most of the available solutions are commercial. Different vendors including Dell, IBM and HP provide hybrids cloud solutions [START_REF] Connor | Automated cloud brokerage based upon continuous real-time benchmarking[END_REF][START_REF] Breiter | A framework for controlling and managing hybrid cloud service integration[END_REF]. The MODAClouds project [START_REF] Modaclouds | [END_REF] utilizes several tools to provide an environment for utilizing multiple cloud providers. Several large companies are offering hybrid cloud solutions, often in conjunction with their existing product portfolio. VMWare is offering a hybrid cloud solution called vRealize suite which provides one interface to manage the entire hybrid cloud platform [START_REF] Vmware | [END_REF][START_REF][END_REF]. Other companies like Cisco [START_REF] Butler | Re-examining ciscos intercloud strategy[END_REF], IBM [START_REF]Private and hybrid cloud[END_REF] and RackSpace [START_REF]Hybrid cloud computing, hybrid hosting by rackspace[END_REF] are also offering hybrid cloud solutions. Another attempt addresses the challenges of managing heterogeneous virtual environments to create a hybrid cloud platform [START_REF] Breiter | A framework for controlling and managing hybrid cloud service integration[END_REF]. PaaSage is an interesting initiative for building a hybrid cloud solution using a defined deployment model, Cloud Application Modeling and Execution Language (CAMEL) [START_REF] Paasage | Paasage: Model-based cloud platform upperware[END_REF]. However, there has been no practical demonstration of using open-source and freely available clustering technology to attempt to address the multitude of challenges when creating a hybrid cloud platform that is available and supports data segmentation. This paper outlines an attempt to prototype such a solution in addition to facilitate cloud bursting using spot price instances. Borja et al. introduced OpenNebula in [START_REF] Borja | An open source solution for virtual infrastructure management in private and hybrid clouds[END_REF], which is one of the most popular open source Virtual Infrastructure Manager (VIM). OpenNebula permits to abstract resources of an existing local Grid and a cloud infrastructure. At the heart of OpenNebula we find Haizea [START_REF] Kovács | Modelling of virtualized servers[END_REF] which is a VM-based Lease Manager that enhances the resource scheduling manager with advanced reservation of resources and queueing of best effort requests. Nevertheless, OpenNebula suffers from the single point failure problem [START_REF] Feller | Snooze: A scalable and autonomic virtual machine management framework for private clouds[END_REF]. In this paper, we present a lightweight solution, that is tolerant to different failure scenarios. Similarly, it is also possible to create a Hybrid Cloud With AWS and Eucalyptus. This paper will explore and document the attempts at designing and prototyping a possible opensource solution for constructing a computer cluster built on top of private servers and external cloud providers.

2 Design and Implementation

An Apache Mesos cluster including both master nodes and slaves nodes were successfully installed and configured in Altocloud, with slave nodes correctly registering themselves to the cluster through the leading master node. However, when attempting to register a slave node running at Amazon Web Services EC2 peculiar activity was observed. The traffic from the slave node located at EC2 managed to successfully send a registration request to the leading master node, passing through multiple layers of network abstraction including two layers of NAT. Although the master node receives the registration requests, no registration acknowledge is ever sent back. Eventually, the cause was discovered to be a combination of the use of NAT and the way Mesos nodes communicates between each other. When a slave node sends a registration request, it includes information about the resources available and an IP-address. The IP-address sent along is the one that is defined on the network interface bound by the Apache Mesos process. Furthermore, in a cloud environment like Altocloud and Amazon Web Services EC2, the public IP-addresses are loosely coupled with the virtual machine and functions similarly as NAT does. Consequently, the Mesos master attempts to send the acknowledgement and other internal traffic meant for that slave node to the non-routable private IP-address. The communication flow is illustrated in Fig. 1 By using VPN tunneling, the need for allocating public IP-addresses for each node disappears for the purpose of maintaining the cluster, as the private IP-addresses becomes routable within the hybrid cloud platform. With the exception of the extra infrastructure to maintain a VPN, the prototype is identical to the proposed proposed design. Fig. 2

Test scenarios

A Mesos slave process becomes unavailable In the event of a Mesos slave node becoming unavailable for some reason, the Mesos master node allows a default timeout period of 75 seconds to pass before procedures for deactivating the slave node is begun. Should the slave node start responding within this timeout period, nothing will happen and both the Mesos master node and the slave node simply ignores the temporary unavailability.

However, if the timeout period is exceeded and the slave nodes is still unavailable, the Mesos master node will attempt to deactivate the Mesos slave process on the slave node before it from the list of available slave nodes. Tasks that were lost will be rescheduled to other slave nodes with available capacity.

Should a slave node simply be temporarily disconnected from the master node, but exceed the timeout period, the Mesos master will forcibly shut the Mesos slave node down. To account for such scenarios, the official Apache Mesos documentation recommends monitoring the Mesos slave process and restart if it should be terminated for any reason. In this case, this is achieved with a simple check using Monit. In Listing 1.1 log events of such a case is listed.

The working Mesos master instance cease to function ZooKeeper maintains an active connection to the participants of the quorum and will after a very short timeout lasting a few seconds, will initiate a new leader electing for choosing a new leading Mesos master node. As long as the number of functional Mesos master nodes is equal or higher than the quorum size, a new leader will be elected and will replace the unresponsive Mesos master node. This scenario was tested with a simple reboot of the instance where the leading Mesos master was running. The backup Mesos masters quickly discovers the loss of connection to the leading Mesos master and promptly, with the use of ZooKeeper elects a new leading Mesos master node. The rebooted Mesos master node later joins the cluster as a backup node after coming back online.

The setup proposed in this prototype has three Mesos master nodes, with the quorum size set to two. This means that among the Mesos master nodes, one can fail without crippling the cluster, as the quorum size dictates the number of election participants that has to be able to communicate to be able to elect a new leader.

An entire region within the hybrid cloud becomes unavailable If an entire region becomes unavailable, the Mesos nodes located within those regions will by extension also become unavailable. In this particular case, the loss of one single site equals the loss of one Mesos master node and four slave nodes. Each node, depending on the type, is handled as specified in the test scenarios mentioned above.

This was tested by taking down the VPN tunnels at the VPN gateway of the concerned region. This cuts all communication between the the affected region and the other ones. As expected the the Mesos master nodes continued without any issues, as the current leader was not the affected one. As for the affected Mesos slave nodes, after the timeout of 75 seconds, the leading Mesos master node determined that the slave nodes were unresponsive deactivated them.

The hybrid cloud splits and semi-isolates part of the platform In the event of split in the hybrid cloud, resulting in a partly isolated availability region, the quorum mechanics will prevent inconsistencies of the cluster and avoid issues like the split-brain problem.

To test this scenario, two simple iptables DROP rules was added on the Mesos master node located in Frankfurt with the IP address 192.168.0.5. The leading Mesos master node at the current time was 10.0.19.5, with nothing occurring immediately as a result of the iptables DROP rules. The leading master continued with no issues and other two standby Mesos masters correctly redirected to the leading master node. However, after rebooting the ZooKeeper process and Mesos master process on the master nodes, the cluster is unable to elect a new leader. Immediately after the iptables DROP rules were removed, a new leading Mesos master was elected and operations continued as normal.

Conclusion

This paper presents a prototype of a hybrid cloud platform using Apache Mesos to weave together heterogeneous clouds and geographical locations into a unified platform. The prototype proposed focuses on a specific perspective, namely, maximizing availability.

Fig. 1 .

 1 Fig. 1. Communication flow between an Apache Mesos slave node and master node with the registration attempt failing due to how public IP-addresses are handled in cloud platforms.

Fig. 2 .

 2 Fig. 2. Prototype 1: Maximizing availability. Distributing the master nodes and thereby the risks.

  iptables -A INPUT -s 10.0.19.5 -j DROP iptables -A OUTPUT -d 10.0.19.5 -j DROP

  .

	Slave	NAT	NAT	Master
	192.168.0.10	52.17.132.200	128.39.121.20	10.0.19.5
	From: 192.168.0.10
	To: 128.39.121.20
	Payload:
	Registration request
	I am 192.168.0.10	From: 52.17.132.200
		To: 128.39.121.20
		Payload:
		Registration request
		I am 192.168.0.10
			From: 52.17.132.200
			To: 10.0.19.5
			Payload:
			Registration request
			I am 192.168.0.10
			From: 10.0.19.5
			To: 192.168.0.10
			Payload:
			Registration acknowledged
		IP-address not routable

  1 17:34:23.298998 Shutting down slave ...5050-5669-S3 due to health check timeout 2 17:34:23.300134 Removing slave ...5050-5669-S3 at slave(1)@192.168.187.205:5051 (192.168.187.205) Excerpt from /var/log/mesos/mesos-master.INFO showing the forced shut down of the Mesos slave process at 192.168.187.205 and the registration as new slave at end. Truncated for increased readability.

	→
	3 17:34:23.301009 Removed slave 20150501-230056-2407081856-5050-5669-S3
	4 17:34:23.536837 Notifying framework ...5050-27030-0006 (marathon) at
	→	...473b-b57a-83121a00a01c@128.39.121.140:43217 of lost slave ...5050-5669-S3
	→	(192.168.187.205) after recovering
	5 17:34:29.017205 Slave ...5050-5669-S3 at slave(1)@192.168.187.205:5051 (192.168.187.205)
	→	attempted to re-register after removal; shutting it down
	6 17:34:57.329751 Registering slave at slave(1)@192.168.187.205:5051 (192.168.187 .205) with
		id ...5050-5669-S4

→

Listing 1.1:


Diego Figueira

Piotr Hofman

Sławomir Lasota

To appear in EPTCS. Relating timed and register automata *

Timed automata and register automata are well-known models of computation over timed and data words respectively. The former has clocks that allow to test the lapse of time between two events, whilst the latter includes registers that can store data values for later comparison. Although these two models behave in appearance differently, several decision problems have the same (un)decidability and complexity results for both models. As a prominent example, emptiness is decidable for alternating automata with one clock or register, both with non-primitive recursive complexity. This is not by chance.

This work confirms that there is indeed a tight relationship between the two models. We show that a run of a timed automaton can be simulated by a register automaton, and conversely that a run of a register automaton can be simulated by a timed automaton. Our results allow to transfer complexity and decidability results back and forth between these two kinds of models. We justify the usefulness of these reductions by obtaining new results on register automata.

Introduction

Timed automata [START_REF] Alur | A theory of timed automata[END_REF] and register automata (known originally as finite-memory automata) [START_REF] Kaminski | Finite-Memory Automata[END_REF] are two widely studied models of computation. Both models extend finite automata with a kind of storage: clocks in the case of timed automata, capable of measuring the amount of time elapsed from the moment they were reset; and registers in the case of register automata, capable of storing a data value for future comparison. In this paper we are interested in decidability and complexity of standard decision problems for both models of automata. In particular, we focus on the problems of nonemptiness (Does an automaton A accept some word?), universality (Does an automaton A accept all words?), and inclusion (Are all words accepted by an automaton A also accepted by an automaton B?).

The emptiness problem for nondeterministic timed or register automata is PSPACE-complete [START_REF] Alur | A theory of timed automata[END_REF][START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF]. It becomes undecidable for alternating automata of both kinds [START_REF] Lasota | Alternating timed automata[END_REF][START_REF] Ouaknine | On the Decidability of Metric Temporal Logic[END_REF][START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF], as soon as they have at least two clocks or registers [START_REF] Alur | A theory of timed automata[END_REF][START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF]. Even the universality problem was shown undecidable for nondeterministic timed and register automata, respectively, with two clocks or registers [START_REF] Alur | A theory of timed automata[END_REF][START_REF] Neven | Finite state machines for strings over infinite alphabets[END_REF][START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF]. A break-through result of [START_REF] Ouaknine | On the Language Inclusion Problem for Timed Automata: Closing a Decidability Gap[END_REF] showed that universality becomes decidable for one clock timed automata. Later, the emptiness problem for one clock alternating timed automata was shown decidable. However, the computational complexity of this problem has been found to be non-primitive recursive [START_REF] Lasota | Alternating timed automata[END_REF][START_REF] Ouaknine | On the Decidability of Metric Temporal Logic[END_REF]. Analogous (independent) results appeared for the other model: emptiness is decidable and non-primitive recursive for one register alternating automata [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF]. For infinite words, both one clock and one register alternating automata are undecidable, as well as the universality problem of nondeterministic one clock/register automata [START_REF] Lasota | Alternating timed automata[END_REF][START_REF] Parosh | Decidability and Complexity Results for Timed Automata via Channel Machines[END_REF][START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF]. The analogies between the two models appear to some extent also at the level of proof methods. The decidability proofs for one clock/register alternating automata are based on similar well-structured transition systems; and both non-primitive recursive lower bounds are obtained by simulation of a kind of lossy model of computation. All these analogies between the two models rise a natural question about the relationship between them. This paper is an attempt to answer this question.

Register automata were traditionally investigated over an unordered data domain. However, our model works on a data domain equipped with a total order. This is a necessary extension, that allows to simulate runs of timed automata, and to have a tight equivalence between the timed and the register models. Roughly speaking, the main contribution of this paper is to show that timed automata ≈ register automata over an ordered data domain. On a more technical level, we show that a run of a timed/register automaton on a timed/data word w may be simulated by a run of a register/timed automaton over a specially instrumented transformation of w, that we call braid. The reductions we exhibit are performed in exponential time, and keep the number of clocks equal to the number of registers, and preserve the mode of computation (alternating, nondeterministic, deterministic). Additionally, we show that the complement of all braids is recognizable by a nondeterministic one clock/register automaton. These results lead straightforwardly to reductions from decision problems for one class of automata to analogous problems for the other class, thus allowing us to carry over (un)decidability results and derive complexity bounds in both directions.

As an application, our simulations allow to obtain known results on timed (or register) models as simple consequences of results on register (or timed) models. These include, e.g., that over finite words the emptiness problem of alternating 1 register automata is decidable [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF]. In fact, our reductions yield decidability of the model extended with a total order over the data domain. As two further examples of application, we show how the following decidability results for timed automata can be transferred to the class of register automata:

• decidability of the inclusion problem between a nondeterministic (many clocks) automaton and an alternating one clock automaton (shown in [START_REF] Lasota | Alternating timed automata[END_REF]);

• decidability of the emptiness problem for an alternating (many clocks) automaton over a bounded time domain (shown in [START_REF] Jenkins | Alternating Timed Automata over Bounded Time[END_REF]). In this paper we limit our study to finite timed and data words, as the first step in the general program of relating the timed and data settings.

Preliminaries

R + denotes the set of non-negative real numbers. Let B + (X) denote the set of all positive boolean formulas over the set X of propositions, i.e., the set generated by:

φ ::= x | φ 1 ∧ φ 2 | φ 1 ∨ φ 2 (x ∈ X).
We fix a finite alphabet A for the sequel. We recall the definitions of alternating timed and register automata [START_REF] Lasota | Alternating timed automata[END_REF][START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF]. To avoid inessential technical complications, we have deliberately chosen a slightly unusual definition of register automata, equivalent in terms of expressible power to the one defined in [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF], but as similar as possible to the definition of timed automata.

Alternating timed automata

By a timed word over A we mean a finite sequence

w = (a 1 ,t 1 ) (a 2 ,t 2 ) . . . (a n ,t n ) (1)
of pairs from A × R + , with t 1 < t 2 < . . . < t n . Each time stamp t i denotes the amount of time elapsed since the beginning of the word. For simplicity, we prefer to work with strictly monotonic timed words, although the analogous results would hold for weakly monotonic words as well. For a given finite set C of clock variables (or clocks for short), consider the set Constr(C ) of clock constraints σ defined by

σ ::= c < k | c ≤ k | σ 1 ∧ σ 2 | ¬σ ,
where k stands for an arbitrary nonnegative integer constant, and c ∈ C . For instance, note that tt (standing for always true), or c = k, can be defined as abbreviations. Recall also that the difference constraints c 1c 2 ≤ k, typically allowed in timed automata, may be easily eliminated (however, the size of automaton may increase exponentially). A valuation of the clocks is an element v ∈ (R + ) C . Given a constraint σ we write [σ ] to denote the set of clock valuations satisfying the constraint,

[σ ] ⊆ (R + ) C .
An alternating timed automaton over A consists of: a finite set of states Q, a distinguished initial state q 0 ∈ Q, a set of accepting states F ⊆ Q, a finite set C of clocks, and a finite partial transition function

δ : Q × A × Constr(C ) • → B + (Q × P(C )),
subject to the following additional restriction: (Partition) For every state q and label a,

{[σ ] : δ (q, a, σ ) is defined} is a (finite) partition of (R + ) C .
The (Partition) condition does not limit the expressive power of automata. We impose it because it permits to give a nice symmetric semantics for the automata as explained below. We will write q, a, σ → b instead of δ (q, a, σ ) = b.

To define an execution of an automaton, we will need two operations on valuations v ∈ (R + ) C . A valuation v+t, for t ∈ R + , is obtained from v by increasing the value of each clock by t. A valuation v[X := 0], for X ⊆ C , is obtained by reseting to zero the value of all clocks from X.

For an alternating timed automaton A and a timed word w as in (1), we define the acceptance game G time A ,w between two players Adam and Eve. Intuitively, the objective of Eve is to accept w, while the aim of Adam is the opposite. A play starts at the initial configuration (q 0 , v 0 ), where v 0 : C → R + is a valuation assigning 0 to each clock variable. It consists of n phases. The (k+1)-th phase starts in (q k , v k ), and ends in some configuration (q k+1 , v k+1 ) proceeding as follows. Let v := v k + t k+1t k (for k = 0, t 0 is deemed to be 0). Let σ be the unique constraint such that v satisfies σ and φ = δ (q k , a k+1 , σ ) is defined. Existence and uniqueness of such σ is implied by the (Partition) condition. Now the outcome of the phase is determined by the formula φ . There are three cases:

• φ = φ 1 ∧ φ 2 : Adam chooses one of subformulas φ 1 , φ 2 and the play continues with φ replaced by the chosen subformula;

• φ = φ 1 ∨ φ 2 : dually, Eve chooses one of subformulas;

• φ = (q, X) ∈ Q × P(C ): the phase ends with the result (q k+1 , v k+1 ) := (q, v[X := 0]). A new phase is starting from this configuration if k+1 < n.

The winner is Eve if q n is accepting (q n ∈ F), otherwise Adam wins. Formally, a play is a finite sequence of consecutive game positions of the form k, q, v or k, q, φ , where k is the phase number, φ a positive boolean formula, q a state and v a valuation. A strategy of Eve is a mapping which assigns to each such sequence ending in Eve's position a next move of Eve. A strategy is winning if Eve wins whenever she applies this strategy.

The automaton A accepts w iff Eve has a winning strategy in the game G time A ,w . By L (A ) we denote the language of all timed words w accepted by A .

Alternating register automata

Fix an infinite data domain D. Data words over A are finite sequences

w = (a 1 , d 1 )(a 2 , d 2 ) . . . (a n , d n ) (2)
of pairs from A × D. Additionally, assume a total order over D. The order may be chosen arbitrarily, and our results apply to all total orders. For a given finite set R of register names (or registers for short), consider the set Tests(R) of register tests σ defined by

σ ::= ≺ r | r | σ 1 ∧ σ 2 | ¬σ , where r ∈ R.
Each test σ refers to registers and the current data, thus σ denotes a subset

[σ ] of D R × D. E.g., [≺ r]
means that the current data value is strictly smaller than the value stored in register r. The equality '= r' and inequality ' = r' tests may be defined as abbreviations.

An alternating register automaton over A consists of: a finite set Q of states with a distinguished initial state q 0 ∈ Q and a set of accepting states F ⊆ Q, a finite set R of registers, and a transition function

δ : Q × A × Tests(R) → B + (Q×P(R))
subject to the following additional restriction:

(Partition) For every q and a, the set {[σ ] : δ (q, a, σ ) is defined} gives a (finite) partition of D R × D.

Register automata are typically defined over unordered data domain. For the purpose of relating the existing models, distinguish a subclass of register automata that only use equality = r and inequality = r tests; we call them order-blind automata. Order-blind automata correspond to the model defined in [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF]. As usual, we will write q, a,t → φ instead of δ (q, a,t) = φ .

Given a data word w as in [START_REF] Alur | A theory of timed automata[END_REF], it is accepted or not by A depending on the winner in the acceptance game G data A ,w , played by Eve and Adam similarly as for timed automata. We assume for convenience that as the very first step the automaton loads the current data into all registers (in this way we avoid undefined values in registers). The initial configuration is thus (q 0 , v 0 ), where v 0 : R → D assigns d 1 to each register. The play consists of n phases. The (k+1)-th phase starts in (q k , v k ) and proceeds as follows. Let σ be the unique test such that v k satisfies σ and φ = δ (q k , a k+1 , σ ) is defined (recall the (Partition) condition). Now the outcome of the phase is determined by the formula φ . The logical connectives are dealt with analogously as in case of timed automata. When the play reaches an atomic formula φ = (q, X) ∈ Q × P(R), the phase ends with the result

(q k+1 , v k+1 ) := (q, v k [X := d k+1 ]), where v[X := d] differs from v by setting v(r) = d for all r ∈ X. If k+1 < n, the game continues with a new phase starting in (q k+1 , v k+1 ).
The winner is Eve if q n is accepting (q n ∈ F), otherwise Adam wins. The automaton A accepts w iff Eve has a winning strategy in G data A ,w . Overloading the notation, L (A ) denotes the language of all data words accepted by A .

Deterministic, nondeterministic, and alternating. For both timed and register automata, we distinguish a subclass of nondeterministic automata as those that do not use conjunction in the image of transition function, and a subclass of deterministic automata that do not use disjunction either. The term alternating automata refers then to the full, unrestricted class.

Isomorphisms

By a time isomorphism we mean any order-preserving bijection f over the interval [0, 1) (this implies f (0) = 0 in particular). The intuition is that an isomorphism will not be applied to a time stamp t, but to its fractional part only (that we write t ), keeping the integer part t unchanged.

Given a time isomorphism f , we apply it to a timed word w = (a 1 ,t 1 ) • • • (a n ,t n ) as follows:

f (w) = (a 1 , t 1 + f ( t 1 ))(a 2 , t 2 + f ( t 2 )) • • • (a n , t n + f ( t n ))
Proposition 2.1. Languages recognized by alternating timed automata are closed under time isomorphism: for any timed automaton A and a time isomorphism f , A accepts a timed word w iff A accepts f (w).

We say that two data words w = (a

1 , d 1 )(a 2 , d 2 ) . . . (a n , d n ) and v = (a 1 , e 1 )(a 2 , e 2 ) .
. . (a n , e n ) with the same string projection a 1 a 2 . . . a n are data isomorphic if for all i, j ∈ {1 . . . n}, d i d j iff e i e j . Proposition 2.2. Languages recognized by alternating register automata are closed under data isomorphism: for any register automaton A and a two data isomorphic words w and v, A accepts w iff A accepts v.

Braids

An idea which is crucial to obtain reductions in both directions is an instrumentation of timed and data words, to be defined in this section, that enforces a kind of 'braid' structure in a word.

Data braids. The data projection

of w = (a 1 , d 1 ) . . . (a n , d n ) ∈ (A × D) * is d 1 . . . d n ∈ D * .
We define the ordered partition of a data word w as a factorization

w 1 • . . . • w k = w (3)
into data words w 1 , . . . , w k such that each w i is a maximal subword ordered with respect to ≺. In other words: all the data values of any w i are strictly increasing, and for all i < k, the first data value of w i+1 is less or equal to the last one of w i . It follows that for every data word there is a unique ordered partition.

A data word w is a data braid iff • The minimum data value of w appears at the first position, and

• Its ordered partition is such that the data projection of each factor w i is a substring of the data projection of w i+1 . In this context, we say that v is a substring of v iff v is the result of removing some (possibly none) positions from v .

• We can partition the alphabet

A = A 1 ∪ A 2 so that a position i of w is labeled with a symbol of A 2 iff d i = d 1 .
We call a marked position to any A 2 -labeled position of the word. Note that the marked positions are those starting some factor of the ordered partition of w. Example 3.1. The word w below is not an ordered data braid since its ordered partition does not satisfy the substring requirement. Neither is v, since the minimum element does not appear at the first position. In this example as well as in the following ones we use natural number as exemplary data value.

w = (c, 1) • (d, 1)(a, 4)(b, 8) • (c, 1)(b, 2)(a, 4)(a, 8)(b, 9) • (c, 1), v = (c, 3) • (d, 2)(a, 3)(b, 8) • (c, 2)(b, 3)(a, 5)(a, 8).
In the case of w, the substring requirement is fulfilled if, e.g., the last element (c, 1) is removed, or when w is extended with (b, 2)(a, 4)(b, 5)(a, 8)(b, 9); in both cases A 1 = {a, b} and A 2 = {c, d}. Timed braids. Intuitively, the braid condition for timed words is analogous to that of ordered data braids if one considers the fractional part of a time stamp t i as datum. A timed word w = (a 1 ,t 1 )(a 2 ,t 2 ) . . . (a n ,t n ) is a timed braid if the very first time stamp equals zero, t 1 = 0, and moreover

• for all i < n, if t i < t n then t i + 1 appears among t i+1 . . . t n ,

• the alphabet can be partitioned into A = A 1 ∪ A 2 so that the marked positions (i.e., those labeled by A 2 ) are precisely those carrying integer time stamp. Braids will play a central role in the following section. In fact both data braids and timed braids represent essentially the same concept, disregarding some minor details, as illustrated next. Example 3.2. We show a data braid w and a 'corresponding' timed braid v. A 1 = {a, b} and

A 2 = { ā, b}. w = ( b, 2)(a, 4) • ( ā, 2)(b, 4)(b, 8) • ( b, 2)(b, 3)(a, 4)(a, 8)(b, 9) v = ( b, 0.0)(a, 0.5) • ( ā, 1.0)(b, 1.5)(b, 1.6) • ( b, 2.0)(b, 2.3)(a, 2.5)(a, 2.6)(b, 2.9).
The particular data values and time stamps are exemplary ones. A canonical way of obtaining a timed braid from a data braid (and vice versa), to be explained below, will be ambiguous up to time (data) isomorphism.

Transformations. We introduce two simple encodings: one maps a timed word into a data braid, and the other maps a data word into a timed braid. A data word w over A may be canonically extended to a data braid db(w) over the alphabet A ∪ { } ∪ Ā ∪ { ¯ } as follows. Consider the ordered partition w = w 1 • . . . • w n and let d min be the smallest datum appearing in w. Firstly, for every factor w i , add the pair ( , d min ) at the very first position of w i , unless w i already contains the datum d min . Secondly, for each datum d appearing in any w i , add ( , d) to each of the following factors w i+1 . . . w n that do not contain d. This insertion is done preserving the order of the factor. Finally, change every symbol a at the first position of a factor by its 'marked' counterpart ā ∈ Ā ∪ { ¯ }. Note that as a result we obtain a data braid. Example 3.3. As an illustration, consider the effect of the above transformations on an exemplary data word w and a timed word v.

w = (a, 4) • (b, 1)(a, 4)(b, 8) • (a, 1)(a, 5)(a, 8) db(w) = ( ¯ , 1)(a, 4) • ( b, 1)(a, 4)(b, 8) • ( ā, 1)( , 4)(a, 5)(a, 8) v = (a, 0.0)(a, 0.7) • (b, 1.5) • (b, 2.0) tb(v) = ( ā, 0.0)(a, 0.7) • ( ¯ , 1.0)(b, 1.5)( , 1.7) • ( b, 2.0)( , 2.5)( , 2 .7)
We have thus explained the horizontal arrows of the diagram, and now we move to the vertical ones. Both mappings preserve the length of the word.

A timed braid (a 1 ,t 1 ) . . . (a n ,t n ) gives naturally rise to a data braid by replacing each time stamp t i by its fractional part t i , and then mapping the set { t 1 , . . . , t n } into the data domain D through an orderpreserving injection. We only want to consider order-preserving injections, thus this always yields a data braid. Note that the choice of a particular order-preserving injection is irrelevant, as one always obtains the same data word up to data isomorphism (cf. Proposition 2.2). We hope this ambiguity will not be confusing.

A data braid w = (a 1 , d 1 ) • • • (a n , d n ) may be turned into a timed braid through any order-preserving injection f : {d 1 , . . . ,

d n } → [0, 1) such that f (d 1 ) = 0. Each element (a i , d i ) is mapped into a similar element (a i , k + f (d i )),
where k is the number of factors (in the ordered partition of w) that end strictly before position i. Consecutive factors will get consecutive natural numbers as the integer part of time stamps. As before, we consider the choice of a particular injection f irrelevant (cf. Proposition 2.1).

Notice that going from a timed braid to a data braid and back returns to the original word up to time isomorphism; likewise, combining the transformations in the reverse order we get back to the same word, up to data isomorphism.

Slightly overloading the notation, we write db(w) to denote the data braid obtained from a timed word w by the appropriate composition of transformations just described. Similarly, we write tb(w) to denote the timed braid obtained from a data word w.

From timed automata to register automata

We are going to show that, up to a suitable encoding, languages recognized by timed automata are recognized by register automata as well. The transformation keeps the number of registers equal to the number of clocks, and preserve the mode of computation (nondeterministic, alternating). Theorem 4.1. Given an alternating timed automaton A one can compute in exponential time an orderblind register automaton B such that for any timed word w, A accepts w if an only if B accepts db(w). The number of registers of B equals the number of clocks of A . Moreover, B is deterministic (resp. nondeterministic, alternating) if A is so.

Proof. We describe the construction of a register automaton B that faithfully simulates a given timed automaton A . The idea is that the behavior of each clock can be simulated by a register. When the clock is reset on one automaton, the other loads the current data value d into the register. Then, by the data braid structure, the register automaton knows exactly how many units of time have elapsed for the clock by simply counting the number of times that d has appeared.

Consider the maximum constant k max that appears in the transition rules of A . Let Q and C denote the states and clocks of A , respectively. The states of B will be Q × {0, 1, . . . , k max } C . Intuitively, for each clock c the automaton B stores the information about the integer part c of current value of c, up to k max . In other words, B keeps the count of how many times (up to k max ) the value stored in c appeared in the word since it was stored. The initial state is (q 0 , v) where v assigns 0 to each c ∈ C . Recall that it is assumed that as the very first step the automaton loads the current data into all registers.

There will be as many registers in B as clocks in A , R = C , and each register c will be used to update the information about the integer part of the value of c. Whenever the clock c is reset in A , the corresponding action of B is to store the current value in the register c and to change state from (q, v) to (q, v c ), where v c differs from v by assigning v c (c) = 0. The automaton B will also be capable to detect that the integer part of c increases. Whenever the equality test = c succeeds (recall that B is supposed to run over a data braid) and v(c) < k max , the state is changed from (q, v) to (q, v c ), where v c differs from v by assigning v c (c) = v(c) + 1. On the other hand, v is not changed when v(c) = k max . Now we describe the transitions of B in more detail. The automaton does not distinguish marked symbols from unmarked ones. If the current letter is or ¯ , then B only needs to update the v part of its state (q, v). Note that in this model many registers may store the same data value, and then there will be a transition in B for each vector v ∈ {0, 1, . . . , k max } C and subset X ⊆ C :

(q, v), a, c∈X = c ∧ c / ∈X = c → ((q, v X ), X) for a ∈ { , ¯ }. ( 4
)
where v X is defined by:

v X (c) = v(c) + 1 if c ∈ X and v(c) < k max v(c) otherwise.
Otherwise, when the current letter a is different from , ¯ , the automaton B simultaneously updates v similarly as above and simulates an actual step of A . Consider any transition q, a, σ → φ (5) of A . We describe the corresponding transitions of B. There are many of them, each of them induced by v and X similarly as above. They are of the following form:

(q, v), a, c∈X = c ∧ c / ∈X = c → φ X v for a ∈ A ∪ Ā, (6)
where φ X v is appropriately obtained from φ to ensure that the set of clocks reset by A is the same as the set of registers to which B loads the current value, and that the new vector v keeps up-to-date information about the integer parts of clock values. Let us describe how to build φ X v more precisely. Consider any fixed vector v ∈ {0, 1, . . . , k max } C and X ⊆ C . Being in state (q, v) and reading a next letter a, the automaton assumes that the clock c has a value in (v(c), v(c)

+ 1] if v(c) < k max , or in (k max , ∞) if v(c) = k max .
Further, if a clock c verifies c ∈ X, it means that the value of the corresponding register c equals to the current datum. This translates in an integer number of units of time elapsed for the clock c, and the exact number (up to k max ) is given by v(c) + 1. The pair [v, X] induces a subset of (R + ) C (keep in mind that the test in (6) holds) containing all vectors z such that for each clock c,

z(c) = v(c) + 1 iff c ∈ X and v(c) < k max , v(c) < z(c) < v(c) + 1 iff c / ∈ X and v(c) < k max , z(c) > k max iff v(c) = k max . Recall that [σ ] is also a subset of (R + ) C . If [v, X] ∩ [σ ] = / 0, the transition (6) is added to B. The action φ X v of B is derived from φ by replacing each pair (p,Y ) ∈ Q × P(C ) appearing in φ with ((p, v Y ),Y )
, where v Y is obtained from v X by setting v Y (c) = 0 for all c ∈ Y . Note that the structure of logical connectives in φ X v is the same as in φ . A careful examination of the above construction reveals that the initial configuration of the automaton B should be treated differently, as no modification of v should be done in this case. We omit the details.

The automaton B is order-blind as required. It is deterministic (resp. nondeterministic, alternating) whenever the automaton A is so. The size of B may be exponential with respect to the size of A , as the number of different sets X considered in ( 4) and ( 6) is exponential.

Example 4.2. As an illustration, consider the nondeterministic one clock timed automaton that checks that there are two time stamps whose difference is 1 depicted in Figure 1. Nondeterminism is represented by separate arrows in the automaton instead of disjunctive formulae. For the sake of clarity, we omit some (non-accepting) transitions that would have to be added in order to fulfill the (Partition) condition. The

q start p a tt reset {c} a tt reset / 0 a c = 1 reset / 0 a tt reset / 0
Figure 1: An automaton checking that there are two timestamp whose difference is 1.

construction described in the proof of Theorem 4.1 yields the order-blind register automaton of Figure 2. For the next results, we make use of the following Lemma. • there is some marked (i.e., carrying an alphabet letter from Ā∪ ¯ ) position i+1 such that d i ≺ d i+1 ,

q, 0 start q, 1 p, 0 p, 1 , ¯ , a, ā = c load / 0 , ¯ , a, ā = c load / 0 , ¯ , a, ā = c load / 0 , ¯ , a, ā = c load / 0 , ¯ , a, ā = c load / 0 , ¯ , a, ā = c load / 0 , ¯ , a, ā = c load / 0 , ¯ , a, ā = c load / 0 a, ā tt load {c} a, ā tt load {c} a, ā = c load {c}
• there is some unmarked position i + 1 such that d i d i+1 ,

• some datum strictly smaller than d 1 appears in w, or

• for some position i, there are two marked positions j < k, both greater than i, such that d i does not appear among {d j . . . d k }; or if d i does not appear after the last marked position.

A nondeterministic automaton can easily guess which of these conditions fails and verify it using one register.

As a consequence of Lemma 4.3, the language of data braids is recognized by an alternating one register automaton. This is due to the fact that this model is closed under complementation.

We want to use Theorem 4.1 together with Lemma 4.3 to show Theorem 4.4 below. However, there is a subtle point here: by Lemma 4.3 register automata can recognize the complement of data braids, while we would need register automata to recognize the complement of the image of db( ) (a different language, since db( ) is not surjective). Unfortunately, the model cannot recognize such a language. In the proof below we deal with this problem by observing that db( ) is essentially surjective onto data braids. Theorem 4.4. The following decision problems for timed automata: language inclusion, language equality, nonemptiness and universality, reduce to the analogous problems for register automata. The reductions keep the number of registers equal to the number of clocks, and preserve the mode of computation (nondeterministic, alternating) of the input automaton.

Proof. Consider the inclusion problem only, the other reductions are obtained in the same way. Given two timed automata A and B, nondeterministic or alternating, we apply Theorem 4.1 to obtain two corresponding register automata A and B . We claim that, for A ¬db given by Lemma 4.3, it holds: Proof of Claim 4.4.1. If the mapping db( ) was surjective onto data braids (up to isomorphism), then w would be equal to db(v) (up to isomorphism) for some v. This is however not the case! For example, consider appending ( , d) for a sufficiently big d at the end of db(v). We then obtain a data braid which is not equal to db(v) for any v. But notice that in fact this last position is useless for A and B .

L (A ) ⊆ L (B) if and only if L (A ) ⊆ L (B ) ∪ L (A ¬db ). (if) This implication is easy. Assume L (A ) ⊆ L (B ) ∪ L (A ¬db
A position i in a data braid w is considered useless iff (i) it is labeled by ( , d), for some datum d, and all appearances of the datum d before i are labeled with ; or (ii) all the positions in its factor and in all following factors are labeled exclusively with or ¯ . Let w denote the result of removing all useless positions from w. We then have the following.

w equals to db(v), up to isomorphism, for some timed word v.

Consider any order preserving injection f from data values appearing in w to [0, 1), and let v be the result of the following steps: (1) i.e., replace every

(a i , d i ) of w with (a i , k + f (d i )),
where k is the number of factors in w that end before position i; (2) remove all / ¯ positions; and (3) project the alphabet into A.

By definition of db( ), db(v) is, up to isomorphism, equal to w. Thus, A and B do not distinguish between w and db(v). It only remains to show that A and B do not distinguish between w and w.

Each of A , B either accepts both w and w, or none of them. This is true by construction, since when the input letter is , the register automaton A (or B ) only updates the information about the integer part of those clocks c for which the equality test = c holds. When reading a useless position, if it is useless because of (i), then the equality holds for no clock; whereas in case (ii) the update will be inessential for the acceptance. This completes the proof of the claim as well as the proof of the theorem.

From register automata to timed automata

In this section we complete the relation between the models of automata. We show that, up to a suitable encoding, languages of register automata may be recognized by timed automata. Again, this transformation keeps the number of registers equal to the number of clocks, and preserves the mode of computation (nondeterministic, alternating). Thus we obtain a tight relationship between the two classes of automata.

Theorem 5.1. Given an alternating register automaton A one can compute in exponential time a timed automaton B such that for any data word w, A accepts w if and only if B accepts tb(w). The number of clocks of B equals the number of registers of A . Moreover, B is deterministic (resp. nondeterministic, alternating) if A is so.

Proof. We describe the construction of a timed automaton B that faithfully simulates the behavior of a given register automaton A . Let R be the set of registers of A . The number clocks in B is the same as the number of registers in A , C = R. A clock r is reset whenever A loads the current data value into register r. Moreover, each clock is also reset whenever the constraint r = 1 is met. Thus, when B runs over a time braid, no clock will ever have value greater than 1.

The state space of B is built on top of the states Q of A . Additionally, for each clock r the automaton B stores in its state one bit of information describing whether the last marked position was seen before or after the last reset of r. This will allow B to simulate tests comparing the current data value with data values stored in registers.

Formally, states of B are pairs (q, X) ∈ Q × P(R). Initially the set X, which we call the register component of a state, is chosen as X = R (according to the assumption that the register automaton loads the first datum into all its registers as its very first action). At each marked symbol ā or ¯ , the automaton B sets X := / 0. Moreover, at each reset of r (at marked or unmarked positions), r is added to X. As a consequence of this behavior, it invariantly holds: r ∈ X if and only if the position of the last reset of r is greater or equal to the last marked position. Hence, the test r (current data smaller or equal to register r) is satisfied at a state (q, X) if and only if r / ∈ X. The table below summarizes all the atomic tests and the corresponding constraints on clock values and on the register component of state:

test in A meaning constraint in B r
current datum smaller or equal to r r / ∈ X ≺ r current datum smaller than r r / ∈ X and r = 1 r current datum greater or equal to r r ∈ X or r = 1 r current datum greater than r r ∈ X

We just described how the register component of a state is updated and when the clocks are reset. At input letter or ¯ this is the only the automaton B has to do. Each transition q, a,t → b of A with a ∈ A gives raise to a number of transitions (q, X), a, σ → b and (q, X), ā, σ → b of B that additionally keep track of the change of state of A and of load operations performed by A , as described above. The register test t gives raise to a clock constraint σ as described in the table above. The structure of logical connectives in b is the same as in b, hence B is deterministic (resp. nondeterministic, alternating) whenever A is so.

Example 5.2. Consider the simple nondeterministic one register automaton that checks if the first datum in a word is equal to the last one depicted in Figure 3. Similarly as before, the (Partition) condition is not satisfied as some (non-accepting) transitions are missing. The construction in the proof of Theorem yields the automaton of Figure 4. For the next results, we make use of the following Lemma.

p, 0 p, 1 start q, 0 q, 1 s, 0 s, 1 r = 1 reset {r} r < 1 reset / 0 ¯ r = 1 reset {r} ¯ r < 1 reset / 0 r < 1 reset / 0 a, r = 1 reset {r} a, r < 1 reset / 0 ā, ¯ r = 1 reset {r} ā, ¯ r < 1 reset / 0 a, r < 1 reset / 0 r = 1 reset {r} r < 1 reset / 0 ¯ r = 1 reset {r} ¯ r < 1 reset / 0 r < 1 reset / 0 a, ā tt reset {r} a tt reset {r} a r = 1 reset {r} ā r = 1 reset {r}
Lemma 5.3. The complement of the language of timed braids is recognized by a nondeterministic one clock automaton.

Proof. A timed word fails to be a timed braid iff: (0) the time-stamp in the first position is not equal 0;

(1) there is some marked position appearing at some non-integer position; (2) there is some unmarked position appearing at some integer position; (3) there is some missing position with time-stamp t induced by the existence of an element (a,t -1.0) for some a.

It is easy to check that (0), ( 1) and ( 2) can be verified by a deterministic one clock automaton. ( 3) is verified as follows. The automaton guesses a position i, where it resets the clock. Then it checks that after the next marked position, the clock is continuously strictly smaller than 1 until it finally becomes strictly greater than 1, or the word ends.

As a consequence of Lemma 5.3, the language of timed braids is recognized by an alternating one clock automaton. This is due to the fact that this model is closed under complementation.

The following theorem is proved analogously to Theorem 4.4, using Theorem 5.1 and Lemma 5.3:

Theorem 5.4. The following decision problems for register automata: language inclusion, language equality, nonemptiness and universality, reduce to the analogous problems for timed automata. The reductions keep the number of clocks equal the number of registers, and preserve the mode of computation (nondeterministic, alternating) of the input automata.

Sketch. The proof is very similar to the proof of Theorem 4.4. We need to deal with a minor difficulty of the same kind: the mapping tb( ) is not surjective, up to isomorphism, onto timed braids. Thus we need the following claim, similar to one used in the proof of Theorem 4.4:

Claim 5.4.1. For each timed braid w there is a data word v such that the automata A and B cannot distinguish between w and tb(v).

The claim is demonstrated similarly as before, by identifying useless positions in a timed braid. First, a position i is useless iff (1) it is labeled with ( ,t), for some (necessarily non-integer) t, and all positions before i carrying time-stamps with the same fractional part as t are labeled with ; or (2) position i carries time stamp t and all positions carrying time-stamps in the interval [t,t + 1) are labeled exclusively with or ¯ .

Similarly as before, the automaton obtained by Theorem 5.1 cannot tell the difference when all useless positions are removed from a word. To see this, observe that in case (1) no clock will be reset as the constraint r = 1 will not hold for any clock r. In case (2), the whole segment of length 1 labeled exclusively by and ¯ may be safely skipped as it has no impact on state of the automaton.

Applications

Here we provide some evidence that the tight relationship between register automata and timed automata may be useful: we transfer a couple of results from timed do data setting. First, from the fact that 1-clock alternating timed automata have decidable emptiness [START_REF] Lasota | Alternating timed automata[END_REF], applying Theorem 5.4 we obtain: Theorem 6.1. The emptiness problem for alternating one register automata is decidable.

Note that register automata, as we define it here, work over ordered data domains and are capable of comparing data values w.r.t. . According to our terminology, decidability was only known for the subclass of order-blind automata [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF]. Interestingly, the results holds for any total order over data.

A note on complexity Note that alternating 1 register automata over an ordered domain have the same complexity (modulo an exponential time reduction) as alternating 1 clock timed automata. However, we must remark that these automata have a much higher complexity than order blind alternating 1 register automata, although both are beyond the primitive recursive functions. While the latter can be roughly bounded by the Ackermann function applied to the number of states, the complexity of the former majorizes every multiply-recursive function (in particular, Ackermann's).

More precisely, the emptiness problem for alternating timed automata with 1 clock sits in the class F ω ω in the Fast Growing Hierarchy [START_REF] Löb | Hierarchies of number theoretic functions[END_REF]-an extension of the Grzegorczyk Hierarchy for non-primitive recursive functions-by a reduction to Lossy Channel Machines [START_REF] Parosh | Decidability and Complexity Results for Timed Automata via Channel Machines[END_REF], which are known to be 'complete' for this class, i.e. in F ω ω \ F <ω ω [START_REF] Chambart | The Ordinal Recursive Complexity of Lossy Channel Systems[END_REF]. However, the emptiness problem for order blind alternating 1 register automata belongs to F ω in the hierarchy, by a reduction to Incrementing Counter Automata [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF], which are complete for F ω [START_REF] Schnoebelen | Revisiting Ackermann-hardness for lossy counter systems and reset Petri nets[END_REF][START_REF] Figueira | Ackermann and Primitive-Recursive Bounds with Dickson's Lemma[END_REF]. We then obtain the following result. Corollary 6.2. The emptiness problem of alternating 1 register automata over a linearly ordered domain is in F ω ω \ F <ω ω in the Fast Growing Hierarchy.

We show another example of a result that can be directly copied from the timed to the data setting: Theorem 6.3. Consider the following inclusion problem: Given a nondeterministic register automaton A (with possibly many registers) and an alternating one register automaton B, is every word accepted by A also accepted by B? This problem is decidable and of non-primitive recursive complexity.

The result is immediate as the analogous problem is decidable and non-primitive recursive for timed automata [START_REF] Lasota | Alternating timed automata[END_REF]. Decidability follows from Theorem 5.4 while the lower bound follows from Theorem 4.4.

As the last example of application of our results, we consider the emptiness problem over a restricted class of data words. We say that a data word (a 1 , d 1 ) . . . (a n , d n ) is m-decreasing iff there are at most m -1 positions i with d i d i+1 . Theorem 6.4. Let m be a fixed nonnegative number. The non-emptiness problem for alternating register automata over m-decreasing data words is decidable and non-elementary.

Again, the result is an immediate consequence of the result of [START_REF] Jenkins | Alternating Timed Automata over Bounded Time[END_REF]: emptiness of alternating timed automata over m-bounded timed words is decidable and non-elementary, where m-bounded words are those with all time stamps smaller than m. The upper bound follows by Theorem 5.1 and from the fact that a data word w is m-decreasing iff tb(w) is m-bounded. Conversely, the lower bound follows from Theorem 4.1 and from the symmetric fact: a timed word is m-bounded iff db(w) is m-decreasing.

Finally, note that the upper (decidability) bounds of Theorems 6.3 and 6.4 also apply to the class of order-blind register automata.

Discussion

We have shown that timed and register automata on finite words are essentially equivalent. In order to relate these two models we introduced the notion of a 'braid'-like structure, that corresponds naturally to the way a clock works when running over a timed word. As shown, most decision problems are actually equivalent for these two models. This work can be useful to derive results on one model of automata as corollaries of results on the other model, by exploiting the duality between timed and data automata shown here. This is evidenced here by showing some new results (Section 6). One limitation of our results is the both translations between timed and register automata suffer of an exponential blow-up in the size of the automaton. As a consequence, one should not expect applicability to low-complexity problems, like non-emptiness of timed or register automata, in both cases a PSPACE-complete problem.

As a relatively straightforward further step, we plan to investigate automata over ω-words; in particular, we hope for transferring results of [START_REF] Parys | Weak Alternating Timed Automata[END_REF][START_REF] Ouaknine | Safety Metric Temporal Logic Is Fully Decidable[END_REF] to register automata and for comparing them e.g. with those of [START_REF] Lazić | Safety alternating automata on data words[END_REF]. It seems however that one must restrict to dense orders on data domain for proper treatment of infinite words. Furthermore, we also plan to attempt a similar comparison of logical formalisms, namely of freeze LTL and MTL or TPTL, both over finite and ω-words. This should allow to compare or transfer the complexity result for syntactic fragments of freeze LTL and MTL that appeared recently in the literature, see e.g. [START_REF] Parys | Weak Alternating Timed Automata[END_REF][START_REF] Ouaknine | Safety Metric Temporal Logic Is Fully Decidable[END_REF][START_REF] Lazić | Safely Freezing LTL[END_REF][START_REF] Figueira | Future-Looking Logics on Data Words and Trees[END_REF].

  timed words / / timed braids O O data words / / data braids A timed word w over an alphabet A induces a timed braid tb(w) over the extended alphabet A ∪ { } ∪ Ā ∪ { ¯ }, where Ā = { ā | a ∈ A}, as follows. First, if t 1 = 0, add the pair ( , 0) at the very first position. Then add pairs ( ,t) at all time points t that are missing according to the definition of timed braid. Finally change every symbol a at each position carrying an integer time stamp by its 'marked' counterpart ā ∈ Ā ∪ { ¯ }.

Figure 2 :

 2 Figure 2: The automaton resulting from the construction of Theorem 4.1.

Lemma 4 . 3 .

 43 The complement of the language of data braids is recognized by a nondeterministic one register automaton.Proof. A data word w = (a 1 , d 1 ) • • • (a n , d n ) fails to be a data braid iff either

  ) and let w ∈ L (A ). By Theorem 4.1 db(w) ∈ L (A ) and hence db(w) ∈ L (B ). Again by Theorem 4.1 w ∈ L (B) as required. (only if) Assume L (A ) ⊆ L (B) and let w ∈ L (A ). If w is not a data braid then w ∈ L (B ) ∪ L (A ¬db ) as required. Otherwise, w is a data braid, and we have the following: Claim 4.4.1. There is a timed word v such that the automata A and B cannot distinguish between w and db(v), i.e., accept either both or none of them. With the Claim above, by Theorem 4.1 we immediately obtain v ∈ L (A ) ⊆ L (B). Again by Theorem 4.1 we get db(v) ∈ L (B ), thus w ∈ L (B ) as well due to the Claim.

Figure 3 :

 3 Figure 3: An automaton checking that the first datum is equal to the last one.

Figure 4 :

 4 Figure 4: The result of the construction of Theorem 5.1.

Acknowledgements The authors thank the anonymous reviewers for their valuable comments.

* Work supported by the Future and Emerging Technologies (FET) programme within the Seventh Framework Programme for Research of the European Commission, under the FET-Open grant agreement FOX, number FP7-ICT-233599.