domain: info math phys

text:
Ali Yassin
email: aliyassin@etu.u-bourgogne.fr

Hocine Cherifi
email: hocine.cherifi@u-bourgogne.fr

Hamida Seba
email: hamida.seba@univ-lyon1.fr

Olivier Togni
email: olivier.togni@u-bourgogne.fr

Exploring Statistical Backbone Filtering Techniques in the Air Transportation Network

Keywords: Complex Networks, Backbone Filtering Techniques, Network Compression, Graph Summarization, Sparsification, Transportation Networks

The dense nature of transportation networks expands the challenge of their visualization and processing. Several statistical backbone extraction techniques are proposed to reduce their size while keeping essential information. Here, we perform a comparative evaluation of seven prominent statistical backbone extraction techniques in the USA weighted air transportation network. One can classify the airports into hubs, spokes, and focus airports based on the business models used by the airlines. We compare the extracted backbones using various performance measures. We consider the number of components, sizes, the fraction of airport type, edge type, and weights preserved by each method. Results show that the Enhanced Configuration Model (ECM) Filter tends to preserve edges between spoke airports uncovering the infrastructure connecting the regional spoke airports. In contrast, the alternative filters (Disparity, Polya Urn, Marginal Likelihood, Noise Corrected, Global Statistical Significance (GLOSS), Locally Adaptive Network Sparsification (LANS)) highlight edges between the hub and spoke, focus and spoke, and spoke and spoke airports revealing more of the hub and spoke foundation used by airlines. Moreover, the Disparity Filter, Marginal Likelihood Filter, and Noise Corrected Filter preserve the highest proportion of weights while Polya Urn Filter and ECM Filter keep the lowest. The GLOSS and LANS Filters maintain a moderate fraction of weights between the two extremes.

I. INTRODUCTION

Networks are widely adopted for analyzing complex systems in many fields. In particular, there is a significant interest in analyzing transportation networks [START_REF] Ducruet | Ports in multi-level maritime networks: Evidence from the atlantic (1996-2006)[END_REF]- [START_REF] Issa Moussa Diop | Revealing the component structure of the world air transportation network[END_REF]. In these networks, nodes represent spatial units such as cities, airports, ports, and stations, while edges describe transport-related interactions between the nodes. Edges are typically weighted by frequency, distance, capacity, or the time it takes to travel between nodes. Since transport networks are spatial, nodes This material is based upon work supported by the Agence Nationale de Recherche under grant ANR-20-CE23-0002. are preferably visualized in their location, producing dense networks with regionally clustered edges. This type of locally dense representation makes processing and visualization challenging tasks. Filtering the edges with weights below a global threshold value is a naive approach to reducing the network size. Unfortunately, this approach destroys the heterogeneity of the edge weight distribution. Consequently, various backbone extraction techniques have been proposed to reduce the network size while preserving the highest amount of "information". One can classify current backbone extraction techniques into structural and statistical methods. Structural techniques remove edges and nodes according to a criterion allowing the latent structure of the network to emerge [START_REF] Grady | Robust classification of salient links in complex networks[END_REF]- [START_REF] Ibnoulouafi | Mcentrality: identifying key nodes based on global position and local degree variation[END_REF]. They are generally designed to preserve critical topological properties of the network, such as the average distance, the community structure, and so on. In contrast, statistical techniques consider that noisy edges that need to be filtered hide the network structure [START_REF] Serrano | Extracting the multiscale backbone of complex weighted networks[END_REF]- [START_REF] Foti | Nonparametric sparsification of complex multiscale networks[END_REF]. They assess the significance of an edge through a statistical test, eliminating the least significant edges.

A previous study [START_REF] Dai | Transport network backbone extraction: A comparison of techniques[END_REF] compared six backbone extraction techniques in the Southeast Asian intercity air transport network [START_REF] Dai | The evolving structure of the southeast asian air transport network through the lens of complex networks, 1979-2012[END_REF]. It includes one statistical method (disparity filter) and five structural techniques (global weight thresholding, kcore decomposition, minimum spanning tree, primary linkage analysis, and multiple linkage analysis) [START_REF] Serrano | Extracting the multiscale backbone of complex weighted networks[END_REF], [START_REF] Alvarez-Hamelin | Large scale networks fingerprinting and visualization using the k-core decomposition[END_REF]- [START_REF] Rushton | Locational analysis in human geography[END_REF] . They evaluate the extracted backbones based on their geographical and topological structures, pointing out the potential of each technique in the light of different transport research applications. For instance, they recommend k-core decomposition to analyze the best-connected core for multiplex networks. They suggest that Primary linkage analysis is well-suited for functional/nodal regions analysis and highlighting hub-andspoke structures. Finally, they recommend the Disparity Filter for analyzing the overall topological and spatial information for large-scale networks and possible hidden structures.

After the Airline Deregulation Act in 1978, airport hubs have formed the backbone of the USA's present-day flying network and marketplace. Many regular airline companies such as American Airlines and United Airlines embrace the hub-and-spoke business model. However, not all airlines rely on this system. Many low-cost airlines provide point-to-point networks to route passengers on strategically chosen flight paths between focus airports, such as Southwest Airlines and JetBlue. In this study, we first consider a toy example (a part of the US Air Transportation Network) to understand better the behavior of various statistical backbone extraction techniques under test. We compare their ability to preserve different types of airports (hub, focus, and spoke) and edges. Finally, we extend our investigation to the North American air transportation Network to consolidate our findings

The rest of the paper is organized as follows. Section II introduces the backbone extraction techniques under test. Section III compares the backbone extraction techniques in a toy example. Section IV compares the backbone extraction techniques in the North American air transportation network. Finally, we make some concluding remarks in Section V.

II. BACKBONE EXTRACTION TECHNIQUES

This section briefly presents the statistical backbone extraction techniques under evaluation. Assume that G(N, E, W ) is a simple, undirected, and weighted graph where N is the set of nodes of size n = |N | nodes and E ⊆ N × N is the set of edges of size m = |E| edges. W represents the weight matrix, whose element w ij indicates the weight of the edge joining node i and j. We recall the degree k i of node i is the number of its neighbors, and its strength s i = j w ij is the sum of the weights of the edges incident to it. S = w ij is the the strength of the network All these statistical techniques share a common framework. Given an edge connecting node i to node j, they perform a statistical test based on a defined null model or the empirical data to compute the p-value α ij . Edges with p-values larger than a predefined statistical significance threshold α are considered non-significant and thus removed.

A. Global Threshold

The most straightforward technique is filtering edges with weights lower than a predefined threshold α. [START_REF] Serrano | Extracting the multiscale backbone of complex weighted networks[END_REF] This popular technique assesses the significance of an edge locally from the viewpoint of the incident nodes considered independently. It assumes that a node i distributes its total strength s i uniformly among its edges. Based on the defined model, it normalizes the weights following:

B. Disparity Filter

x ij = wij si .
Then it performs a one-sided right-tail test computing α ij the probability of observing a normalized weight X at least as "extreme" as x ij . It is given by:

α ij = P(X > x ij |k i ) = 1 -(k i -1) xij 0 (1 -x) ki-2 dx (1)
C. Polya Urn Filter [START_REF] Marcaccioli | A Pólya Urn approach to information filtering in complex networks[END_REF] In the Pólya Urn [START_REF] Haigh | Polya Urn models[END_REF], observing a particular event increases the probability of further observing it. Similarly, one can assume that edge weights are due to an aggregation process of nodes interacting with each other over time. Based on this, it assumes that a node i distributes its strength s i randomly through a Pólya process. For each edge, it performs a onesided right-tail test computing α ij the probability that node i will assign randomly through a Pólya process a weight X larger than or equal to w ij . It is given by:

α ij = P(w ≥ w ij |k i , s i , a) = 1 - wij -1 w=0 s i w B( 1 a + w, ki-1 a + s i -w) B( 1 a , ki-1 a ) (2)
A reinforcement parameter a governs this mechanism. The higher the value of the reinforcement mechanism a, the larger the weight must be for the edge to be considered significant. Note that the disparity filter is a special case of the Polya Urn Filter.

