Luca Battisti

Damiano Macedonio

Massimo Merro

Statistical Model Checking of a Clock Synchronization Protocol for Sensor Networks

This paper uses the statistical model checking tool in the UP-PAAL toolset to test the robustness of a distributed clock synchronization algorithm for wireless sensor networks (WSN), in the case of lossy communication, i.e., when the WSN is deployed in an environment with significant multi-path propagation, leading to interference. More precisely, the robustness of the gMAC protocol included in the Chess WSN platform is tested on two important classes of regular network topologies: cliques (networks with full connectivity) and small grids (where all nodes have the same degree). The paper extends previous work by Hedaraian et al. that only analyzed this algorithm in the ideal case of non-lossy communication, and only in the case of cliques and line topologies. The main contribution is to show that the original clock synchronization algorithm is not robust to changing the quality of communication between sensors. More precisely, with high probability the algorithm fails to synchronize the nodes when considering lossy communication over cliques of arbitrary size, as well as over small grid topologies.

Introduction

Wireless sensor networks (WSNs) are (possibly large-scale) networks of sensor nodes deployed in strategic areas to gather data. Sensor nodes collaborate using wireless communications with an asymmetric many-to-one data transfer model. Typically, they send their sensed data to a sink node which collects the relevant information. WSNs are primarily designed for monitoring environments that humans cannot easily reach (e.g., motion, target tracking, fire detection, chemicals, temperature); they are used as embedded systems (e.g., biomedical sensor engineering, smart homes) or mobile applications (e.g., when attached to robots, soldiers, or vehicles).

In wireless sensor networks, the basic operation is data fusion, whereby data from each sensor is agglomerated to form a single meaningful result. The fusion of individual sensor readings is possible only by exchanging messages that are timestamped by each sensor's local clock. This mandates the need for a common notion of time among the sensors which is achieved by means of so called clock synchronization protocols [START_REF] Sundararaman | Clock synchronization for wireless sensor networks: a survey[END_REF][START_REF] Wu | Clock synchronization of wireless sensor networks[END_REF].

In this paper we do model checking of a distributed algorithm of clock synchronization for WSNs that has been developed by the Dutch company Work partially supported by the PRIN 2010-2011 project "Security Horizons".

CHESS [START_REF]QUASIMODO: Preliminary description of case studies, deliverable 5[END_REF]. In order to realize an energy efficient communication mechanism, CHESS developed a gossip-based MAC algorithm [START_REF] Van Vessem | WSN gMAC protocol specifications[END_REF] (abbreviated gMAC) which is responsible for regulating the access to the wireless shared channel.

Here we are interested in verifying the robustness of the gMAC algorithm in the presence of packet loss. Packet loss is particularly relevant in wireless sensor networks which are deployed in environments with significant multi-path distortion (when part of the signal goes to the destination while another part bounces off an obstruction and then goes on to the destination). Most of sensor platforms do not have enough frequency diversity to reject multi-path propagation.

Our work has been strongly inspired by a recent analysis [START_REF] Heidarian | Analysis of a clock synchronization protocol for wireless sensor networks[END_REF] of the gMAC synchronization protocol on clique and line topologies, in the ideal case of nonlossy communication. In the case of line topologies, paper [START_REF] Heidarian | Analysis of a clock synchronization protocol for wireless sensor networks[END_REF] shows that the protocol fails to synchronize all nodes, when the number of nodes grows. On the other hand, on clique topologies the protocol behaves quite well and the paper provides constraints on guard times (delays added before and after the transmission of sync messages) to guarantee clock synchronization, independently on the clique size. In [START_REF] Heidarian | Analysis of a clock synchronization protocol for wireless sensor networks[END_REF] the protocol is modeled as a network of timed automata and verified using the UPPAAL model checker [START_REF] Behrmann | SFM-RT 2004[END_REF][START_REF] Behrmann | QEST 2006[END_REF]. However, the model in [START_REF] Heidarian | Analysis of a clock synchronization protocol for wireless sensor networks[END_REF] does not incorporate several features such as dynamic slot allocation, uncertain communication delays, and unreliable radio communication. In the current paper we extend their analysis by adopting a probabilistic model of radio communication that takes into account message loss according to the measurement of packet delivery suggested in [START_REF] Zhao | Understanding packet delivery performance in dense wireless sensor networks[END_REF]. As our model is a network of probabilistic timed automata, we decided to do our analysis by applying Statistical Model Checking (SMC) [START_REF] David | Time for statistical model checking of real-time systems[END_REF] within the UPPAAL toolset [START_REF] Behrmann | SFM-RT 2004[END_REF][START_REF] Behrmann | QEST 2006[END_REF]. SMC consists in monitoring a proper number of runs of the system and then applying a statistical algorithm to obtain an estimate of the result of the desired query.

Our analysis shows that low guard times (within the safety range proposed in [START_REF] Heidarian | Analysis of a clock synchronization protocol for wireless sensor networks[END_REF]) are not sufficient to guarantee clock synchronization in clique topologies of arbitrary size. More precisely, in the case of lossy communication, the size of the clique does play a crucial role in the effectiveness of the protocol: the bigger is the clique the higher must be the guard time to ensure clock synchronization with high probability. Here it is important to notice that guard times cannot be arbitrary increased without dramatically affecting the duration of the battery life of the sensor nodes [START_REF] Assegei | Decentralized frame synchronization of a TDMA-based wireless sensor network[END_REF]. Finally, we move our analysis on grid topologies, with increasing neighbor degree, to better simulate a uniform node distribution of sensor nodes in a given area. Our simulations show that high values of the guard times may be not sufficient to guarantee clock synchronization in the presence of message loss, even in small 5 × 5 grid networks. On the other hand, we observe that the efficiency of the protocol improves when the number of neighbours, and hence node connectivity, increases.

Outline Section 2 introduces the gMAC protocol. Section 3 illustrates the corresponding UPPAAL probabilistic model. Section 4 details our analysis on cliques and grid topologies. Section 5 concludes the paper with final remarks, future and related work.

The gMAC protocol

The gMAC protocol is a Time Division Multiple Access (TDMA) protocol, where time is divided into fixed length frames, and each frame is subdivided into slots. Slots can be either active or idle. During active slots, a node is either listening for incoming messages from neighbouring nodes (RX slot) or it is sending a message (TX slot). During idle slots a node is switched to energy saving mode. Active slots are gathered in a contiguous sequence placed at the beginning of each frame.

Structure of a time frame:

RX • • • RX TX RX • • • RX idle slots
Structure of an active slot:

← g → sending/receiving ← t →
Since energy efficiency is a major concern in the design of wireless sensor networks, the number of active slots is typically much smaller than the total number of slots. In the implementation of gMAC the number of slots within a frame is 1129 out of which 10 are active. A node can only transmit a message once per time frame in its TX slot. If two neighbouring nodes choose the same send slot then a communication collision will occur in the intersection of their transmission ranges preventing message delivery. In the original protocol a node randomly chooses an active slots as send slot (TX slot) considering all other active slots as receive slots (RX slots). However, for the sake of simplicity, as in [START_REF] Heidarian | Analysis of a clock synchronization protocol for wireless sensor networks[END_REF], in our analysis we assume that the TX slots are fixed and have been chosen in such a way that no collision occurs.

In order to ensure that when a node is sending all its neighbours are listening, guard times are introduced. This means that each sender waits for some time (g clock cycles) at the beginning of its TX slot to ensure that all its neighbours are ready to receive messages; similarly, a sender does not transmit for a certain amount of time (t clock cycles) at the end of its TX slot. Guard times cannot be arbitrary increased without dramatically affecting the duration of the battery life of the sensor nodes [START_REF] Assegei | Decentralized frame synchronization of a TDMA-based wireless sensor network[END_REF]. So, the choice of proper guard time values is crucial in the protocol design. In the current implementation, each slot consists of 29 clock cycles, out of which 18 cycles are used as guard time.

The CHESS sensor nodes come equipped with a 32 kHz crystal oscillator that drives an internal clock used to determine the beginning and the end of each slot. Sensor nodes are also equipped with an ATMega64 micro-controller and a Nordic nRF24L01 [START_REF]Nordic Semiconductors: nRF2401 Single-chip 2.4GHz Transceiver Data Sheet[END_REF] packet radio. Depending on the environment, the Nordic nRF24L01 radio has a transmission range between 0.5m and 50m, For the sake of simplicity we assume that all nodes have the same transmission range; this means that the transmission between nodes is assumed to be symmetric.

UPPAAL Probabilistic Model for gMAC

In this section, we provide a small extension of the UPPAAL model for gMAC of [START_REF] Heidarian | Analysis of a clock synchronization protocol for wireless sensor networks[END_REF] in which a probabilistic choice to model message loss is introduced. The For each node i there are two state variables: clk[i], which records the value of the hardware clock (initially 0), and csn[i], which records the current slot number (initially 0). Furthermore, there are two broadcast channels: tick[i], used to synchronize the activities within the node i, and start message[i], used to inform all neighbours of the beginning of i's transmission. Table 1 reports the protocol parameters.