D. Marginal Likelihood Filter [14]

While the Disparity Filter and Polya Urn Filter assess the significance of an edge in the light of each node it connects independently, the Marginal Likelihood Filter considers the two nodes the edge connects. An integer-weighted edge is treated as multiple unit edges. The null model assumes that each unit edge randomly chooses two nodes, which results in a binomial distribution. For each edge, it performs a onesided right-tail test computing α ij the probability of drawing at least w ij unit edges from the strength S of the network with probability p = sisj 2S 2 proportional to both nodes' strengths. It is given by:

α ij = P(w ≥ w ij |s i , s j , S) = 1 - wij -1 w=0 S w p w (1 -p) S-w (3)
E. Noise Corrected Filter [START_REF] Coscia | Network backboning with noisy data[END_REF] Similar to the Marginal Likelihood Filter, it assumes edge weights are drawn from a binomial distribution. However, it estimates the probability of observing a weight connecting two nodes using a Bayesian framework. This framework enables us to generate posterior variances for all edges. This posterior variance allows us to create a confidence interval for each edge weight. Finally, we remove an edge if its weight is less than δ standard deviations stronger than the expectation, where δ is the only parameter of the algorithm. It also provides a direct approximation through Binomial distribution similar to the Marginal Likelihood Filter. however, the probability of a unit edge connecting node i with node j is defined as follows:

p = sisj S 2 .
F. GLOSS Filter [START_REF] Radicchi | Information filtering in complex weighted networks[END_REF] The GLOSS filter assumes that one cannot assess edges independently of the overall network topology. Therefore, it defines a global null model for evaluating the significance of an edge. However, it makes no assumptions about the distribution of weights. Instead, it employs the empirical distribution. The model is a network with the same topology as the original network and edge weights randomly drawn from the empirical weight distribution. For each edge, it performs a one-sided right-tail test computing α ij the probability of observing at least w ij edge weight between node i and node j considering the nodes' observed degrees k i , k j and strengths s i , s j as constraints. It is given by:

α ij = P(w > w ij |s i , k i , s j , k j ) = ∞ wij P obs (w)P (s i , s j |w, k i , k j )dw ∞ 0 P obs (w)P (s i , s j |w, k i , k j )dw (4) where, P (s i , s j |w, k i , k j ) = F (s i -w ij , k i -1)F (s j - w ij , k j -1)
. The function F (s, k) is the probability of randomly extracting from the weight distribution P obs (w), k elements whose sum is equal to s, which means that:

F (s, k) = P obs (x 1 )dx 1 P obs (x 2 )dx 2 ... × P obs (x k )dx k δ(x 1 + x 2 + ... + x k -s) (5)
G. LANS Filter [START_REF] Foti | Nonparametric sparsification of complex multiscale networks[END_REF] Like the GLOSS Filter, it makes no assumptions about the underlying weight distribution. Instead, it employs the empirical cumulative density function to judge statistical significance. First, it normalizes the weights following:

x ij = wij si .
Then from the viewpoint of node i it calculates the probability of choosing an edge at random with a normalized weight at least equal to the observed normalized weight x ij . It is given by:

α ij = P(X > x ij ) = 1 - 1 k i ki k=1 1{x ik ≤ x ij } ( 6
)
where 1{} is an indicator function.

H. ECM Filter [16]

Like the GLOSS Filter, it makes no assumptions about the underlying weight distribution. Using the Enhanced Configuration Model of network reconstruction, it employs a null model based on the canonical maximum-entropy ensemble of weighted networks having the same degree and strength distribution as the real network. We refer the readers to the original paper for a detailed mathematical explanation.

III. COMPARING BACKBONE EXTRACTION TECHNIQUES

ON A TOY EXAMPLE We begin our review of the backbone extraction techniques using a "toy network," a subgraph from the original worldwide air transportation network [START_REF] Alves | Centrality anomalies in complex networks as a result of model over-simplification[END_REF], including 42 US Airports and 378 edges. Edges represent routes between airports, and weights are the number of flights offered by different companies flying between 17 May and 22 May 2018. After the Airline Deregulation Act in 1978, airport hubs have formed the backbone of the country's present-day flying network and marketplace. Many regular airline companies, such as American Airlines and United Airlines, embraced the hub-andspoke business model. A traveler from a spoke airport would fly using a small carrier into a hub, then to another hub with a large carrier, and then reach the final destination by flying from the hub to another spoke airport. However, some airlines do not rely on the hub-and-spoke system. Indeed, Low-cost companies such as Southwest Airlines and JetBlue provide point-to-point networks to route passengers on strategically chosen flight paths between focus airports. Therefore, we can consider three types of airports (Hubs, Spokes, and Focus).

The toy example network contains 20 Hubs (Stars), 20 Spokes (Triangles), and 3 Focus (Square) airports. We extract the top most significant 30 edges for each backbone filtering technique to build the backbones. We use the Global Threshold Filter as a reference in the comparative evaluation. Figure 1 represents the backbone extracted by the Global Threshold Filter in the toy example. It shows the top 30 edges with the highest weights connecting the Hubs, Focus, and Spokes airports. Table I reports the number of components identified by each filtering technique and their relative size. Except for LANS and ECM, the filters demonstrate their ability to extract a large connected component with a few small ones. In contrast, the backbones of LANS and ECM spread across multiple components of more homogeneous sizes.

Table II reports the percentage of nodes, hub, focus, and spoke airports preserved by each filtering technique. LANS and ECM Filters keep a significant proportion of nodes (above 80%). The other filters are far behind, with a score similar to the Global Threshold Filter. Indeed, they keep around 60% of the nodes of the toy network. All the filters are pretty effective at keeping the hub airports. The LANS Filter backbone includes them all. The GLOSS and ECM Filters Table III reports the fraction of various edge types preserved in the extracted backbones (hub-hub, hub-focus, hub-spoke, and focus-spoke).

Let's start with the hub-hub edges. One can observe that the GLOSS Filter and Polya Urn Filter score similarly to the Global Threshold Filter at preserving the hub-hub edges (≈ 8%). In contrast, the other filters keep a lower fraction. In particular, LANS Filter and ECM Filter preserve a lower portion (5.95% and 4.32%), nearly half the amount of the reference filter.

Let's now turn to the hub-focus edges. The Global threshold Filter keeps 10% of hub-focus edges. The other filters preserve a lower proportion (≤ 8.6%). The GLOSS Filter is the worst, with only 1.72% of the hub-focus edges kept.

Let's now consider the hub-spoke edges. The Global threshold and Polya Urn Filter preserve the same fraction of the hub-spoke edges (6.72%). The other filters preserve a slightly higher fraction. In particular, the LANS and ECM Filters retain the highest fraction of the hub-spoke edges (≈ 12.6%).

Finally, results are more mixed for focus-hub edges. Indeed, the Disparity Filter, Polya Urn Filter, and GLOSS Filter follow the reference filter. They preserve the same amount of the focus-hub edges (7.69%). The Marginal Likelihood Filter, Noise Corrected Filter, and ECM Filter are more effective. Indeed, they preserve more than twice the fraction of these edges compared to the reference. The LANS Filter does not retain any of the focus-spoke edges. Table IV reports the fraction of weights associated with the different types of edges kept in the backbone. The first column gives the total fraction of weight independently of their class. One can see that the Global Threshold Filter preserves the highest possible fraction of weights (36.10%). Indeed, it retains the links with the top weights exclusively. The Disparity Filter, Marginal Likelihood Filter, and Noise Corrected Filter are not far behind. They retain ≈ 34%). In contrast, the Polya Urn Filter preserves the smallest portion of weights (7.6%), showing its ability to keep edges with low weights in the backbone. The other filters are distributed between these two extremes. When we look at the fraction of hub-hub edges retained in the various backbones, we observe the same ranking with all types of nodes. Indeed hub-hub links have generally heavy weights. Concerning the hub-focus links, the Polya Urn Filter and GLOSS Filter preserve a tiny portion of weights (≈ 4.8%). The global Threshold filter, as expected, keeps the highest fraction (≈ 50%). The other filters preserve ≈ 10% fewer edge weights than the Global Threshold Filter. Now, look at the hub-spoke links results reported in the fourth column. Once again, the Polya Urn Filter preserves a tiny portion of this type of edge (≈ 6.2%). The ECM Filter follows. Indeed, it keeps a smaller fraction of edges than the Global Threshold Filter. All the other filters outperform the Global Threshold Filter at preserving a high fraction of hub-spoke links. Indeed, this type of link usually does not have the top weights. The last column reports the fraction of focus-spoke links kept in the various backbones. The Global Threshold, Disparity, and GLOSS Filters preserve the same fraction (≈ 23%). The Marginal Likelihood, Noise Corrected, and ECM Filters retain a significant proportion ranging between 38% and 45%. In contrast, the Polya Urn Filter preserves a tiny portion of weights associated with the Focus-Spoke edges (1.1%). The LANS backbone do not preserve any of this type of edges.

Table V summarizes the strengths and weaknesses of the backbone filtering techniques based on these results.

IV. COMPARING BACKBONE EXTRACTION TECHNIQUES IN THE NORTH-AMERICAN AIR TRANSPORTATION NETWORK

We reproduce the same experiment with a bigger network to validate our findings. We extract the nodes and edges of North America from the original world transportation network. Indeed, it is easier to classify the airports in this region than in the rest of the world. The network contains 839 nodes and 4,046 edges. Finally, we extracted the network's backbone preserving the most significant 10% edges using all the filtering techniques under test.

Table VI reports the size and the number of components of the various backbones. Results are similar to the toy example. Indeed, the LANS and ECM filters split the network into several parts while the other filtering techniques retain a large component.

Table VII reports the fraction of nodes kept by the backbones when filtering 90% of edges. One can consider three categories when comparing the total number of nodes preserved in the various backbone. The first class contains ECM, LANS, and GLOSS filters. They keep the higher fraction of nodes (mean value around 45%). Polya Urn and Disparity filters form the second category. In that case, the mean value of the fraction of kept nodes drops to 30%. Finally, Marginal Likelihood, Noise Corrected, and Global threshold filters are similar. Indeed, they keep around 15% of the nodes. Moreover, except for the ECM Filter, all filters effectively keep Hub and Focus airports. Indeed, they retain between 80 % and 100 % of these types of nodes characterized by high traffic. This observation is in line with the toy example. In contrast, The ECM Filter preserves only 32% of the hubs and 17% of the focus airports. The last column reports the fraction of spokes contained in the backbones. Globally, the results are comparable with the toy example network. The hierarchy is unchanged except for the Polya Urn filter and the Marginal Likelihood Filter. Indeed, compared to the global threshold filter, this time, the Polya Urn Filter preserves more spoke airports while the Marginal preserves less.

Table VIII reports the fraction of edges preserved by the filtering technique in the North American network. Concerning the hub-hub edges, results correlate well with the behavior observed in the toy example. Indeed, this time all the filters contain a lower amount of this type of node than the global threshold filter. We notice a different behavior for the ECM, LANS, and GLOSS Filters for the hub-focus edges. The ECM and LANS Filters preserve a low fraction of these edges, while the GLOSS Filter preservers a higher amount. Except for the ECM Filter, all the filters behave similarly as in the toy example for the hub-spoke edges. Indeed, the ECM Filter preserves a very tiny portion of these edges. The ECM filter and LANS filter behavior deviate from the toy example for the focus-spoke edges. Indeed, the LANS Filter starts to keep this type of edge, while the ECM Filter barely retains any edges of this type. This network contains two new classes of edges that do not exist in the toy example: the focus-focus and spoke-spoke edges. Disparity, Marginal Likelihood, and Noise Corrected Filters keep nearly the same amount of these focusfocus nodes as the Global Threshold Filter (≈ 10%). The other techniques hold a lower share. In particular, the ECM Filter removes all of them. One can notice that all the backbone filtering methods preserve a higher fraction of the spoke-spoke edges than the Global Threshold Filter. It is particularly true for the ECM Filter that keeps almost 40%.

Table IX reports the fraction of weights kept by the filtering techniques in the North-American Network. The results of the total fraction of weights and the hub-hub edge weights are similar to the toy example network. Only the ECM Filter deviates. It preserves a tiny fraction of the weights. LANS and ECM Filters keep a low fraction contrasting with the toy example for the hub-focus weights. Looking at the hub-spoke edge weights, unlike in the toy example, GLOSS and LANS Filter preserve a lower fraction than the Global Threshold this time. For the focus-spoke edge weights, the LANS Filter does not remove all edges of this type, thus increasing the weight. On the other hand, the ECM Filter almost removes all these edges, thus decreasing the preserved weight. The other filters exhibit the same behavior as in the toy example. We observe two categories for the focus-focus edge weights. The first category contains the Disparity, Marginal Likelihood, Noise Corrected, and the Global Threshold Filters. They preserve more than 50% of these links. The techniques in the second category keep a lower amount. In particular, the Polya Urn Filter preserves a tiny portion (7%), and the ECM Filter does not preserve any. Finally, all techniques preserve a fraction similar to the reference filter for the spoke-spoke edge weights, except the Polya Urn Filter. Indeed, it keeps a low amount of spoke-spoke edge weights (7%).

All filtering techniques generally maintain a similar behavior except for the ECM Filter. They preserve a lower fraction Filter, and LANS Filter shift their priority in preserving hubspoke edges to the spoke-spoke edges. Additionally, the ECM Filter almost ignores all types of edges and keeps only the spoke-spoke edges. These edges are associated with small weights usually, which explains the low percentage of weight preserved by the ECM Filter.

V. CONCLUSION

This paper evaluates statistical backbone extraction techniques in filtering the hub and spoke infrastructure of the air transportation network. Results show that the reference (Global Threshold Filter) extracts a backbone mainly composed of the hub and focus airports, revealing the rich-club phenomena in the air transportation network. In contrast, other statistical filters tend to preserve various categories of links (edges connecting the hub to spoke, focus to spoke, and spoke to spoke airports), revealing more information on the hub and spoke foundation used by airline companies. The ECM filter has a unique behavior. It keeps mainly edges between spoke airports uncovering the infrastructure connecting the regional spoke airports. Moreover, LANS and ECM split the backbone into multiple components. It is an undesired property for a transportation network. Indeed, both filters preserve a low portion of hub-hub and focus-hub edges which usually hold the network together. Furthermore, results show that the Disparity Filter, Marginal Likelihood Filter, and Noise Corrected Filter preserve the highest fraction of weights. In contrast, Polya Urn Filter and ECM Filter perform poorly. The other techniques retain a moderate weight fraction between these extremes. Future work will consider an extensive investigation of various transportation networks to consolidate these findings.

Fig. 1 .

 1 Fig. 1. The backbone preserves the 30 top most significant edges extracted by the Global Threshold Filter. Stars, squares, and circles represent hub, focus, and spoke airports. The node's size and the edge's width are proportional to the weighted degree and weight, respectively.

TABLE I RELATIVE

 I SIZE OF THE COMPONENTS EXTRACTED BY THE FILTERING TECHNIQUE IN THE TOY EXAMPLE IN DECREASING ORDER . NOTE THAT VALUES BETWEEN () REPRESENT THE NUMBER OF COMPONENT WITH THE SAME SIZE.Polya Urn Filter and the global threshold filter are the less effective, with a score of 85%. The third column of the table shows that the filters preserve all the focus airports. It is not the case for GLOSS and the Polya Urn Filter. Indeed, they isolated one focus airport. The last column reports the percentage of spoke airports preserved. The Global Threshold Filter and Polya Urn Filter keep the lowest fraction of spoke airports (30%). The Disparity Filter, Marginal Likelihood Filter, Noise Corrected Filter, and GLOSS Filter preserve a medium proportion between 40% and 45%. LANS Filter and the ECM Filter are the more effective. Indeed, they keep a significant balance of spoke airports (65% and 80%).

	Filter	% C1 % C2	% C3	% C4	% C5
	Global Threshold	92.3	7.7	-	-	-
	Disparity	93.1	6.9	-	-	-
	Polya Urn	92	8	-	-	-
	Marginal Likelihood	93.1	6.9	-	-	-
	Noise Corrected	70	23.33	6.67	-	-
	GLOSS	56.67	26.67	10	6.66	-
	LANS	27.79	25	19.45	11.1(2)	5.56
	ECM	28.95	15.79	10.52(2)	7.9(3)	5.26(2)
	follow. They preserve a significant fraction of hub airports
	(95%).