Figure 1 Clock(i)

x := 0, clk[i] := (clk[i] + 1) % k0 x >= min X0 tick[i]! x <= max
Figure 1 depicts the automaton Clock(i) of [START_REF] Heidarian | Analysis of a clock synchronization protocol for wireless sensor networks[END_REF] modeling the hardware clock of node i. The local clock variable x measures the time between two consecutive clock ticks. A tick[i]! action is enabled when x reaches the value min and must fire before x reaches the value max. When the action tick[i]! occurs the variable x is reset to 0 and the variable clk[i] is incremented by 1. As explained in [START_REF] Heidarian | Analysis of a clock synchronization protocol for wireless sensor networks[END_REF], the state variable clk[i] is reset after k 0 clock ticks for the model checking to become feasible. A realistic clock drift rate is about 20 ppm (parts-per-million). Such a

Figure 2 WSN(i) start_message[i]! tick[i]? tick[i]? tick[i]? clk[i]==k0-1 clk[i]==k0 -t -1 csn[i]==tsn[i] && clk[i]==g -1 GO_SEND WAIT SENDING csn[i] := (csn[i]+1) % C
rate is achieved in the model by setting min = 10 5 -2 and max = 10 5 + 2. In the model of [START_REF] Heidarian | Analysis of a clock synchronization protocol for wireless sensor networks[END_REF] ticks may nondeterministically occur within the time interval [min, max]; thus the delay between two tick[i]! actions is nondeterministic. The stochastic semantics for timed automata of UPPAAL SMC excludes nondeterminism; thus the delay between two tick[i]! actions is implemented as a uniformly distributed stochastic delay. This may be non-realistic in general: clocks usually run either too fast or too slow for long periods of time, due to environmental differences. However in our analysis we will focus on small networks and we will assume all sensors being in the same environmental conditions. Thus we exploit UPPAAL SMC's random clock speed jitter.

Figure 2 describes automaton WSN(i) of [START_REF] Heidarian | Analysis of a clock synchronization protocol for wireless sensor networks[END_REF] devoted to message sending. The automaton waits in the initial location WAIT until the current slot number csn[i] equals the TX slot tsn[i], and g ticks occur in that slot. Then the automaton moves to the location GO SEND which is immediately left by performing a start message[i]! action. This action leads the automaton to the location SENDING. The automaton remains in this location until the beginning of the tail interval (which starts after k 0 -t ticks). Then the automaton returns to the location WAIT where it increments the current slot number csn[i] every k 0 ticks.

Figure 3 Synchronizer(i) S0 S1 clk[i]:= g+1 (csn[i] < n) && neighbour(i,j) j:Nodes loss 100 -loss tick[i]? start_message[j]?
Figure 3 contains the automaton Synchronizer(i) which is devoted to synchronize the hardware clock. We enrich the corresponding automaton of [START_REF] Heidarian | Analysis of a clock synchronization protocol for wireless sensor networks[END_REF] with a simulation of message loss on the channel start message [i]. The UPPAAL model checker features branching edges with associated weights for the probabilistic extension. Thus we define an integer constant loss, with 0 ≤ loss ≤ 100, and every node can either lose a message with weight loss or receive it with weight (100-loss). The automaton Synchronizer(i) waits in its initial location S0 until it detects, in an active slot (csn[i] < n), the beginning of a new message from a neighbor j (action start message[j]?). When this happens the automaton moves to a committing location C and it immediately goes to a branching edge where: (i) with weight loss it returns in its initial location S0 and (ii) with weight 100-loss it goes to location S1. Case (i) formalizes the loss of the starting message from node j, while case (ii) formalizes the reception of the same message. Notice that UPPAAL requires input determinism to ensure that the system to be tested always produces the same outputs on any given sequence of inputs. Thus we need an extra intermediate location instead of branching immediately on the start message[j]! action. Notice also that the start message[j]! action occurs exactly when clk[j] = g (as a result of the synchronization of automata WSN(j) and CLOCK(j)); while the node i, by means of automaton Synchronizer(i), resets the variable clk[i] to g + 1 after a further tick. The guard neighbor(i, j) indicates that i and j are in the transmission range of each other. Formally, neighbor() is a symmetric function related to the slot allocation in the following manner [START_REF] Heidarian | Analysis of a clock synchronization protocol for wireless sensor networks[END_REF]:

neighbor(i, j) =⇒ tsn[i] = tsn[j] neighbor(i, j) ∧ neighbor(i, k) =⇒ tsn[j] = tsn[k] (1)
This means that whenever two nodes are neighbours or have a common neighbor then they must have distinct TX slot numbers. The function neighbor() is helpful to provide a formal definition of synchronized sensor networks. Intuitively, a sensor network is said to be synchronized if, whenever a node is sending in a given slot number then all neighbouring nodes are in the same slot number.

Definition 1. A network is said to be synchronized if for all reachable states ( ∀i, j ∈ Nodes )( (

SENDING i ∧ neighbor(i, j) ) =⇒ ( csn[i] = csn[j] ) ).

Our Analysis

UPPAAL Statistical Model Checker [START_REF] David | Time for statistical model checking of real-time systems[END_REF] evaluates properties on execution runs of a network of probabilistic timed automata. The execution time of these runs is represented by a variable time. It is left to the user to set a bound to this variable.

In particular, fixed a constant value bound, the Statistical Model Checker can reply to queries of the following shape