TABLE II FRACTION

 II OF NODES, HUB, FOCUS, AND SPOKE AIRPORTS PRESERVED BY THE FILTERING TECHNIQUES IN THE TOY EXAMPLE.

	Filter	% Nodes	% Hubs % Focus % Spokes
	Global Threshold	60	85	100	30
	Disparity	67	90	100	40
	Polya Urn	58	85	67	30
	Marginal Likelihood	67	90	100	40
	Noise Corrected	69	90	100	45
	GLOSS	69	95	67	45
	LANS	83	100	100	65
	ECM	88	95	100	80

TABLE V SUMMARY

 V ON STRENGTHS AND WEAKNESSES OF THE STATISTICAL BACKBONE FILTERING TECHNIQUES.

	Filter	Strengths	Weaknesses
	Global Threshold
		• Preserves the highest possible fraction of weights	• Preserves a medium portion of nodes (60%)
		• Retains a large connected component	• Ignores edges with low weights
		• Prioritizes hub-hub and hub-focus edges with high
		weights
	Disparity
		• Preserves a very high fraction of weights	• Preserves a medium portion of the nodes (67%)
		• Retains a large connected component	• Biased to edges with high weights
		• Prioritizes hubs-spoke edges with high weights
	Polya Urn
		• Retains a large connected component	• Preserves a medium portion of the nodes (58%)
		• Preserves similar portions for each edge type	• Preserves very low fraction of weights (7.6%)
	Marginal Likelihood
		• Preserves a high portion of weights (34.7%)	• Preserves a medium portion of nodes (67%)
		• Retains a large connected component
		• Prioritizes edges between hub-spoke and focus-spoke
		edges, preserving more hubs and spoke airports
	Noise Corrected
		• Preserves a high portion of weights (34%)

• Retains a large connected component • Prioritizes edges between hub-spoke and focus-spoke edges, preserving more hubs and spoke airports • Preserves a medium portion of nodes (67%) GLOSS • Preserve a medium portion of the nodes (70%) • Prioritizes hub-spoke edges • Preserves almost all the hub and half of the spoke airports • Preserves a medium portion of weights (20%) • Do not retain a large connected component LANS • Preserves a high portion of nodes (83%) • Preserves a high portion of weights (30%) • Prioritizes hub-spoke edges • Do not retain a large connected component • Ignores focus-spoke edges.

ECM

• Preserves a high portion of nodes (88%)

• Prioritizes hub-spoke and focus-spoke edges • Preserves a medium portion of weights (26%)

• Do not retain a large connected component

TABLE VII FRACTION

 VII OF NODES, HUB, FOCUS, AND SPOKE AIRPORTS PRESERVED BY THE FILTERING TECHNIQUES IN THE NORTH AMERICA NETWORK.

	Filter	% Nodes	% Hubs	% Focus % Spokes
	Global Threshold	15.6	100	82.6	10.6
	Disparity	26.8	100	95.6	22.2
	Polya Urn	33.3	100	95.6	29.1
	Marginal Likelihood	17.4	100	91.3	12.3
	Noise Corrected	16.3	100	82.6	11.4
	GLOSS	35.3	100	86.9	31.5
	LANS	49.9	100	91.3	46.95
	ECM	48.9	32.1	17.3	50.5

TABLE VIII THE

 VIII PROPORTION OF HUB-HUB (H-H), HUB-FOCUS (H-F), HUB-SPOKE (H-S), FOCUS-FOCUS (F-F),FOCUS-SPOKE (F-S), AND SPOKE-SPOKE (S-S) EDGES PRESERVED BY THE FILTERING TECHNIQUES IN THE NORTH-AMERICAN NETWORK.

	Filter	% H-H	% H-F % H-S % F-F	% F-S % S-S
	Global Threshold	23.4	15.8	10.9	10.3	8.5	1.9
	Disparity	16.5	14.2	10.8	12.3	8.9	4.7
	Polya Urn	13	13.1	10.7	6.1	7.7	7.7
	Marginal Likelihood	10.7	13.1	12.1	11.3	12.8	2.4
	Noise Corrected	11.4	14.7	12.3	10.3	10.9	2.3
	GLOSS	10.4	9.8	9.8	6.1	8.7	11.3
	LANS	5.3	3.2	14.8	5.1	7.1	6.5
	ECM	0.3	0.2	1.6	0	1.3	39.6

TABLE IX FRACTION

 IX OF WEIGHTS PRESERVED BY THE FILTERING TECHNIQUES IN THE NORTH-AMERICAN NETWORK FOR THE DIFFERENT TYPE OF EGDES: ALL TYPE OF EDGES (W), HUB-HUB (H-H), HUB-FOCUS (H-F), HUB-SPOKE (H-S), FOCUS-FOCUS (F-F),FOCUS-SPOKE (F-S), AND SPOKE-SPOKE (S-S)

	Filter	% W % H-H	% H-F % H-S % F-F	% F-S % S-S
	Global Threshold	47.6	61.8	56.3	44.5	54.9	39.2	23.5
	Disparity	41.1	51.7	52.3	37.2	56.8	33.7	21.1
	Polya Urn	11.6	12.7	12	13.2	7.1	6.3	6.9
	Marginal Likelihood	44.8	38.5	50	45.6	56.7	50.1	28.1
	Noise Corrected	45.3	38.9	52.8	46.9	54.9	45.8	27.5
	GLOSS	25.4	27.9	28.7	24.4	21.1	23.8	24.1
	LANS	24.1	23.3	16.8	28.8	30.6	15.4	20.2
	ECM	2.4	1.6	0.8	1.5	0	0.5	21.1


Carlos Olarte
email: colarte@lix.polytechnique.fr

Camilo Rueda
email: crueda@cic.javerianacali.edu.co

A Declarative Language for Dynamic Multimedia Interaction Systems ⋆

Universal Timed Concurrent Constraint Programming (utcc) is a declarative model for concurrency tied to logic. It aims at specifying mobile reactive systems, i.e., systems that continuously interact with the environment and may change their communication structure. In this paper we argue for utcc as a declarative model for dynamic multimedia interaction systems. Firstly, we show that the notion of constraints as partial information allows us to neatly define temporal relations between interactive agents or events. Secondly, we show that mobility in utcc allows for the specification of more flexible and expressive systems. Thirdly, by relying on the underlying temporal logic in utcc, we show how non-trivial temporal properties of the model can be verified. We give two compelling applications of our approach. We propose a model for dynamic interactive scores where interactive points can be defined to adapt the hierarchical structure of the score depending on the information inferred from the environment. We then broaden the interaction mechanisms available for the composer in previous (more static) models. We also model a music improvisation system based on the factor oracle that scales up to situations involving several players, learners and improvisers.

Introduction

Process calculi provide a language in which the structure of terms represents the structure of processes together with an operational semantics to represent computational steps. Concurrent Constraint Programming (CCP) [START_REF] Saraswat | Concurrent Constraint Programming[END_REF] has emerged as a declarative model for concurrency tied to logic. In CCP, concurrent systems are specified by means of constraints (e.g. x + y ≥ 10) representing partial information about certain variables. This way, agents (or processes) interact with each other by telling and asking information represented as constraints in a global store: A process tell(c) adds the constraint c, thus making it available to other processes. A positive ask when c do P remains blocked until the store is strong enough to entail c; if so, it behaves like P .

Interactivity in multimedia systems has become increasingly important. The aim is to devise ways for the machine to be an active partner in a collective behavior constructed dynamically by many actors. In its simplest form, a musician signals the computer when processes should be launched or stopped. In more complex forms the machine is always actively adapting its behavior according to the information derived from the activity of the other partners. To be coherent these machine actions must be the result of a complex adaptive system composed of many agents that should be coordinated in precise ways. Constructing such systems is a challenging task. Moreover, ensuring their correctness poses a great burden to the usual test-based techniques. In this setting, CCP has much to offer: CCP calculi are explicitly designed for expressing complex coordination patterns in a very simple way by means of constraints. In addition, their declarative nature allows formally proving properties of systems modeled with them.

Interactive scores [START_REF] Allombert | A system of interactive scores based on Petri nets[END_REF] are models for reactive music systems adapting their behavior to different types of intervention from a performer. Weakly defined temporal relations between components in an interactive score specifies loosely coupled music processes potentially changing their properties in reaction to stimulus from the environment (say, a performer). An interactive score defines a hierarchical structure of processes. Musical properties of a process depend on the context in which it is located. Although the hierarchical structure has been treated as static in previous works, there is no reason it should be so. A process, in reaction to a musician action, for example, could be programmed to move from one context to another or simply to disappear. Imagine, for instance, a particular set of musical materials within different contexts that should only be played when an expected information from the environment actually takes place. Modeling this kind of interactive score mobility in a coherent way is greatly simplified by using the calculus described in this paper.

Musical improvisation is another natural context for interacting agents. Improvisation is effective when agents behavior adapts to what has been learned in previous interactions. A music style-learning/improvisation scheme such as Factor Oracle (FO) [START_REF] Allauzen | Factor oracle: A new structure for pattern matching[END_REF][START_REF] Assayag | A concurrent constraints factor oracle model for music improvisation[END_REF] can be seen as a reactive system where several learning and improvising agents react to information provided by the environment or by other agents. In its simplest form three concurrent agents, a player, a learner and an improviser must be synchronized. Since only three independent processes are active, coordination can be implemented without major difficulties using traditional languages and tools. The question is whether such implementations would scale up to situations involving several concurrent agents. For an implementation using traditional languages the complexity of such systems would most likely impose many simplifications in coordination patterns if behavior is to be controlled in a significant way. A CCP model, as described here, provides a compact and simple model of the agents involved in the FO improvisation, one in which coordination is automatically provided by the blocking ask construct of the calculus. Moreover, additional agents could easily be incorporated in the system. As an extra bonus, fundamental properties of the constructed system can be formally verified in the model.

In this paper we argue for Universal Timed CCP (utcc) [START_REF] Olarte | Universal concurrent constraint programing: Symbolic semantics and applications to security[END_REF] as a declarative language for the modeling and verification of multimedia interaction systems. The utcc calculus is a timed extension of CCP with the ability to model mobile reactive sys-tem, i.e., systems that continuously interact with the environment and may change their communication structure.

After a brief introduction of utcc in Section 2, our contributions are as follows. In Section 3, we propose a utcc model for interactive scores where the interactive points allow the composer to dynamically change the hierarchical structure of the score. We then broaden the interaction mechanisms available for the user in previous (more static) models, e.g., [START_REF] Allombert | Concurrent constraints models for interactive scores[END_REF], where temporal objects cannot be moved to different contexts according to the information derived from the environment. We also provide a framework based on the underlying linear temporal logic of utcc to formally verify fundamental properties of the constructed system. For instance, we can verify if certain musical structure is not played due to the absence of a stimulus from the environment. In Section 4 we model a music improvisation system based on the factor oracle that scales up to situations involving several agents and offers a more compact and efficient representation of the data structure wrt the model in [START_REF] Assayag | A concurrent constraints factor oracle model for music improvisation[END_REF]. Section 5 concludes the paper.

An extended version of this work, including further details, is available at [START_REF] Olarte | A declarative language for dynamic multimedia interaction systems[END_REF].

Preliminaries

CCP-based languages are parametric in a constraint system [START_REF] Saraswat | Concurrent Constraint Programming[END_REF] defining the kind of constraints that can be used in the program. Here, constraints c, d, . . . are understood as formulae in a first-order language. If the information of d can be entailed (or deduced) from the information represented by c we write c ⊢ d (e.g. pitch > 64 ⊢ pitch > 48).

Universal timed CCP (utcc) [START_REF] Olarte | The expressivity of universal timed CCP: Undecidability of monadic FLTL and closure operators for security[END_REF] extends Timed CCP (tcc) [START_REF] Saraswat | Foundations of timed concurrent constraint programming[END_REF] for mobile reactive systems. Time in utcc is conceptually divided into time intervals (or time-units). In a particular time-unit, a utcc process P gets an input c from the environment, it executes with this input as the initial store, and when it reaches its resting point, it outputs the resulting store d to the environment. Furthermore, the resting point determines a residual process, which is then executed in the next time interval.

Processes in utcc are built by the following syntax:

P, Q := skip | tell(c) | (abs x; c) P | P Q | (local x; c) P | next P | unless c next P | ! P
A process skip represents inaction. A process tell(c) adds c to the store in the current time interval, thus making it available to other processes.

In utcc, the CCP ask operator when c do P (executing P if c can be deduced) is replaced by the abstraction operator (abs x; c) P . This construct is a parameterized ask where P [t/x] is executed for all the terms t s.t c[t/x] is entailed by the store.

A process P Q denotes P and Q running in parallel possibly "communicating" via the common store. The process (local x; c) P behaves like P but the information c about the variables in x is local to P . We shall omit c in (local x; c) P when c ≡ true.

From a programming language perspective, x in (local x; c) P can be viewed as the local variables of P while x in (abs x; c) P as the formal parameters of P . This way, abstractions can encode recursive definitions of the form X(x) def = P (see [START_REF] Olarte | A declarative language for dynamic multimedia interaction systems[END_REF]). The unit-delay next P executes P in the next time interval. The (weak) time-out unless c next P executes P in the next time-unit iff c cannot be entailed by the final store at the current time interval. The replication ! P means P next P next 2 P..., i.e. unboundedly many copies of P but one at a time.

We shall also use the derived operator (wait x; c) do P that waits, possibly for several time-units, until for some t, c[t/x] holds and then it executes P [t/x] (see [START_REF] Olarte | Universal concurrent constraint programing: Symbolic semantics and applications to security[END_REF]).

An Example. The abstraction operator allows us to communicate (local) names or variables between processes, i.e., mobility in the sense of the π-calculus [START_REF] Milner | Communicating and Mobile Systems: the Pi-Calculus[END_REF]. Let us give a simple example of this situation. Let P be a process modeling a musician playing notes at different time-units, and Q be an improvisation system which after "reading" the note played by P performs some action R. Roughly, this scenario can be modeled as follows

P def = tell(play (A)) next (tell(play (G)) next tell(play (B))) . . . Q def = ! (abs x; play(x)) R
When executing P Q, we observe, e.g., R[G/x] in the second time-unit. This means that P and Q synchronized on the constraint play(•) and the note played by P (i.e. G) was read by Q and then processed by R. See [START_REF] Olarte | A declarative language for dynamic multimedia interaction systems[END_REF] for a more involved example defining synchronization of multiple agents.

Logic Characterization. The utcc calculus enjoys a declarative view of processes as first-order linear-time temporal logic (FLTL) formulae [START_REF] Manna | The Temporal Logic of Reactive and Concurrent Systems: Specification[END_REF]. This means that processes can be seen, at the same time, as computing agents and as logic formulae.

Formulae in FLTL are built from the following syntax

F, G, . . . := c | F ∧ G | ¬F | ∃xF | •F | F.
where c is a constraint. The modalities •F and F stand for resp., that F holds next and always. We use ∀xF for ¬∃x¬F , and the eventual modality ✸F as an abbreviation of ¬ ¬F . See [START_REF] Manna | The Temporal Logic of Reactive and Concurrent Systems: Specification[END_REF] for further details on this logic.

Processes in utcc can be represented as FLTL formulae as follows:

[[skip]] = true [[tell(c)]] = c [[P Q]] = [[P ]] ∧ [[Q]] [[(abs y; c) P ]] = ∀y(c ⇒ [[P ]]) [[(local x; c) P ]] = ∃x(c ∧ [[P ]]) [[next P ]] = •[[P ]] [[unless c next P ]] = c ∨ •[[P ]] [[! P ]] = ✷[[P ]] Let A = [[P ]].
Roughly, A ⊢ ✸c (i.e., c eventually holds in A) iff the process P eventually outputs c (see [START_REF] Olarte | A declarative language for dynamic multimedia interaction systems[END_REF][START_REF] Olarte | The expressivity of universal timed CCP: Undecidability of monadic FLTL and closure operators for security[END_REF] for further details).

A Model for Dynamic Interactive Scores

An interactive score [START_REF] Allombert | A system of interactive scores based on Petri nets[END_REF] is a pair composed of temporal objects and Allen temporal relations [START_REF] Allen | Maintaining knowledge about temporal intervals[END_REF]. In general, each object is comprised of a start-time, a duration, and a procedure. The first two can be partially specified by constraints, with different constraints giving rise to different types of temporal objects, so-called events (duration equals zero), textures (duration within some range), intervals (textures without procedures) or control-points (a temporal point occurring somewhere within an interval object). The procedure gives operational meaning to the action of the temporal object. It could just be playing a note or a chord, or any other action meaningful for the composer. temporal structure is determined by the hierarchy of temporal objects. Suppose that, as a result of the information obtained by the occurrence of an event, object T 2 should no longer synchronize with a control-point inside T 1 but, say, with a similar point inside T 5 . This very simple interaction cannot be modeled in the standard model of interactive scores [START_REF] Allombert | A system of interactive scores based on Petri nets[END_REF]. Another example is an object waiting for some interaction from the performer within some temporal interval. If the interaction does not occur, the composer might then determine to probe the environment again later when a similar musical context has been defined. This amounts to moving the waiting interval from one box to another.

The model. Figure 2 shows our model for dynamic interactive scores. The process BoxOperations may perform the following actions:

mkbox(id, d): defines a new box with id id and duration d. The start time is defined as a new (local) variable s whose value will be constrained by the other processes. destroy(id): firstly, it retrieves the box sup which contains the box id. If the box id is not currently playing, in the next time-unit, it drops the boundaries of id by inserting all the boxes contained in id into sup. before(x, y): checks if x and y are contained in the same box. If so, the constraint bf(x, y) is added. into(x, y): dictates that the box x is into the box y if x is not currently playing.

out(x, y): takes the box x out of the box y if x is not currently playing.

Process Constraints adds the necessary constraints relating the start times of each temporal object to respect the hierarchical structure of the score. For each constraint of the form in(x, y), this process dictates that the start time of x must be less than the one of y. Furthermore, the end time of y (i.e. d y + s y ) must be greater than the end time of x. The case for bf(x, y) can be explained similarly.

The process P ersistence transfers the information of the hierarchy (i.e. box declarations, in and bf relations) to the next time-unit.

The process Clock defines a simple clock which binds the variable t to the value v in the current time-unit and to v + 1 in the next time-unit. The process P lay(x, t) adds the constraint play(x) during t time-units. This informs the environment that the box x is currently playing.

The process Init(t) waits until the environment provides the constraint init(x) for the outermost box x to start the execution of the system. Then, the clock is started and the start time of x is set to 0. The rest of the boxes wait until their start time is less or equal to the current time (t) to start playing.

Finally, the whole system is the parallel composition between the previously defined processes and the specific user model, e.g. :

U srBoxes def = tell(mkbox(a, 22) ∧ mkbox(b, 12) ∧ mkbox(c, 4)) tell(mkbox(d, 5) ∧ mkbox(e, 2)) tell(into(b, a) ∧ into(c, b) ∧ into(d, b) ∧ into(e, d)) tell(before(c, d)) whenever play(b) do unless signal next tell(out(d, b) ∧ mkbox(f, 2) ∧ into(f, a)) tell(before(b, f ) ∧ before(f, d))
This system defines the hierarchy in Figure 3(a). When b starts playing, the system asks if the signal signal is present (i.e., if it was provided by the environment). If it was not, the box d is taking out from the context b. Furthermore, a new box f is created such that b must be played before f and f before d as in Figure 3(b). Notice that when the box d is taken out from b, the internal box e is still into d preserving its structure.

Verification of the Model

The processes defined by the user may lead to situations where the final store is inconsistent as in st < 5 ∧ st > 7 where st is the start time of a given box. Take for example the process U srBoxes above. If the box f is defined with a duration greater than 5, the execution of f (and then that of d) will exceed the boundaries of the box a which contains both structures. In this context, the declarative view of utcc processes as FLTL formulae provides a valuable tool for the verification of the model: The formula A = [[P ]] allows us to verify whether the execution of P leads to an inconsistent store. Thus, we can detect pitfalls in the user model such as trying to place a bigger box into a smaller one or taking a box out of the outermost box.

In the following, we present some examples of temporal properties we could verify in an interactive score represented as the process P . Remark. For the sake of presentation we only defined here the before relation. Our model can be straightforwardly extended to support all Allen temporal relations [START_REF] Allen | Maintaining knowledge about temporal intervals[END_REF]. Making use of the into and out operations, we can define also the operation move(a, b) meaning, move the structure a into the structure b.

As described above, in interactive scores the actual musical output may change depending on interactions with a performer, but the framework is not meant for learning from those interactions, nor to change the score (i.e. improvise) accordingly.

Music improvisation provides a complex context of concurrent systems posing great challenges to modeling tools. In music improvisation, partners behave independently but are constantly interacting with others in controlled ways. The interactions allow building a complex global musical process collaboratively. Interactions become effective when each partner has somehow learned about the possible evolutions of each musical process launched by the others, i.e, their musical style. Getting the computer involved in the improvisation process requires learning the musical style of the human interpreter and then playing jointly in the same style. A style in this case means some set of meaningful sequences of musical material the interpreter has played. A graph structure called factor oracle (F O) is used to efficiently represent this set [START_REF] Allauzen | Factor oracle: A new structure for pattern matching[END_REF].

A FO is a finite state automaton constructed in an incremental fashion. A sequence of symbols s = σ 1 σ 2 . . . σ n is learned in such an automaton, which states are 0, 1, 2 . . . n. There is always a transition arrow (called factor link) labeled by the symbol σ i going from state i -1 to state i, 1 ≤ i < n. Depending on the structure of s, other arrows will be added. Some are directed from a state i to a state j, where 0 ≤ i < j ≤ n. These also belong to the set of factor links and are labeled by symbol σ j . Some are directed "backwards", going from a state i to a state j, where 0 ≤ j < i ≤ n. They are called suffix links, and bear no label (represented as '⋆' in our processes below). The factor links model a factor automaton, that is every factor p in s corresponds to a unique factor link path labeled by p, starting in 0 and ending in some other state. Suffix links have an important property : a suffix link goes from i to j iff the longest repeated suffix of s[1..i] is recognized in j. Thus suffix links connect repeated patterns of s.

The oracle (see Figure 4) is learned on-line. For each new input symbol σ i , a new state i is added and an arrow from i -1 to i is created with label σ i . Starting from i -1, the suffix links are iteratively followed backward, until a state is reached where a factor link with label σ i originates (going to some state j), or until there is no more suffix links to follow. For each state met during this iteration, a new factor link labeled by σ i is added from this state to i. Finally, a suffix link is added from i to the state j or to state 0 depending on which condition terminated the iteration. Navigating the oracle in order to generate variants is straightforward : starting in any place, following factor links generates a sequence of labelling symbols that are repetitions of portions of the learned sequence; following one suffix link followed by a factor links creates a recombined pattern sharing a common suffix with an existing pattern in the original sequence. This common suffix is, in effect, the musical context at any given time.