Pr[time<=bound] (<> expr)
by performing an adequate number of runs to estimate the probability to reach a state which satisfies the property expr, within the time bound. The user must fix two main statistical parameters, α and ε, both in the real interval ]0, 1[ . The answer provided by the tool is a confidence interval [p -ε, p + ε] where α represents the probability of the answer of being wrong. The higher is the precision of the analysis the bigger must be the number of runs performed by the simulator. Thus the waiting time for a reply of a query depends both on the length of runs, i.e. on the parameter bound, and on the statistical parameters ε and α.

In order to make feasible our analysis we try to understand if we can change some system parameters without affecting the quality of the analysis. In particular, we focus on the parameter C that is the number of slots composing a frame. The effectiveness of any synchronization protocol is crucially based on the exchange of some timing information to synchronize neighbor nodes. Said in other words, the longer nodes remain silent the quicker they get out of sync, because they do not get enough information to synchronize with each other. As consequence, once fixed the number of active slots, if the system gets out of sync with probability p, for a certain value of C, then the same system will get out of sync more quickly (or with higher probability) for a bigger value of C.

The parameter loss expresses the probability of message loss at the physical level due to the unreliability of the wireless medium. In our analysis, we will instantiate loss according to the results appeared in [START_REF] Zhao | Understanding packet delivery performance in dense wireless sensor networks[END_REF], where packet delivery performances of WSNs have been studied at physical layer under different transmission powers and physical-layer encodings. In that analysis, 60 Mica motes have been used to measure packet delivery under three different environmental settings: office building, open parking lot, habitat with moderate foliage. Under these settings, results show that the physical layer contributes to the packetdelivery performance, which is defined as the fraction of packets not successfully received by the receiver within a time window.

For the sake of simplicity, all nodes of our networks will be instantiated with the same value of the parameter loss. According to [START_REF] Zhao | Understanding packet delivery performance in dense wireless sensor networks[END_REF] this parameter will be set to: 10, to approximate the average message loss in a parking lot; 20, to model the average message loss in a office building; and 30, which represents the average message loss in an habitat setting with moderate foliage.

Verifying Clique Topologies

Paper [START_REF] Heidarian | Analysis of a clock synchronization protocol for wireless sensor networks[END_REF] derives necessary and sufficient constraints on the guard times to guarantee the correctness of the protocol on clique topologies in the case of perfect communication. These constraints depend on the clock ratio min/max, on the parameter k 0 and on the maximal distance M between two transmitting slots1 ; they do not depend on the size N of the network. They are:

g > 1 -min max • M • k 0 + min max g < 1 -max min • M • k 0 + k 0 -2 t > 1 -min max • (k 0 -g) + min max (2)
From an analysis of these conditions, paper [START_REF] Heidarian | Analysis of a clock synchronization protocol for wireless sensor networks[END_REF] demonstrates that guard time values g = t = 3 are sufficient to guarantee clock synchronization in a clique of arbitrary size. Here we want to demonstrate that, in the presence of packet loss, the size of the clique network does play a crucial role. In particular, the bigger is the clique the higher must be the value of g (and t) to ensure clock synchronization. Said in other words: in the presence of message loss, fixed a value of g (and t), there is always a clique which gets out of sync with high probability.

For networks with full connectivity clock synchronization means that all nodes of the network agree on the current slot. As a consequence, Definition 1 can be rephrased as in [START_REF] Heidarian | Analysis of a clock synchronization protocol for wireless sensor networks[END_REF] in the following manner: Definition 2. A clique network is said to be synchronized if for all reachable states it holds the following:

(∀i, j ∈ Nodes)(SENDING i =⇒ csn[i]=csn[j]).
So, in order to estimate the probability of going out of synchronization we will use UPPAAL SMC to perform the following quantitative check:

Pr[time<=bound] (<> exists(i:Nodes) exists(j:Nodes) (WSN(i).SENDING and not(csn

[i]==csn[j])) (3)
Simulation setting In our simulations on cliques, all protocol parameters will satisfy the constraints in [START_REF] Behrmann | SFM-RT 2004[END_REF]. As in [START_REF] Heidarian | Analysis of a clock synchronization protocol for wireless sensor networks[END_REF], the guard time t is chosen to be the same as g. Parameter tsn[i] is chosen equal to i, as fully connectivity implies a different TX slot for each node. We set k 0 = 29. Unfortunately, we cannot set C = 1129, as in the real implementation, because the length of the runs that can be analyzed by UPPAAL is limited: in order to avoid integer overflow, the parameter bound cannot overtake the value 2 • 10 9 . This means that if we would keep C close to the real value, then our execution runs would last for just a single time frame and they would be too short to provide any significant result. According to the discussion done in the preface of this section we perform our analysis for low values of the parameter C. This modification does not affect our analysis. As an example, in Table 2 we consider cliques with N = 10, 15, loss = 20 and g = 3, 4.

We then perform the quantitative check (3) by varying C and keeping constant the number of observed time frames. The value p represents the center of the confidence interval computed by UPPAAL SMC. Every check required 6623 runs of the protocol and lasted for about four days on a Intel core i5-2420M CPU 2.30GHz with 6G RAM. We gradually increased the precision of the parameter ε in order to achieve an interval which does not include the value 0 as a reply; in other words we have looked for lower bounds p -ε > 0. Table 2 outlines that when the number of time frames is fixed then the probability of going out of sync for the system does not decrease when the parameter C increases (similar results can be obtained for different values of N, g, loss and for different topologies). As a consequence, our simulations provide a lower bound of the probability of getting out of sync in a setting with C = 1129.

In Table 3 we study the behaviour of the protocol on cliques up to 30 nodes. We vary the number of nodes N, the guard time g and the parameter loss. Since we consider fully connected networks and the transmitting slots are grouped at the beginning of each time frame, we fix C = N+2, as in [START_REF] Heidarian | Analysis of a clock synchronization protocol for wireless sensor networks[END_REF], to allow at least two idle slots at the end of each frame. We set the statistical parameters ε = 0.025, α = 0.05 to have meaningful results. We check property (3) on the maximal run UPPAAL SMC can handle without incurring in integer overflow. The result of the quantitative check is represented by the probability p, which is the center of the confidence interval computed by UPPAAL SMC. Every check required 2952 runs of the protocol. In the following table we report the time required by our simulations on a Intel core i3-2310M CPU 2.10GHz with 4G RAM. 3 are quite short (from 30 to 60 frames, depending on N); however, they are long enough to deduce some significant observation. For instance, we notice that once fixed the value of the guard time g, the probability of going out of sync increases when either N or loss increase. Moreover, once fixed both N and loss, the probability p decreases when the guard time g increases. Since the probability of going out of sync cannot decrease when going to longer runs, in Table 3 we compare probabilities associated to runs of different lengths. In particular, we notice that if we fix loss and g then the probability of getting out of sync increases when N increases. At the end of this section we will compare runs of the same length. The analysis provided in Table 3 says also that the protocol is certainly not suitable in certain scenarios. For instance, in a clique of at least 10 nodes with g = 3 the system will get immediately out of sync with high probability if the loss probability is greater than 0.2. In other settings the results are not that strong. This is the case of a clique with 10 nodes, g = 4 and loss = 20. In this case, our analysis says that this system will get out of sync with probability 0.025. Such a value is ten times smaller than the loss probability, too small to conclude anything, at least in a so short run. Unfortunately, a priori, we cannot predict the behaviour of the system for longer runs as the probability p may increase or stabilize. In the following we will try to overcome this limitation.

UPPAAL SMC can simulate the behaviour of our systems on runs limited in size, called execution modules. At the beginning of an execution module all nodes are in the same time slot and with the same value in their clock variables. At the end of an execution module, UPPAAL SMC computes an estimate of the probability p to reach a state which does not satisfy Definition 2. This definition does not identify a single state of the system: nodes may have different clock values while still being in the same time slot. We claim that the initial state, where all nodes begin the execution module with the same clock value, is the state which has the smallest probability to lead the system out of sync. In order to support our argument, we provide an example in Table 4. We consider cliques of 5 and 10 nodes, with g = 4, C = 7 and loss = 20. Table 4 shows experiments in which the system starts from a state that satisfies Definition 2 while internal clocks may have different values. The starting value of every internal clock is randomly chosen from a fixed interval I of clock values. Runs are 30 time frames long. We set α = 0.05. It can be noticed that the smallest desync probability is obtained when the execution module starts in the initial state where all nodes have the same clock value. Similar results can be obtained for other values of N, g, C and loss.

In virtue of this observation, we can divide a long run in consecutive execution modules, all starting in the initial state. Then, we can derive by composition a lower bound of the probability of desynchronization for that run. Thus, if [pε, p + ε] is the confidence interval provided by UPPAAL SMC after performing the quantitative check (3) within an execution module, then the probability of going out of sync within n execution modules is at least Table 5 extends the results of Table 3 to longer runs which lasts for 300, 600 and 900 time frames, respectively. The forth column of Table 5 reports the lower bound of the confidence interval of an execution module. When N = 10, 15, 20, 30 the execution module studied in Table 3 lasts for approximately 60, 40, 30 and 20 time frames respectively. Thus, by applying the formula (4) with n = 5, 8, 10, 15 we obtain a lower bound for the probability of being out of sync within 300 time frames in the cases of cliques with 10, 15, 20 and 30 nodes, respectively. Analogously when n = 10, 15, 20, 30 and n = 15, 22, 30, 45 we obtain a lower bound for the probability of being out of sync within 600 and 900 time frames, respectively.

1 -(1 -(p -ε)) n . (4)
As discussed at the beginning of this section, the values of Table 5 represent also lower bounds of the probability of desynchronization for the real implementation. In the real setting, with C = 1129 and clock frequency of 32 kHz, a time frame lasts for about 1sec. As a consequence, Table 5 expresses a lower bound of the probability of getting out of sync within 5, 10 and 15 min. Thus, when g = 3 the probability of getting out of sync is high also for small networks and increases as long as N increases. The probability of getting out of sync within 5min increases dramatically when N reaches 10: the network gets out of sync almost certainly. The value g = 4 is enough for small networks (around 10 nodes), but when N = 15 we have a probability of being out of sync of almost 0.4 in 15min. When N = 20 the probability reaches 0.7 in less than 15min. When N = 30 the probability reaches 0.7 in less than 5min. These results outline an increasing of the desync probability when the number of nodes increases.

Verifying Grid Topologies

Clock synchronization in clique topologies has been studied in [START_REF] Heidarian | Analysis of a clock synchronization protocol for wireless sensor networks[END_REF] as a first step towards more realistic topologies. Usually sensor nodes have a limited number of neighbours and do not have direct communication with the whole network. In this section, we study how the gMAC synchronization protocol behaves on regular topologies which better simulate a uniform node distribution in a given area 2 . In particular, we will focus on grid topologies where nodes have a uniform number of neighbours. Unlike cliques, there are no theoretical results suggesting how to choose protocol parameters to guarantee the synchronization of grid networks in the case of non-lossy communication. The implementation of gMAC adopts an high guard time, g = 9, to ensure synchronization in networks with arbitrary topologies. In this section, we study whether high values of g guarantee node synchronization in grid-based networks, in the case of lossy communication.

In our simulations we focus on a small sensor network where nodes are placed in a 5×5 grid, thus N = 25. Unlike cliques, grid topologies do not need a different TX slot for each node: we can allocate the same TX slot to different nodes provided that when two nodes are neighbours or have a common neighbor then they get distinct TX slot numbers. According to the implementation of gMAC, where the number of TX slots is limited, we consider the minimum number of TX slots to be allocated to satisfy conditions [START_REF] Assegei | Decentralized frame synchronization of a TDMA-based wireless sensor network[END_REF]. The number of transmission slots depends on the number of neighbours for each single node; if a node v has k neighbours then we need a TX slot in which v transmits and all its neighbours listen, and k distinct slots in which each neighbor transmits and v listens. Thus if k represents the maximum node degree, then we need at least k + 1 TX slots.

In the following we analyze the behaviour of the protocol on grid topologies by considering three possible maximum node degrees: 4, 6 and 8. These grid networks require at least 5, 7 and 9 TX slots, respectively. Below we report the three topologies we consider along with a simple slot allocation which satisfies conditions (1) by using exactly k + 1 TX slots, where k is the maximum node degree. The grid structures outlines the network topology while the identifiers 0, 1, . . . show the TX slot allocated for the corresponding node. for almost 100, 80 and 65 time frames when the maximum node degree is 4, 6 and 8, respectively. These are quite short runs, but long enough to conclude that the system may get out of sync also for high values of the guard time g. The result of the quantitative check is reported in Table 6. The value p represents the center of the confidence interval computed by UPPAAL. The compositional reasoning on execution modules adopted for cliques can be easily generalized to grid topologies. Table 7 fixes loss = 20 and g = 6. It reports lower bounds to the probability of getting out of sync within 900, 1800, 2700 and 3600 time frames. As said before, in the real implementation a time frame lasts for around 1sec. Thus, when considering g = 6 and a message loss of 20%, we observe that the desync probability exceeds 0.5 in less than 15min for degree 4, in less than 30min for degree 6, and in less than 45min for degree 8. Table 7 outlines also how the performances of the protocol depend on the node degree: the probability of getting out of sync decreases for grid topologies with higher node degree.

Finally, let us give a taste of what happens when g = 7. Among the results on Table 6 we extend the case of degree 4 and loss = 20, where the probability of getting out of sync within 100 time frames lays in the interval [0.03 , 0.09]. The projection to 2700 time frames says that the probability of getting out of sync becomes greater than 0.54. In the real settings, this means that the probability of getting out of sync exceeds 0.5 in less than 45min.

In conclusion, in the case of lossy communication, small grid topologies have a high probability of getting out of sync even for high values of the guard time g and for low values of the loss probability. Moreover the probability of getting out of sync increases when decreasing the maximum node degree.

Conclusions, Future and Related Work

Our work has been strongly inspired by a recent analysis [START_REF] Heidarian | Analysis of a clock synchronization protocol for wireless sensor networks[END_REF] of the gMAC synchronization protocol on clique and line topologies, in the ideal case of non-lossy communication. That analysis provides constraints on the protocol parameters that are both necessary and sufficient for the correctness of the protocol for cliques of arbitrary size. Here we have carried on the work of [START_REF] Heidarian | Analysis of a clock synchronization protocol for wireless sensor networks[END_REF] in the case of lossy communication. We have extended their model and obtained a network of probabilistic timed automata [START_REF] David | Statistical model checking for networks of priced timed automata[END_REF] which has been used for doing Statistical Model Checking within the UPPAAL toolset [START_REF] David | Time for statistical model checking of real-time systems[END_REF]. As a main result, we have showed that in the presence of message loss the constraints provided in [START_REF] Heidarian | Analysis of a clock synchronization protocol for wireless sensor networks[END_REF] may be not sufficient to ensure clock synchronization of cliques of arbitrary size. Then, we have extended our analysis of the protocol to small grid topologies and again found that, in the case of lossy communication, the nodes of the grid may get out of sync with high probability. More interestingly, grid topologies with higher node degree have a smaller probability of desynchronization. This lets us to conjecture that higher connectivity helps synchronization protocols. In this respect, among the regular topologies, clique topologies are those with the best performances!

As in [START_REF] Heidarian | Analysis of a clock synchronization protocol for wireless sensor networks[END_REF] we have assumed a fixed slot allocation. However, the implementation of gMAC includes a probabilistic dynamic slot allocation algorithm. The only analysis we are aware of the probabilistic gMAC algorithm appears in [START_REF] Yue | Analyzing energy consumption in a gossiping mac protocol[END_REF]. In that paper, mobile sensors do not use a fixed schedule to control medium access but instead employ gMAC's full decentralized slot allocation: gossiping is introduced to allow each node to decide when to send. Paper [START_REF] Yue | Analyzing energy consumption in a gossiping mac protocol[END_REF] analyzes the energy-efficiency of gMAC under the assumption of perfect clock synchronization. The protocol, formalised in the MoDeST language [START_REF] Bohnenkamp | MODEST: A compositional modeling formalism for hard and softly timed systems[END_REF], is evaluated using the discrete-event simulator of the Möbius tool suite. We are planning to study the performance of the gMAC protocol with dynamic slot allocation in the case of lossy communication and realistic clock. In doing that, we intend to adopt either a (truncated) normal distribution or a (truncated) exponential distribution for modeling a more realistic delay between consecutive ticks.

Statistical Model Checking allows us to study networks of bigger size with respect to the state-of-the art model checking technology, such as PRISM [START_REF] Kwiatkowska | PRISM 4.0: Verification of probabilistic real-time systems[END_REF][START_REF] Norman | Model checking for probabilistic timed automata[END_REF]. SMC can be seen as a trade off between testing and formal verification: its approach consists in performing an appropriate number of simulations which are elaborated with statistical algorithms to verify if a given property is satisfied with a certain probability. Unlike an exhaustive approach, a simulation-based solution does not guarantee a correct result with a 100% confidence. It is only possible to bound the probability of making an error. In order to study bigger systems with an higher confidence, paper [START_REF] Bulychev | Checking and distributing statistical model checking[END_REF] proposes a distributed implementation of UPPAAL SMC by means of a master/slave architecture where several computers are used to generate simulations and a single master process is used to collect those simulations and perform the statistical test. We are planning to employ this approach to extend the confidence of the results we obtained in this paper.

7

 7 hours 20 2 days 23 hours 30 9 days 4 hours All runs in Table

Table 1

 1 Protocol parameters

	Parameter Description	Constraints
	N	number of nodes	0 < N
	C	number of slots in a time frame	0 < C
	n	number of active slots in a time frame	0 < n ≤ C
	k0	number of clock ticks in a time slot	0 < k0
	csn[i]	current slot number for node i	0 ≤ csn[i] < n
	tsn[i]	TX slot number for node i	0 ≤ tsn[i] < n
	clk[i]	clock value for node i	0 ≤ clk[i] < k0
	g	guard time	0 < g
	t	tail time	0 < t
	min	minimal time between two clock ticks	0 < min
	max	maximal time between two clock ticks	min ≤ max
	loss	message loss probability	0 ≤ loss ≤ 100
	model assumes a finite, fixed set of sensor nodes Nodes = {0, . . . , N -1}. The
	behaviour of each individual node i ∈ Nodes is described by means of three
	different timed automata: Clock(i), WSN(i), Synchronizer(i). Automaton
	Clock(i) models the hardware clock of the node, WSN(i) takes care of sending
	messages, and Synchronizer(i) re-synchronizes the hardware clock upon receipt
	of a message. The automaton Synchronizer(i) is the only one where probabil-
	ities are introduced to model packet loss. The complete model consists of the
	composition of the three automata Clock(i), WSN(i) and Synchronizer(i),
	for each i ∈ Nodes.

Table 2

 2 On the parameter C.

	g N C	bound frames	p	ε	α
	3 10 12 0.07 • 10 9	2	0.025 0.02 0.01
	3 10 48 0.28 • 10 9	2	0.029 0.02 0.01
	3 10 192 1.12 • 10 9	2	0.031 0.02 0.01
	3 10 336 2.00 • 10 9	2	0.031 0.02 0.01
	4 15 17 0.50 • 10 9	10	0.022 0.01 0.05
	4 15 34 1.00 • 10 9	10	0.027 0.01 0.05
	4 15 68 2.00 • 10 9	10	0.027 0.01 0.05

Table 3

 3 Cliques and node number. Maximal run length. α = 0.05, ε = 0.025

	N = 10 frames: 60	N = 15 frames: 40	N = 20 frames: 30	N = 30 frames: 20
	g loss	p	g loss	p	g loss	p	g loss	p
	3 10	0.059	3 10	0.100	3 10	0.133	3 10	0.236
	3 20	0.386	3 20	0.560	3 20	0.692	3 20	0.851
	3 30	0.787	3 30	0.931	3 30	0.972	3 30	0.992
	4 10	0.000	4 10	0.000	4 10	0.003	4 10	0.005
	4 20	0.025	4 20	0.046	4 20	0.063	4 20	0.106
	4 30	0.155	4 30	0.243	4 30	0.325	4 30	0.464

Table 4

 4 Module comparison -g = 4, α = 0.05, run length 30 frames -

		N = 5			N = 10
	I	p	ε	I	p	ε
	[0]	0.019 0.01	[0]	0.015 0.01
	[0, . . . , 4] 0.113 0.030	[0, . . . , 4] 0.113 0.030
	[0, . . . , 9] 0.665 0.050	[0, . . . , 9] 0.677 0.030
	[0, . . . , 14] 0.827 0.050	[0, . . . , 14] 0.816 0.030

Table 5

 5 Quantitative check on cliques with loss = 20 and α = 0.05

	g N C p -ε 300 frames 600 frames 900 frames
	3 10 12 0.361 ≥ 0.893	≥ 0.989	≥ 0.999
	3 15 17 0.535 ≥ 0.998	≥ 0.999	≥ 0.999
	3 20 22 0.667 ≥ 0.999	≥ 0.999	≥ 0.999
	3 30 32 0.826 ≥ 0.999	≥ 0.999	≥ 0.999
	4 15 17 0.021 ≥ 0.156	≥ 0.273	≥ 0.373
	4 20 22 0.038 ≥ 0.321	≥ 0.539	≥ 0.687
	4 30 32 0.081 ≥ 0.718	≥ 0.920	≥ 0.980

Table 6

 6 Grids 5 × 5 and node degree. Maximal run length. α = 0.05, ε = 0.03

	max degree 4	max degree 6	max degree 8
	g C loss	p	g C loss	p	g C loss	p
	6 7	0	0	6 9	0	0	6 11 0	0
	6 7 10 0.03	6 9 10 0.01	6 11 10	0
	6 7 20 0.11	6 9 20 0.07	6 11 20 0.05
	6 7 30 0.45	6 9 30 0.25	6 11 30 0.19
	7 7	0	0	7 9	0	0	7 11 0	0
	7 7 10 0.01	7 9 10	0	7 11 10	0
	7 7 20 0.06	7 9 20 0.03	7 11 20 0.02
	7 7 30 0.28	7 9 30 0.18	7 11 30 0.11

Table 7

 7 Quantitative check on 5 × 5 grids with loss = 20 and g = 6

	degree C p -ε 900 frames 1800 frames 2700 frames 3600 frames
	4	7 0.08	≥ 0.53	≥ 0.78	≥ 0.90	≥ 0.95
	6	9 0.04	≥ 0.39	≥ 0.61	≥ 0.76	≥ 0.84
	8	11 0.02	≥ 0.25	≥ 0.44	≥ 0.58	≥ 0.69

For a formal definition of parameter M we refer to[START_REF] Heidarian | Analysis of a clock synchronization protocol for wireless sensor networks[END_REF].

Regular topologies have been applied to WSNs to study coverage, connectivity and energy-efficiency.

Acknowledgments The anonymous referees provided insightful comments.

As for cliques, our analysis does not loose in generality if we consider small values of C. Thus we pick C = 7, 9, 11 for the three different cases, respectively. Depending on the maximum node degree, a single time frame is composed by 5, 7, 9 TX slots plus 2 idle slots. TX slots are allocated according to the distributions depicted above. We set k 0 = 29 and we vary the parameter loss, as done for cliques. Then, we apply UPPAAL SMC to perform the following quantitative check, according to Definition 1:

Pr[time<=bound](<> exists(i:Nodes) exists(j:Nodes) (neighbor(i,j) and WSN(i).SENDING and not(csn

Again, we consider the longest run UPPAAL SMC can handle to avoid integer overflow by setting bound = 2 • 10 9 . This means that an execution module lasts


I T Banu-Demergian

C I Paduraru

G Stefanescu
email: gheorghe.stefanescu@fmi.unibuc.ro

A new representation of two-dimensional patterns and applications to interactive programming

Keywords: regular expressions, two-dimensional patterns, contours, structured interactive programming, formal methods

Regular expressions and the associated regular algebra provide a rich formalism for specifying and analysing sequential models of computation. For parallel computation, extensions to handle twodimensional patterns are often required. In this paper we present a new type of regular expressions for two-dimensional patterns based on contours and their composition. Targeted applications comes from the area of modelling, specification, analysis and verification of structured interactive programs via the associated scenario semantics.

Introduction

Regular expressions and the associated regular algebra provide a rich formalism for specifying and analysing sequential models of computation. They were originally introduced by Kleene [START_REF] Kleene | Representation of events in nerve nets and finite automata[END_REF] in connection with neural networks and finite automata -Kleene theorem states that finite automata and regular expressions are equivalent (i.e., they specify the same language). In the meantime, regular expressions became a core formalism for many other models used in computer science. In particular, they provide the backbone of a rich algebraic theory of automata, see, e.g. [START_REF] Salomaa | Two complete axiom systems for the algebra of regular events[END_REF][START_REF] Conway | Regular Algebra and Finite Machines[END_REF][START_REF] Kuich | Semirings, automata and languages[END_REF][START_REF] Kozen | A completeness theorem for Kleene algebras and the algebra of regular events[END_REF][START_REF] Bloom | Equational axioms for regular sets[END_REF][START_REF] Krob | Complete systems of β-rational identities[END_REF][START_REF] Bonsangue | A Kleene theorem for polynomial coalgebras[END_REF].

For parallel computation, enrichment of the sequential models with mechanisms for modelling process interaction are needed. We only mention a Kleene theorem to Petri nets [27, 13]: Petri nets and a class of concurrent regular expressions are equivalent. The result is based on the following procedure: [START_REF] Alur | A theory of timed automata[END_REF] decompose the behaviour to have separate components where each transaction has no more than one input and one output place; [START_REF] Asarin | Timed regular expressions[END_REF] decompose the behaviour of a component to have an independent run for each initial token; (3) use the classical Kleene theorem for these sequential runs; (4) use synchronization and renaming to force the composition of these separate projected runs to behave as a run of the initial overall system. However, as it was often noticed (see, e.g., [START_REF] Kozen | A completeness theorem for Kleene algebras and the algebra of regular events[END_REF]), renaming has bad algebraic properties and should be avoided.

A natural semantics for parallel computation is provided by a kind of twodimensional patterns/languages -for instance, messages sequence charts or scenarios fall into this category. A robust class of "regular two dimensional languages" has been identified in 1990's [START_REF] Giammarresi | Two-dimensional languages[END_REF][START_REF] Lindgren | Complexity of two-dimensional patterns[END_REF]; it may be specified by many equivalent formalisms, in particular by a 2-dimensional version of regular expressions 2RE, including intersection and renaming.

In this paper we present a new type of regular expressions for two-dimensional patterns n2RE based on contours and their composition. It avoids the use of intersection and renaming, being closer in spirit with classical 1-dimensional regular expressions. In this approach, the magic way of getting the intended language by renaming and intersection is replaced by a steady work of tiling shapes to build up the words step by step.

Our targeted applications comes from the area of modelling, specification, analysis and verification of structured interactive programs via the associated scenario semantics. Interactive computation [START_REF] Goldin | Interactive computation: The new paradigm[END_REF] is becoming more and more important in the recent years, in particular due to the advance of multicore computation. We use a model rv-IS [START_REF] Stefanescu | Interactive systems with registers and voices[END_REF] based on space-time duality. In particular, finite interactive systems [START_REF] Stefanescu | Algebra of networks: Modeling simple networks as well as complex interactive systems[END_REF] are the space-time invariant extension of finite automata in this context. Agapia programming [START_REF] Dragoi | Agapia v0. 1: A programming language for interactive systems and its typing system[END_REF] is a core interactive programming language based on this model. We use the n2RE expressions to present a relational semantics for Agapia programs; it may be seen as an extension to two dimensions of the classical relational semantics of sequential computing models [START_REF] Maddux | Relation-algebraic semantics[END_REF][START_REF] Manes | Algebraic approaches to program semantics[END_REF].

The paper is organized as follows. Section 2 presents a known approach using two sets of regular algebra operators, intersection, and renaming. Section 3 presents the new approach based on contours and Section 4 shows an application for getting a relational semantics for structured interactive programs. Related and future works and references conclude the paper.

A known approach

2.1 Finite interactive systems (FIS's) and regular expressions (2RE's) Definition 1. A finite interactive system (FIS) [START_REF] Stefanescu | Algebra of networks: Modeling simple networks as well as complex interactive systems[END_REF][START_REF] Stefanescu | Interactive systems with registers and voices[END_REF] is defined by two types of nodes: states (denoted by numbers 1, 2, ...) and classes (denoted by capital letters A, B, ...); transactions: (A, 1) -a → (B, 2), where a is a letter of the considered alphabet and A, B, 1, 2 are as above; specification of the initial/final states and classes. 2

A useful cross/tile representation may be used; is is based on showing the transitions and stating which states and classes are initial/final. An example is FIS recognizing procedure. The FIS recognizing procedure is via accepted scenarios. A scenario alternates class/state information and letters according to the FIS transitions. It is an accepting scenario if the northern border has initial states, the western border has initial classes, the eastern border has final classes, and the southern border has final states.

S1: A 2 1 B A 1 2 B a
Graphically, a scenario may be easily obtained using the crosses representing the transitions and identifying the matching classes or states of the neighbouring cells. In Fig. 1 we show a few examples of scenarios for the FIS S1 above. Notice that the recognizing procedure may be applied to non-rectangular words, as well. Definition 2. First, simple 2-dimensional regular expressions (simple 2RE's) are defined by two sets of regular operators (one for the vertical, the other for the horizontal direction) which share the additive part. Formally, they use:

1. the additive operators: 0 (for empty set) and + (for union); 2. the vertical composition operators: I v (vertical identity), ; v (vertical composition) and * v (iterated vertical composition); our preferred textual notation is: |, ; and *; 3. the horizontal composition operators: I h (horizontal identity), ; h (horizontal composition) and * h (iterated horizontal composition); our preferred textual notation is: -, > and ^. Next, 2-dimensional regular expressions (2RE's) are obtained adding intersection and renaming to simple 2RE's. Formally, they use the following additional operators 1. intersection: our preferred textual notation is /\; 2. renaming via a letter-to-letter homomorphism rho:V->V' (V and V' are the old and the new vocabulary, respectively). 2

Examples.

A few examples of 2RE expressions and typical specified words are presented in Fig.

(1) (2) (3) (4) (5)
Fig. 2. A 2RE expression for the FIS S1 for a FIS S with transitions having distinct letters the procedure is:

• take a usual regular expression Es for the state-projected nondeterministic finite automaton (NFA) of S and another one Ec for the classprojected NFA of S (these NFA's are obtained from S ignoring one dimension) • an expression for S is (Es)^/\ (Ec)* for an arbitrary FIS proceed as follows: first rename the transitions with new letters to apply the above step; then, apply the previous result; finally, use the renaming operator to rename back the new letters with their original version in the resulting expression.

For the other part, one can use the result in [START_REF] Sofronia | Undecidability results for finite interactive systems[END_REF] showing that FIS's are equivalent with tile systems, then the relation between 2RE's and tile systems. 2

Example: Let us consider the FIS S2 defined by

A 2 1 B A 1 2 B a 2 A 1 B a a
, where 1,A are initial and 2,B are final.

The procedure is the following:

1. rename the 2-nd a as c and the 3-rd a as b to get different letters for transitions; actually, this way we get the FIS S1 above; 2. get a 2RE for this new FIS; using the projected NFA's such an expression is Problems. There are a few problems with this approach, the main critics being the following:

-Intersection is a nonintuitive operator: Indeed, it is difficult to grasp what you get by intersecting two or more languages.

-The formalism is not robust under renaming: As an example, notice that the expression E3 = ( a* ; a ; a*)^/\ (a^> a > a^)*, obtained by syntactically renaming a,b,c as a into the expression E above, represents all rectangular words of a's, not only the square ones as one expects.

-Renaming is yet a still more nonintuitive operator: It's like writing in Chinese and getting an English text using a letter-to-letter morphism, losing most of the information.

The solution we propose to the above problems is the following:

-Construct a formalism for handling words of arbitrary shapes in the 2dimensional plane;

-Introduce a powerful set of composition operators for these shapes (extending vertical/horizontal compositions and their iterated versions)

In other word, the magic way of getting the intended language by renaming and intersection is to be replaced by a steady work of tiling shapes to get the words step by step.

A new approach

General 2-dimensional words

A (pointed) contour is a closed line, with a chosen starting point, on a rectangular grid Z×Z that divide the space into two disjoint regions: the internal area (which is required to be finite) and the external area. It will be represented using a sequence of letters from the set {u,d,l,r} (u stands for "up", d for "down", l for "left", and r for "right") and a placement (x, y) of the starting point. For simplicity, by default one can consider the starting point to be (0, 0).

A few examples of contours are shown in Fig. 3. A representation for C1 is l_1 u_1 l_1 d_1 l_1 u_2 r_3 d_2. The numbers after the letters are used to count repetitions. The contour starts at the chosen (black dot) point and travel clockwise. The interior area of a contour is the dashed (yellow) one. As the contour is surrounded clockwise, the area on the right is internal, while the one on the left is external. By changing the starting point, the representation is shifted circularly; for instance, C2 is represented by l_1 d_1 l_1 u_2 r_3 d_2 l_1 u_1. Two slightly more complicate contours are shown in C3 and C4 in Fig. 3. As the last example shows, one can have contours with distinct disjoint components in its internal area, connected via lines travelled forth and back in the representation. The lines travelling into the internal areas are also called tunnels, while those sitting in the external areas bridges. As one can see, the tunnels and the bridges have a lot of freedom regarding both their forms and their For a point p = (x, y) ∈ Z 2 , p k C specifies the information that C passes exactly k time through p; notice that k ≥ 0. A vertical line segment ((x, y), (x, y + 1)) is specified by its middle point l = (x, y + 0.5); the notation l k C specifies that the difference between the "up" and the "down" times C passes through this segment is k; notice that k ∈ Z may be both positive or negative. Similarly, for an horizontal line segment ((x, y), (x + 1, y)), denoted l = (x + 0.5, y), the notation l k C says that k is the difference between the "right" and the "left" times C passes through l. Finally, a unit cell with the corners {(x, y), (x + 1, y), (x + 1, y + 1), (x, y + 1)} is specified by its center point c = (x + 0.5, y + 0.5).

For a cell c = (x + 0.5, y + 0.5), the notation c k C,w specifies how c is seen in C from a western perspective. Formally, let z = max{w ∈ Z : w < x and l = (w, y + 0.5) is such that l k C is true with k = 0}; then c k C,w is true if l k C is true for the line l = (z, y + 0.5). In words, starting from the center of the cell and travelling horizontally towards the west there is a first line crossed and having a unequal up/down passings and, moreover, the difference between the "up" and the "down" passings along that line is k. The notations c k C,e , c k C,n , and c k C,s are similarly introduced for the eastern, northern, and southern directions.

A cell is seen as internal if c k C,w and k > 0. For the external property the condition is slightly different: either c k C,w and k < 0 (i.e., going horizontally towards west, the there is a first line crossed with more down than up passings) or there is no line crossed with unequal up/down passings. This additional condition is needed to ensure the internal area of a valid contour is finite; for instance, drul is not a valid contour (see below the formal definition of valid contours).

With these notations, the correctness criteria for a string to represent a valid contour are the following: a closed line C represents a valid contour if:

each cell is either internal from all directions, or external from all directions; for the internal cells, the conditions c k C,w , c k C,e , c k C,n , and c k C,s are all satisfied with k = 1. The last condition is needed to avoid overlapping by multiple surroundings of the same internal area; for instance rdlurdlu is not valid, while rdlu is. It is possible to replace the conditions here with conditions on the string itself, rather than on the lattice cells. However, such an approach is less intuitive (it is based on forbidden string configurations) and the details are quite complex; see [START_REF] Banu-Demergian | On the contour representation of twodimensional patterns[END_REF].

A general 2-dimensional word is specified by a contour and a filling of its internal area with letters from the given alphabet. In the following we will mostly ignore this additional information as most of the difficulties are posed by the handling of the contours/shapes and not by the contents of their internal areas.

General composition

A general composition operator '.' on contours may be defined as follows: given two contours, get a new contour by putting them together and identifying their starting points (the black dots). This means, one has to travel along the first contour and when he arrives back to the starting point, to travel along the next. In the string representation of the contours, the operation actually is concatenation C1 . C2 = C1 C2.

Comments: The condition to have a definite composite is to have a valid non-overlapping contour after the concatenation of the representations of the given contours (for instance, a pointed contour cannot be composed with itself). In particular, this implies that there is no constraint on the contents of the internal areas of the contours, hence the operation is straightforwardly extended to general 2-dimensional words. This is a very powerful and general composition operator, indeed.

For a graphical example, C1 . C3 in Fig. 4 shows a composition leading to a valid contour, while C2 . C3 leads to a string representation which does not represent a valid contour (it has overlapping areas).

This composition is extended to two-dimensional words as follows. For two words W1, W2, consider arbitrary contours C1, C2 representing them (having as internal areas the shapes of the words) and arbitrary positions as starting points of these contours. Then, W1 . W2 consists of all words resulting from valid compositions of such contours and placing the letters of the words W1, W2 in the corresponding positions of the resulting composites. E.g., the composite a . a contains the words a a a a a a a a , etc.

Particular composition operators

The new type of 2-dimensional regular expressions, to be defined below, put constraints on the contact elements of the composed words. These constraints acts on the following three types of elements: side borders, land corners (turning points on the contour having 3 neighbouring cells outside the word and one neighbouring cell inside), and golf corners (turning points on the contour with at least 2 neighbouring cells inside and one neighbouring cell outside). An example is shown in Fig. 5(1). The resulting restricted composition operators extend the usual vertical and horizontal composition operators used on rectangular words.

Points of interest on the words borders. Let us use the following notation (their meaning is explained right after the listing):

side borders: elements in C1={w,e,n,s}, where w stands for "west border", e for "east border", n for "north border", and s for "south border"; land corners: elements in C2={nw,ne,sw,se}, where nw stands for "northwest land corner", ne for "north-east land corner", sw for "south-west land corner", and se for "south-east land corner"; golf corners: elements in C3={nw',ne',sw',se'}, where nw' stands for "northwest golf corner", ne for "north-east golf corner", sw for "south-west golf corner", and se for "south-east golf corner".

A line l = (x, y + 0.5) is on the east border of a word f if the cell c = (x -0.5, y + 0.5) is in the internal area of f , while the cell c = (x + 0.5, y + 0.5) is in the external area of f . For the other west, north, and south directions, the definition is similar. A point p = (x, y) ∈ Z 2 is on the south-east land corner border of a word f if the cell c = (x -0.5, y + 0.5) is in the area of f , while the other 3 cells around are not in the area of f (they are in the external area of f ). For the other 3 types of land corners the definition is similar. A point p = (x, y) ∈ Z 2 is on the south-east golf corner border of a word f if the cell c = (x -0.5, y + 0.5) is not in the area of f (it is in the external area of f ), while at least 2 of the other 3 cells around are in the area of f . For the other 3 types of golf corners the definition is similar.

Glueing combinations. The constraints on glueing the borders of the words in the composite word are independently put on one or more the following combinations (x, y):

x and y are different and either they are both in {e, w}, or both in {s, n}, or both are land corners in {nw, ne, sw, se}, or both are combinations golf-land corners for the same directions.

Spelling out the resulting combinations we get the following lists:

linking side borders: L1={(w,e),(e,w),(n,s),(s,n)}; linking land corners: L2={(nw,ne),(nw,se),(nw,sw),(ne,nw),(ne,se), (ne,sw),(se,nw),(se,ne),(se,sw),(sw,nw),(sw,ne),(sw,se)}; linking golf-land corners: L3={(nw',nw),(nw,nw'),(ne',ne),(ne,ne'), (se',se),(se,se'),(sw',sw),(sw,sw')}.

The set of all combinations in L1 ∪ L2 ∪ L3 is denoted by Connect.

Constricting formulas. On each of the above eligible glueing combination (x, y) we put a constrain given by a propositional logic formula1 F ∈ P L(φ 1 , φ 2 , φ 3 , φ 4 ), i.e., a boolean formula built up starting with the following atomic formulas:

φ 1 (x, y) = "x < y", φ 2 (x, y) = "x = y", φ 3 (x, y) = "x > y", φ 4 (x, y) = "x # y".
The meaning of the connectors is the following: "<" -left is included into the right; "=" -left is equal to the right; ">" -left includes the right; "x # y" -left and right overlaps, but no one is included in the other.

For instance: f (e = w)g means "restrict the general composition of f and g such that the east border of f is identified to the west border of g"; f (e > w)gthe east border of f includes all the west border of g, but some east borders of f may still be not covered by west borders of g; etc.

We also use the notation φ 0 (x, y) = "x ! y", where "!" means empty intersection.

Actually, this is a derived formula ¬(φ 1 (x, y) ∨ φ 2 (x, y) ∨ φ 3 (x, y) ∨ φ 4 (x, y)).

Particular composition operators.

We are now in a position to introduce the particular composition operators induced by the above constricting formulas.

Definition 3. (restricted compositions)

A restriction formula φ is a boolean combination in P L(F 1 , . . . , F n ), where F i are constricting formulas involving certain eligible glueing combinations (x i , y i ) ∈ Connect. A restricted composition operation (F ) is the restriction of the general composition to composite words satisfying F . A word h ∈ f . g belongs to f (F ) g if for all glueing combinations (x i , y i ) occurring in F the contact of the x i border of f and y i border of g satisfies F i . 2

This interpretation shows the constricting formulas act on the involved glueing combinations, while for the glueing combinations (x j , y j ) not occurring in the formula no constraints are imposed, at all. Other default conventions are possible, too; for instance stating that what is not specified should not touch.

Notice that the restricted composition operations are not always associative; e.g., ((a (s=n) a) (e>w) b) (e>w) c = (a (s=n) a) (e>w) (b (e>w) c). When some parentheses are missing, we suppose a left-parentheses order applies, as in ((C1 op C2) op C3).

}; b (ne>ne') y is {(9)}; y (s#n & w#e) b is {(9), (3),(4),(5)
}. The words for y (e#w) b strictly include the set {( 6),( 6),( Examples, related to S1. The examples in Fig. 6 are related to S1, the original FIS we have considered in the beginning of the section. We first show the expressions, then include samples of typical words associated to these expressions. Combined with the constraint to have rectangular words, the final regular expression Eabc specifies the language of S1.

Observation. The formalism is robust, in particular it commutes with renaming: renaming letters either in the associated words or in the given expression leads to the same set of general 2-dimensional words.

A relational semantics for structured interactive programs

In this section we show how the introduced regular expressions can be used to get a relational semantics for structured interactive programs presented in the rv-IS formalism [START_REF] Stefanescu | Interactive systems with registers and voices[END_REF][START_REF] Dragoi | Agapia v0. 1: A programming language for interactive systems and its typing system[END_REF]. The operational semantics of structured programs is given in terms of scenarios. In Fig. 7(a) we illustrate an rv-IS scenario for deciding whether the number 6 is a perfect number (i.e., it is equal to the sum of its proper divisors); in (b) it is a scenario for testing if 7 is a perfect number.

In this representation, the actions to be performed are placed in the square cells. One example is the cell with the identifier P placed in the 2nd row and the 1st column in (a). On the top and the bottom of this cell there is the same state variable x with its concrete values 3 and 2. Actually, the effect of P on the memory state is to decrease x by 1. With respect to the interaction part, this cell has no variables for its left border (a fact specified by the '.' inserted there) and has a variable tx at its right border. The effect of P on the interaction part is to set in tx the input value 3 of x in order to be used in other columns/processes.

In Fig. 8 we present relational specifications for the cells used in Fig. 7. All these cells have functional behaviour, hence the corresponding relations may be A final line contains terminating modules that rearrange some interfaces, keeping only the relevant result z.

Dataflow and mixed imperative-dataflow programming styles.

The above model corresponds to the construction of scenarios by rows and it exhibits a (parallel) imperative programming style, illustrated in Fig. 9 In this implementation, the processes corresponding to the 2nd and the 3rd columns act as "services": they receive initialization data (here the value of n), then a stream of data to act individually on each one according to the service function (for the 2nd process this function is the check for divisibility, while for the 3rd is subtraction), and finally a termination token (represented here by -1).

Finally, we present a last model, illustrated in Fig. 9(c), which mixes the imperative and dataflow styles

((IP (e=w) ID) (e=w) IM) (s=n) [(((P (e=w) D) *(s=n)) (s=n) (TP (e=w) TD)) (e=w) ((M *(s=n)) (s=n) TM)]
In this version the construction of the scenarios is as follows. It starts by constructing the 1st line of the scenarios. Then, the remaining parts of the first two columns are generating in the same way as with the initial model (that is, by an imperative style). Moreover, the same is done separately for the remaining part of the third column. Finally, these parts are composed horizontally (following a dataflow style).

Related and future works

Related work. Regular expressions are introduced in the seminal paper by Kleene [START_REF] Kleene | Representation of events in nerve nets and finite automata[END_REF] on the representation of events in neural nets and automata; it was published in the early 1950s. Kleene theorem (i.e., the equivalence between finite automata and appropriate regular expressions) was extended to cover other computing models of interest and is a basis for the development of algebraic theories for those models.

The algebraic theory of finite automata is based on semirings enriched with an axiomatic iteration operator; often the term Kleene algebra is used in this context. It was steadily developed since 1960s till now, including deep results as Krob's solution [START_REF] Krob | Complete systems of β-rational identities[END_REF] for two deep conjectures of Conway [START_REF] Conway | Regular Algebra and Finite Machines[END_REF]. We notice the interest in getting complete equational axiomatizations; see, e.g., [START_REF] Salomaa | Two complete axiom systems for the algebra of regular events[END_REF][START_REF] Kozen | A completeness theorem for Kleene algebras and the algebra of regular events[END_REF][START_REF] Bloom | Equational axioms for regular sets[END_REF][START_REF] Krob | Complete systems of β-rational identities[END_REF][START_REF] Bonsangue | A Kleene theorem for polynomial coalgebras[END_REF]. A few books recording the results are [START_REF] Conway | Regular Algebra and Finite Machines[END_REF] and [START_REF] Kuich | Semirings, automata and languages[END_REF].

When (matrices over) semirings are replaced by more general algebraic structures as symmetric (strict) monoidal categories, the iteration operators may have different expressive powers and axiomatisations. Trace monoidal categories [START_REF] Stefanescu | Feedback Theories (A Calculus for Isomorphism Classes of Flowchart Schemes)[END_REF][START_REF] Cazanescu | Towards a new algebraic foundation of flowchart scheme theory[END_REF][START_REF] Joyal | Traced monoidal categories[END_REF][START_REF] Stefanescu | Network algebra[END_REF] are now recognized as a powerful formalism for iterative processes, with wider applications than Kleene algebras; in particular they apply to circuits, dataflow computation, quantum computation, etc. Translations between various formalisms using axiomatic iteration operators may be found in [START_REF] Stefanescu | On flowchart theories: Part I. The deterministic case[END_REF][START_REF] Stefanescu | On flowchart theories: Part II. The nondeterministic case[END_REF][START_REF] Bloom | Iteration Theories: The Equational Logic of Iterative Processes[END_REF][START_REF] Cazanescu | Feedback, iteration and repetition[END_REF][START_REF] Stefanescu | Network algebra[END_REF]. Axiomatic iteration operators are also present in process calculi; a few papers are [START_REF] Milner | Flowgraphs and flow algebras[END_REF][START_REF] Bergstra | Process algebra with iteration[END_REF][START_REF] Milner | Action calculi V : Reflexive molecular forms[END_REF].

Parallel computation often requires the enrichment of the sequential computation models with mechanisms for modelling process interaction. We mention three examples of extensions of Kleene theorem into such a context: Kleene theorems for tile systems [START_REF] Giammarresi | Two-dimensional languages[END_REF], for Petri nets [27, 13], and for timed automata [START_REF] Alur | A theory of timed automata[END_REF][START_REF] Asarin | Timed regular expressions[END_REF]. In all these contexts, the Kleene theorem is based on the following procedure: (1) decompose/project the behaviour to have separate sequential runs; (2) use the classical Kleene theorem for these sequential runs; (3) use synchronization and renaming to force the composition of these separate projected runs to behave as the initial overall system. It was noticed (see, e.g., [START_REF] Kozen | A completeness theorem for Kleene algebras and the algebra of regular events[END_REF]) that renaming has bad algebraic properties and should be avoided.

The study of two dimensional languages has started in 1960's; see [START_REF] Giammarresi | Two-dimensional languages[END_REF][START_REF] Lindgren | Complexity of two-dimensional patterns[END_REF]. In 1990's, a robust class of "regular two dimensional languages" has been identified; it may be specified either by tile systems, or by a type of cellular automata, or by a class of monadic second-order formulas, etc. Unfortunately, the class is quite complex -for instance, emptiness property is not decidable, see [START_REF] Latteux | Context-sensitive string languages and recognizable picture languages[END_REF].

Interactive computation [START_REF] Goldin | Interactive computation: The new paradigm[END_REF] is becoming more and more important in the recent years, in particular due to the advance of multicore computation. We use a model rv-IS [START_REF] Stefanescu | Interactive systems with registers and voices[END_REF] based on space-time duality. In particular, finite interactive systems [START_REF] Stefanescu | Algebra of networks: Modeling simple networks as well as complex interactive systems[END_REF] are the space-time invariant extension of finite automata in this context. A Kleene theorem for finite interactive systems follows directly from their equivalence with tile systems [START_REF] Sofronia | Undecidability results for finite interactive systems[END_REF]. Agapia programming [START_REF] Dragoi | Agapia v0. 1: A programming language for interactive systems and its typing system[END_REF] is a core interactive programming language based on this model. The relational semantics described in the present paper for Agapia programs may be seen as an extension to 2 dimensions of the classical relational semantics of sequential computing models [START_REF] Maddux | Relation-algebraic semantics[END_REF][START_REF] Manes | Algebraic approaches to program semantics[END_REF].

Future work. There are many directions to continue the research presented in this paper. We are particularly interested to develop the theoretical basis of the model (e.g., to prove a Kleene theorem for finite interactive systems2 ; to look for an associated algebraic theory; etc.) and to provide a software tool for manipulating n2RE's. Among the possible applications we mention:

the study of massively parallel, interactive OO-programs (semantics, specification, verification, etc.), in particular the programs written in the structured interactive programming language Agapia; applications to image processing, in particular learning n2RE as a image recognition procedure; modelling discrete physical or biological systems.

with 1 ,Fig. 1 .

 11 Fig. 1. FIS recognizing procedure

2 .

 2 They are related to the following expression E = ( b* ; a ; c*)^/\ (c^> a > b^)*. In Fig. 2.(1)-(4), typical words generated by the following expressions are presented: b* ; a ; c*; ( b* ; a ; c*)^; c^> a > b^; and (c^> a > b^)*. It can be proved that the intersection ( b* ; a ; c*)^/\ (c^> a > b^)* has only square words with a on the diagonal, b on the top right area and c on the bottom left area, see Fig. 2.(5). The first part of the expression constrains the column patterns, while the second the rows. Intersection does the magic action of selecting only the square 2-dimensional words.

  E1 = ( b* ; a ; c*)^/\ (c^> a > b^)* 3. rename back to get an expression for S2 E2 = rho [( b* ; a ; c*)^/\ (c^> a > b^)*] with rho mapping a,b,c into a,a,a, respectively.

Fig. 3 .

 3 Fig. 3. Contours

?Fig. 4 .

 4 Fig. 4. Contours composition

Fig. 5 .

 5 Fig. 5. Particular composition operators

  }; one can use the expression y (e#w & ne!nw & se!sw) b to exclude two words from y (e#w) b and to get precisely the set {(

Definition 4 . 2 Definition 5 .

 425 (iterated composition operators) The iterated composition operators are denoted by * (F ), for a restriction formula F . The set of expressions obtained using the operators defined so far are denoted by n2RE's; they represent our new type of regular expressions for two-dimensional patterns/words. 2

Fig. 6 .Fig. 7 .

 67 Fig.6. A n2RE expression for the FIS S1

  (a).

Fig. 9 .

 9 Fig. 9. Programming strategies

P L(Atom) denotes the set of propositional logic formulas built up with atomic formulas in Atom. For typing reasons, the boolean operations "not", "and", and "or" are denoted by "!", "&", and "|", respectively.

Recently, the first and the last authors presented a characterization theorem for FIS languages in[START_REF] Banu-Demergian | Representation of scenarios in finite interactive systems[END_REF]. Their result shows that a slightly extended class of n2RE expressions and a mechanism for solving recursive equations suffice to represent FIS languages.

Acknowledgements. The research reported in this paper was partially supported by Deploy Project, an FP7 Integrated Project supported by European Commission (Grant No. 214158). We thank the anonymous reviewers for their suggestions for improving the presentation of the results.

specified as partial functions in the following way:

Cell(west,north) = (east,south), if Condition.

Example -imperative programming style

We start with the following expression specifying scenarios checking if a number n is perfect

In this model we can imagine that we have three processes: one generates all the numbers in the set {n/2, . . . , 1} (with module P), one checks if a number is a divisor of n (module D) and the last one updates a variable z (module M). Modules IP, ID and IM are used for initializations and TP, TD and TM for termination. At the end of the program, if the variable z is 0, then the number n is perfect.

In order to show how we can construct a scenario using the expression above let us consider a concrete example for n = 6. The scenario for n = 6 is presented in Fig. 7 (a).

IP((.),(x)) = ((tx'),(x')) with tx' = x and x' = x/2; defined if x ≥ 2 ID((tx),(.)) = ((tx'),(y')) with tx' = tx and y' = tx IM((tx),(.)) = ((.),(z')) with z' = tx P((.),(x)) = ((tx'),(x')) with tx' = x and x' = x-1; defined if x > 0 D((tx),(y)) = ((tx'),(y')) with y' = y and tx' = if(y%tx=0) then tx else 0 M((tx),(z)) = ((.),(z')) with z' = z-tx TP((.),(x)) = ((tx'),(.)) with tx' = -1; defined if x = 0 TD((tx),(y)) = ((tx'),(.)) with tx' = -1 TM((tx),(z)) = ((.),(z')) with z' = z Fig. 8. Relational semantic specifications for the cells used in Fig. 7 In the first line of the scenario we initialize the processes with the needed informations: module IP is reading the value n = 6 and provides the first process with x = 3 and declare a temporal variant of n, namely tn = 6, that will be used by modules ID and IM for the other initializations; modules ID and IM use the temporal variable tn for initializing the other two processes with the initial value of n, namely y = 6, z = 6, respectively.

In the next step, module P produces a temporal data tx = 3 (tx is equal with the data x of the first process) and decrease x. Module D verifies if tx is a divisor of y and, if no, it resets the value of tx to 0. Finally, module M decreases the value of z by tx. Notice that module M decreases the value of z only with the divisors of the initial variable n. We continue this steps until the variable x becomes 0.