In [START_REF] Assayag | A concurrent constraints factor oracle model for music improvisation[END_REF] a tcc model of FO is proposed. This model has three drawbacks. Firstly, it (informally) assumes the basic calculus has been extended with general recursion in order to correctly model suffix links traversal. Secondly, it assumes dynamic construction of new variables δ iσ set to the state reached by following factor link labelled σ from state i. This construction cannot be expressed with the local variable primitive in basic tcc. Thirdly, the model assumes a constraint system over both finite domains and finite sets. We use below the expressive power of the abstraction construction in utcc to correct all these drawbacks (see Figure 5). Furthermore, our model leads to a compact representation of the data structure of the FO based on constraints of the form edge(x, y, N ) representing an arc between node x and y labeled with N . Process Counter signals when a new played note can be learned. It can be learned when all links for the previous note have already been added to the FO. Process Persistence transmits information about already constructed arcs (factor and suffix) to all future time-units. Process Step 1 adds a factor link from i -1 to i labelled with a just played note and launches traversal of suffix links from i -1. When state zero is reached by traversing suffix links, process Step 2 adds a suffix link from i to a state reached from 0 by a factor link labelled N ote, if it exists, or from i to state zero, otherwise. For each state k different from zero reached in the suffix links traversal, process Step 2 adds factor links labelled N ote from k to i.

The inclusion of a new agent in our FO model (e.g. a learner agent for a second performer) entails a new process and new interactions, both with the new process and among the existing ones. In traditional models this usually means major changes in the synchronization scheme, which are difficult to localize and control. In utcc, all synchronization is done semantically, through the available information in the store. Each agent would thus have to be incremented with processes testing for the presence of new information (e.g. a factor link with some label in the other agent's FO graph). The new synchronization behavior that this demands is automatically provided by the blocking ask (abstraction) construct.

Here we argued for utcc as a declarative framework for modeling and verifying dynamic multimedia interaction systems. We showed that the synchronization mechanism based on entailment of constraints leads to simpler models that scale up when more agents are added. Moreover, we showed that systems can be formally verified with the underlying temporal logic in utcc. We modeled two non trivial interacting systems. The model proposed for interactive scores in Section 3 improved considerably the expressivity of previous models such as [START_REF] Allombert | A system of interactive scores based on Petri nets[END_REF]. It allows the composer to dynamically change the structure of the score according to the information derived from the environment.

The results presented here are so far encouraging although much remains to be done at the implementation level. Currently, to guarantee reliable responses in time, we are working on assessing the behavior of utcc processes in real-time contexts. We plan to provide a more principled notion of time where the duration of each time-unit can be related to the amount of computation involved in it. We also plan to enrich our FO model with probabilistic traversals of the graph in the lines of [START_REF] Perez | Non-determinism and probabilities in timed concurrent constraint programming[END_REF].

Figure 1 ,Fig. 1 .

 11 Figure 1, based on one from [3], shows an interactive score where temporal objects are represented as boxes. Objects are T i , durations D i . Object T 4 is a control point, whereas T 0 and T 3 are intervals. Duration D 3 should be such that D s ≤ D 3 ≤ D f . The whole

Fig. 2 .

 2 Fig. 2. A utcc model for Dynamic Interactive Scores

-Fig. 3 .

 3 Fig. 3. Example of an Interactive Score Execution

Fig. 4 .

 4 Fig. 4. A FO automaton for s = ab

=Fig. 5 .

 5 Fig. 5. Implementing the FO into utcc

⋆ This work has been partially supported by FORCES, an INRIA's Equipe Associée between the teams COMETE (INRIA), the Music Representation Research Group (IRCAM), and AVISPA.


Jesús Aranda

Gerard Assayag

Carlos Olarte

Jorge A Pérez

Camilo Rueda

Mauricio Toro

Frank D Valencia

An Overview of FORCES: An INRIA Project on Declarative Formalisms for Emergent Systems

The FORCES project aims at providing robust and declarative formalisms for analyzing systems in the emerging areas of Security Protocols, Biological Systems and Multimedia Semantic Interaction. This short paper describes FORCES's motivations, results and future research directions.

Introduction FORCES (FORmalisms from Concurrency for Emergent Systems) is an ongoing project funded by the Equipes Associées programme of INRIA. It is carried by the INRIA team COMETE (France), the IRCAM Music Representation Team (France) and the team AVISPA (Colombia). The main goal of FORCES is to provide robust declarative formalisms for modeling systems from emergent application areas of computer science in which our teams have been working during recent years: Namely, Security Protocols, Biological Systems and Multimedia Semantic Interaction.

Process calculi are formalisms that treat communicating processes much like the λ-calculus treats computable functions: The structure of terms reflects the structure of processes and process evolution is represented by term reduction. Concurrent Constraint Programming (CCP) based calculi [START_REF] Saraswat | The semantic foundations of concurrent constraint programming[END_REF] are computational models that combine the operational view of process calculi with a declarative one based upon logic. Some of the members of FORCES developed and used ntcc [START_REF] Nielsen | Temporal concurrent constraint programming: Denotation, logic and applications[END_REF], a timed CCP calculus, to predict the behavior of systems from Security Protocols [START_REF] Olarte | Universal concurrent constraint programing: Symbolic semantics and applications to security[END_REF], Systems Biology [START_REF] Gutiérrez | Timed concurrent constraint programming for analysing biological systems[END_REF] and Multimedia Semantic Interaction [START_REF] Rueda | A temporal concurrent constraint calculus as an audio processing framework[END_REF]. Although these areas differ significantly from one another, there is a crucial commonality in the analysis we wanted to perform in them: Reachability i.e., whether a system reaches a particular state. The ntcc calculus provides several reasoning tools for reachability analysis. These include a temporal logic, a proof system, verification techniques, and a denotational semantics.

Nevertheless, we have learned from our modeling experience and theoretical studies that ntcc is not sufficiently robust for these applications. E.g., some security protocols use a mechanism to allow communication of nonces (i.e., uniquely generated random number). The ntcc calculus can at best express this mechanism indirectly [START_REF] Valencia | Decidability of infinite-state Timed CCP processes and first-order LTL[END_REF]. Also, ntcc lacks constructs for quantitative information, which are essential for biological systems. Furthermore, we have identified musical settings exhibiting complex non-regular timed behavior that cannot be expressed in ntcc.

Our research strategy in FORCES has been, with the benefit of hindsight, to develop declarative formalisms for modeling systems from the above-mentioned areas as suitable extensions or specializations of ntcc. Our expertise in ntcc as well as our modeling experience have been fundamental for guiding our research.

This short paper provides an overview of FORCES. Further information can be found at http://www.lix.polytechnique.fr/comete/Forces. Declarative Models of Security Protocols A fundamental ability for security protocols is that of generating and communicating private nonces; process calculi for security therefore include mechanisms for creating and communicating local names. Neither ntcc nor its predecessor tcc [START_REF] Saraswat | Foundations of timed concurrent constraint programming[END_REF] features such mechanisms.

As a remedy to this, in [START_REF] Olarte | Universal concurrent constraint programing: Symbolic semantics and applications to security[END_REF] we introduced the Universal Timed CCP process calculus (utcc): a generalization of tcc that allows for the communication of local names (or links). This additional expressiveness paves the way for the declarative modeling of a wider class of systems, most notably dynamic ones.

We have endowed utcc with a number of reasoning techniques for reachability analysis. A symbolic semantics was defined to deal with problematic operational aspects involving infinitely many substitutions which often arise when modeling security protocols. The semantics uses temporal constraints to finitely represent infinitely-many substitutions; it has been used to exhibit secrecy flaws in some security protocols [START_REF] Olarte | Universal concurrent constraint programing: Symbolic semantics and applications to security[END_REF]. The utcc calculus also enjoys a declarative view of processes as First-Order Temporal Logic (FLTL) formulae [START_REF] Manna | The Temporal Logic of Reactive and Concurrent Systems: Specification[END_REF]. This allows for reachability analysis of utcc processes using FLTL techniques. For instance, in [START_REF] Olarte | Universal concurrent constraint programing: Symbolic semantics and applications to security[END_REF] we used the FLTL formulae representing the model of a protocol to know if it reaches a state where the attacker knows a secret.

We also defined a denotational semantics for utcc [START_REF] Olarte | The expressivity of universal timed CCP: Undecidability of monadic FLTL and closure operators for security[END_REF]. This way, processes can be represented as partial closure operators. As an application of the semantics, we identified a language for security protocols that can be represented as closure operators over a cryptographic constraint system. We showed that the least fixed point of such an operator may then be used to check a secrecy property in a protocol. To our knowledge, this is the first denotational account in the context of calculi for security protocols.

This way, our work has brought new semantic insights into the verification of security protocols, and is related to the research in security protocols from areas closely related to CCP. Namely, Constraint Programming (e.g. [START_REF] Bella | Soft constraint programming to analysing security protocols[END_REF]) and Logic Programming (e.g. [START_REF] Abadi | Analyzing Security Protocols with Secrecy Types and Logic Programs[END_REF][START_REF] Millen | The interrogator: A tool for cryptographic protocol security[END_REF]). To our knowledge there is no work on Security Protocols that takes advantage of the reasoning techniques of CCP. Declarative Models of Biological Systems Quantitative information is fundamental for biological systems. For example, behavior in most biochemical reactions is highly dependent on the presence of a certain amount of the substances involved. Very often, information is partial as obtaining exact values for parameterizing models is difficult. Unpredictable behavior is thus an inherent condition of the biologic phenomena, and one counts with partial behavioral information for describing system interactions. This partial information not only ignores elements on how reactions occur (e.g. what components actually interact), but also on when such reactions commonly happen (e.g. the relative speeds of the interacting components).

While the notion of partial quantitative information is central to CCP via constraints, partial behavioral information is actually the novelty of ntcc via non-deterministic and asynchronous operators. Our teams have already explored these advantages by analyzing mechanisms for cellular transport and genetic regulatory networks [START_REF] Gutiérrez | Timed concurrent constraint programming for analysing biological systems[END_REF][START_REF] Arbeláez | Timed Concurrent Constraint Programming in Systems Biology[END_REF].

A drawback of these models is their lack of explicit quantitative information. As hinted at above, a fundamental feature of any model of biological systems is the capability of exploiting any available quantitative information. In biological systems this is often represented as stochastic behavior. One then has a set of reactions each endowed with a rate representing their propensity or speed. When considering their execution, a race between them takes place and the fastest action is executed.

We have taken initial steps on the inclusion of stochastic information into an explicitly timed concurrent constraint process language [START_REF] Aranda | Stochastic behavior and explicit discrete time in concurrent constraint programming[END_REF]. We defined stochastic events in terms of the time units defined by the language: this provides great flexibility for modeling and allows for a clean semantics. Most importantly, by considering stochastic information and adhering to explicit discrete time, it is possible to reason about processes using quantitative logics (both discrete and continuous), while retaining the simplicity of calculi such as ntcc for deriving qualitative reasoning techniques (such as denotational semantics and proof systems). We plan to consolidate the framework outlined in [START_REF] Aranda | Stochastic behavior and explicit discrete time in concurrent constraint programming[END_REF], and to apply it to study systems such as the modeled in [START_REF] Cardelli | A process model of rho gtp-binding proteins in the context of phagocytosis[END_REF].

Declarative Models of Multimedia Semantic Interaction Interactivity in multimedia systems has become increasingly important. The aim is to devise ways for the machine to be an effective and active partner in a collective behavior constructed dynamically by many actors. In complex forms of multimedia interaction the machine is always adapting its behavior according to the information derived from the activity of the other partners who, in turn, adapt theirs according to the computer actions.

Constructing multimedia systems is thus a challenging task. Their core depends on powerful and consistent concurrent agents architectures. In this setting, ntcc has much to offer. Complex dynamic agent synchronization scenarios can be modeled cleanly and compositionally based on the synchronization mechanism provided by blocking ask constructs. Also, interactions on which little information is available can be conveniently represented using non-determinism. Most importantly, safety properties of the model, crucial in performance settings, can be formally proved to hold.

Quantitative information is also important in musical settings. In [START_REF] Pérez | Non-determinism and Probabilities in Timed Concurrent Constraint Programming[END_REF], we proposed pntcc, the first ntcc extension featuring probabilistic and non-deterministic choices. pntcc advocates the specification of probabilistic, reactive systems within non-deterministic environments. The calculus is equipped with an operational semantics that ensures consistent interactions between both kinds of choices. The semantics is also crucial in the definition of logic-based verification capabilities over system specifications. We have used pntcc for analyzing a scenario of interactive music improvisation (see the extended version of [START_REF] Pérez | Non-determinism and Probabilities in Timed Concurrent Constraint Programming[END_REF]). Probabilitistic information was shown to be useful to obtain a quantitative measure of the quality of an improvised sequence and to enhance the control the modeler has over the whole process.

Interactive scores [START_REF] Allombert | A system of interactive scores based on Petri nets[END_REF] are models for reactive music systems where weakly defined temporal relations between components specify a hierarchy of loosely coupled music processes. Although the hierarchical structure has been treated as static in previous works, there is no reason it should be so. In [START_REF] Olarte | A declarative language for dynamic multimedia interaction systems[END_REF], we propose a model for dynamic interactive scores where interactive points can be defined to adapt the score depending on the information inferred from the environment (say, a set of performers). We then broaden the interaction mechanisms available for the composer.

In [START_REF] Sarria | Real-time concurrent constraint programming[END_REF] we proposed rtcc, a model of real-time concurrent constraint programming which adds to ntcc the means for specifying and modeling real-time behavior. This calculus has constructs for modeling strong preemption and for defining delays within the same time unit. The operational semantics of rtcc supports resources, limited time and true concurrency. We showed the applicability of the rtcc calculus by giving more faithful models of various musical situations previously modeled in other CCP calculi.

In multimedia interaction settings the real-time execution of models is central. We have implemented a first prototype of an interpreter for ntcc specifications providing real-time interaction with the models developed in the calculus. The tool, called Ntc-cRT [START_REF] Toro | NtccRT: A Concurrent Constraint Framework for Real-Time Interaction[END_REF], also allows for the integration with music composition environments such as OpenMusic (OM, [START_REF] Bresson | Openmusic 5: A cross-platform release of the computerassisted composition environment[END_REF]). NtccRT provides a means to write a ntcc specification graphically (using OM) and then to compile it as an standalone program interacting with Midishare [START_REF] Fober | Midishare: une architecture logicielle pour la musique[END_REF]. The tool is available at http://ntccrt.sourceforge.net.

Future Directions: Automatic Verification Presently there are no automatic, nor machine-assisted, tools for the simulation and verification of concurrent systems specified in ntcc. Since we deal with complex and large systems, these tools are essential to our intended applications. In fact, the issue of automatic support has received little attention in the case of CCP formalisms. To our knowledge only Villanueva et al (e.g. [START_REF] Alpuente | Verifying Real-Time Properties of tccp Programs[END_REF][START_REF] Falaschi | Automatic verification of timed concurrent constraint programs[END_REF]) have addressed automatic verification but in the context of finite-state CCP systems. Several applications of ntcc are, however, inherently infinite-state. Automatic verification of large systems, not to mention infinite systems, is challenging because of the state explosion problem it poses-i.e., the number of states a system has is exponential in the number of processes.

We will take up this challenge by identifying ntcc fragments amenable to automatic verification and by developing techniques and tools to machine assist the verification of system properties in ntcc. We envisage two main complementary approaches for our purposes: (1) Automaton-based and symbolic techniques, and (2) Static and abstract interpretation techniques. We plan to use the automaton representations of processes used to prove the the decidability of the verification problem for ntcc [START_REF] Valencia | Decidability of infinite-state Timed CCP processes and first-order LTL[END_REF], together with the symbolic approach in [START_REF] Olarte | Universal concurrent constraint programing: Symbolic semantics and applications to security[END_REF] to ameliorate the state explosion problem. Finally, we expect to develop static and abstract interpretation techniques to extract representative information from system specifications. Such information can be used to reason about essential properties of systems behavior.

We plan to use Security Protocols to test the above-mentioned techniques and tools. In fact, the analysis of Security Protocols is typically carried out using symbolic verification techniques thus making them ideal application candidates. It is also worth noticing that computer simulation plays a fundamental role for Biological Systems because of their inherent complexity. We also plan to develop an ntcc simulation tool and use it as a test bench for (abstractions of) biological systems. We expect that the declarative and parametric nature of ntcc should provide bench biologists with a tool for computing with and analyzing these systems that is intuitive.