Claudio De Persis
email: c.de.persis@rug.nl.

Romain Postoyan
email: romain.postoyan@univ-lorraine.fr.

Lyapunov design of event-based controllers for the rendez-vous of coupled systems

The objective is to present a new type of triggering conditions together with new proof concepts for the eventbased coordination of multi-agents. As a first step, we focus on the rendez-vous of two identical systems modeled as double integrators with additional damping in the velocity dynamics. The reduced number of agents in the system allows us to illustrate the design of the new triggering rule while avoiding technical issues that arise in the full multi-agent system. We first propose an event-triggering policy which relies on a designed clock variable whose dynamics depend on the relative position of the agents. We then explain how to derive self-triggered and time-triggered rules. The overall system is modeled as a hybrid system in each case, and an invariance principle is used to conclude about the rendez-vous. Simulation results are provided to illustrate the efficiency of the proposed controllers.

I. INTRODUCTION

Event-based sampling paradigms have recently been developed to implement controllers in order to provide alternatives to the traditional periodic sampling. This line of research is motivated by the rise of networked control systems and embedded systems which are subject to communication and/or computation constraints and for which periodic sampling may not be suitable. Indeed, it seems more natural in this context to use the CPU and the communication channel only when it is needed, in other words at some time instants which depend on the system state, rather than periodically. Following this idea, event-triggered control has been introduced in [START_REF] Arzén | A simple event-based PID controller[END_REF], [START_REF] Aström | Comparison of periodic and event based sampling for first-order stochastic systems[END_REF]. It consists in closing the feedback loop whenever a designed state-dependent criterion is satisfied. Many works have then proposed event-triggered controllers mostly to stabilize (nonlinear) systems, see [START_REF] Donkers | Output-based event-triggered control with guaranteed L∞-gain and improved and decentralized event-triggering[END_REF], [START_REF] Heemels | Analysis of event-driven controllers for linear systems[END_REF], [START_REF] Miskowicz | Send-on-delta concept: An event-based data reporting strategy[END_REF], [START_REF] Postoyan | A unifying Lyapunovbased framework for the event-triggered control of nonlinear systems[END_REF], [START_REF] Tabuada | Event-triggered real-time scheduling of stabilizing control tasks[END_REF], [START_REF] Wang | On event design in event-triggered feedback systems[END_REF] and the references therein, where it is shown that event-triggered control may significantly reduce the usage of the network compared to periodic sampling. A potential drawback of event-triggered control is that it requires to continuously evaluate the triggering law, which may be difficult to realize in practice. To overcome this issue, self-triggered control strategies have been developed to decide the next time instant at which the loop must be closed based on the last received measurement, see e.g. [START_REF] Anta | To sample or not to sample: self-triggered control for nonlinear systems[END_REF], [START_REF] Anta | Exploiting isochrony in self-triggered control[END_REF], [START_REF] Velasco | The self triggered task model for real-time control systems[END_REF], [START_REF] Wang | Self-triggered feedback control systems with finite-gain L 2 stability[END_REF]. This approach usually leads to more transmissions than event-triggered control, but necessitates less computation resources. Another alternative to eventtriggered control is periodic event-triggered control [START_REF] Heemels | Periodic eventtriggered control for linear systems[END_REF], [START_REF] Postoyan | Periodic event-triggered control for nonlinear systems[END_REF], where the triggering condition is periodically evaluated; we will not investigate it in this paper.

These event-based sampling approaches are particularly relevant in the context of multi-agent systems, for which the communication and the computation capacities are often (strongly) limited. On the other hand, multi-agent systems exhibit the following features which are absent in the works cited above:

(i) Weak Lyapunov function. The stability analysis usually relies on a weak Lyapunov function, in the sense that the derivative of the Lyapunov function along the system solution is non-positive, as opposed to strong Lyapunov functions for which it is strictly negative (outside the attractor). This is an important difference with the vast majority of stabilizing event-triggered control techniques, which require the knowledge of strong Lyapunov function; the only exception is [START_REF] Postoyan | Nonlinear event-triggered tracking control of a mobile robot: design, analysis and experimental results[END_REF] to the best of our knowledge. This point induces non-trivial technical difficulties, which makes existing event-triggering results not applicable for the eventbased control of multi-agent systems.

(ii) Distributed control. Multi-agent systems are generally distributed as each agent has only access to its own state and the state of its neighbours (and not to the state of the overall system). Hence, it is necessary to design distributed triggering conditions which only depend on the local variables.

Various results have been proposed to address these challenges, see e.g. [START_REF] Dimarogonas | Distributed event-triggered control for multi-agent systems[END_REF], [START_REF] Nowzari | Self-triggered coordination of robotic networks for optimal deployment[END_REF], [START_REF] De Persis | Self-triggered coordination with ternary controllers[END_REF], [START_REF] Persis | On self-triggered synchronization of linear systems[END_REF], [START_REF] De Persis | Self-triggered rendezvous of gossiping second-order agents[END_REF], [START_REF] Seyboth | Event-based broadcasting for multi-agent average consensus[END_REF]. In this paper, we focus on the rendez-vous of agents modeled as double integrators with a damping term in the velocity dynamics. By rendez-vous, we mean that the agent positions must asymptotically converge towards each other. We choose to focus on the particular case where the system is composed of two agents in order to concentrate on (i). Indeed, the aim of this paper is to present a new type of triggering conditions together with new proof concepts to address (i).

The presented approach is extended to systems with an arbitrary finite number of agents in our forthcoming work [START_REF] De Persis | A Lyapunov redesign of coordination algorithms for cyberphysical systems[END_REF], and we think that it can be used to address other eventbased coordination problems, as we will show in future work. We first focus on event-triggered control and we present a triggering rule which relies on a clock whose dynamics depends on the relative position of the agents. At each triggering instant, the clock is reset to a fixed constant b > 0, it then decreases according to some state-dependent dynamics until it reaches a ∈ [0, b), where a and b are designed by the agent. This technique is easy to construct and facilitates the analysis of the existence of a (uniform) amount of time between two successive triggering instants. Indeed, it suffices to verify that a boundedness property holds (which directly follows from the Lyapunov analysis) to ensure it. The existence of such a time is crucial in practice in order to respect the hardware which prevents the occurrence of arbitrarily close-in-time events. We then explain how to derive self-triggered and time-triggered rules. The idea of adding a variable to define the triggering condition is borrowed from [START_REF] Postoyan | A unifying Lyapunovbased framework for the event-triggered control of nonlinear systems[END_REF] and the proposed techniques are inspired by [START_REF] Carnevale | A Lyapunov proof of an improved maximum allowable transfer interval for networked control systems[END_REF], [START_REF] Postoyan | Event-triggered and self-triggered stabilization of networked control systems[END_REF]. The overall system is modeled as a hybrid system using the formalism of [START_REF] Goebel | Hybrid dynamical systems[END_REF]. The analysis is based on a hybrid Lyapunov function which is shown to be weak. An invariance principle from [START_REF] Sanfelice | Invariance principles for hybrid systems with connections to detectability and asymptotic stability[END_REF] is then applied to conclude about the desired rendez-vous.

The main novelty with respect to the existing literature on event-based control of distributed coordinated systems is that the triggering rule is designed to compensate for samplinginduced perturbative terms that appear in the Lyapunov analysis of the system. In that regard, the design is more systematic than in previously proposed approaches. The other added value of our contribution lies in the use of a hybrid invariance principle that allows us to infer the convergence result in a straightforward way. We believe that these two features (Lyapunov-based event-triggering function design and hybrid-invariance-principle-based analysis) can lead to a systematic analysis and design of event-based coordination algorithms. We focus here on the simplest example of coordination system with two agents to better highlight the two features mentioned above and to avoid technical issues that would divert the attention from the main focus of the contribution. The extension to the case of a general number of agents and the related technical details are addressed in [START_REF] De Persis | A Lyapunov redesign of coordination algorithms for cyberphysical systems[END_REF].

The paper is organized as follows. Preliminaries on hybrid systems are recalled in Section II and the problem is stated in Section III. Event-triggered control is addressed in Section IV and we then explain respectively in Sections V and VI how to derive self-triggered and time-triggered rules. In Section VII, simulation results are presented and Section VIII concludes the paper.

II. PRELIMINARIES Let R = (-∞, ∞), R ≥0 = [0, ∞), Z ≥0 = {0, 1, 2, . . .},
and Z >0 = {1, 2, . . .}. For (x, y) ∈ R n+m , (x, y) stands for [x T , y T ] T . Let f : R n → R and r ∈ R, we denote by f -1 (r) the set {x ∈ R n : f (x) = r}. A function γ : R ≥0 → R ≥0 is of class K if it is continuous, zero at zero and strictly increasing and it is of class K ∞ if in addition it is unbounded.

We will study hybrid systems of the form below, using the formalism of [START_REF] Goebel | Hybrid dynamical systems[END_REF],

ẋ = F (x) for x ∈ C, x + = G(x) for x ∈ D, (1)
where x ∈ R n is the state, F is the flow map, G is the jump map, C is the flow set and D is the jump set. We assume that C and D are closed subsets of R n and that F and G are continuous. These conditions ensure that system (1) is well-posed, see Chapter 6 in [START_REF] Goebel | Hybrid dynamical systems[END_REF]. We recall some definitions related to [START_REF] Goebel | Hybrid dynamical systems[END_REF]

. A subset E ⊂ R ≥0 × Z ≥0 is a hybrid time domain if for all (T, K) ∈ E, E ∩ ([0, T ] × {0, . . . , K}) = k∈{0,1,...,K-1} ([t k , t k+1 ], k) for some finite sequence of times 0 = t 0 ≤ t 1 ≤ . . . ≤ t K . A function φ : E → R nx is a hybrid arc if E is a hybrid time domain and if for each k ∈ Z ≥0 , t → φ(t, k) is locally absolutely continuous on I k = {t : (t, k) ∈ E}. The hybrid arc φ : dom φ → R nx is a solution to (1) if: (i) φ(0, 0) ∈ C ∪ D; (ii) for any k ∈ Z ≥0 , φ(t, k) ∈ C and d dt φ(t, k) = F (φ(t, k))
for almost all t ∈ I k , where I k = {t : (t, k) ∈ dom φ}; (iii) for every (t, k) ∈ dom φ such that (t, k + 1) ∈ dom φ, φ(t, k) ∈ D and φ(t, k + 1) = G(φ(t, k)). A solution φ to (1) is:

• nontrivial if its domain contains at least two points;

• maximal if it cannot be extended;

• complete if dom φ is unbounded;

• precompact if it is complete and the closure of its range is compact, where the range of φ is rge φ := {y ∈ R n : ∃(t, k) ∈ dom φ such that y = φ(t, k)}. We will use the definition below. Definition 1: The solutions to (1) have a uniform semiglobal dwell-time if for any ∆ ≥ 0, there exists τ (∆) > 0 such that for any solution φ to (1) with |φ(0, 0)| ≤ ∆, sup I k -inf I k ≥ τ (∆) for any k ∈ Z >0 , where I k = {t : (t, k) ∈ dom φ}. We say that the solutions to (1) have a uniform global dwell-time if there exists τ > 0 such that sup I k -inf I k ≥ τ for any k ∈ Z >0 and any solution.

We recall the following invariance definition, see Definition 6.19 in [START_REF] Goebel | Hybrid dynamical systems[END_REF]. Definition 2: A set S ⊂ R nx is weakly invariant for system (1) if it is:

• weakly forward invariant, i.e. for any ξ ∈ S there exists at least one complete solution φ with initial condition ξ such that rge φ ⊂ S; • weakly backward invariant, i.e. for any ξ ∈ S and τ > 0, there exists at least one solution φ such that for some

(t * , k * ) ∈ dom φ, t * + k * ≥ τ , it is the case that φ(t * , k * ) = ξ and φ(t, k) ∈ S for all (t, k) ∈ dom φ with t + k ≤ t * + k * . Finally, we say that a solution φ approaches the set S ⊂ R nx ([26]) if for any ǫ > 0 there exists (t * , k * ) ∈ dom φ such that for all (t, k) ∈ dom φ with t + k ≥ t * + k * , φ(t, k) ∈ S + ǫB, where B is the unit ball of R n .

III. PROBLEM STATEMENT

The objective is to construct distributed controllers to ensure the rendez-vous of two identical agents with limited communication and/or computation capacities. The dynamics of each agent is given by, for i ∈ {1, 2},

ṗi = v i vi = -v i + u i (2)
where

p i ∈ R is the position, v i ∈ R is the velocity, u i ∈ R
is the control input. This dynamics corresponds to agents modeled as double integrators with the addition of a damping term possibly due to friction. In continuous-time, the control input u i is defined as, like in [START_REF] Arcak | Passivity as a design tool for group coordination[END_REF],

u i = ψ(z i ) (3)
where

z i = p j -p i , j ∈ {1, 2}\{i} (4)
is the relative position of agent i with respect to agent j and we similarly call v j -v i the relative velocity. The function ψ : R → R is designed and it is required to be continuously differentiable, nondecreasing and odd, that implies that (x -y)(ψ(x) -ψ(y)) ≥ 0 and ψ(-x) = -ψ(x) for x, y ∈ R. According to [START_REF] Arcak | Passivity as a design tool for group coordination[END_REF], the controllers (3) guarantee that the positions p i , i ∈ {1, 2}, asymptotically converge towards each other, which means that the rendez-vous is achieved.

In this paper, we take into account the resources limitations of the agents in terms of communication and/or computation. Hence, we envision a setting where the agents only receive measurements from their neighbour and/or update their control input at some given time instants t k , k ∈ Z ≥0 , to be determined. The control input u i in (3) becomes, for i ∈ {1, 2},

u i = ψ(ẑ i ) (5)
where ẑi is a sampled version of z i , which is locally maintained by agent i. The variable z i is held constant between two successive updates, i.e.

żi = 0, (6)
and is reset to the actual values z i at the update time instant, which leads to the jump equation

ẑ+ i = z i . ( 7
)
Our goal is to define the sequence t k , k ∈ Z ≥0 , which we term as events, in order to save resources while still ensuring the rendez-vous. We present solutions for the three scenarios listed below:

• Event-triggered control: the agents know their relative position at any time instant and the control input is only updated whenever a certain triggering condition is satisfied (see e.g. [START_REF] Dimarogonas | Distributed event-triggered control for multi-agent systems[END_REF], [START_REF] Rabi | Optimal stopping for event-triggered sensing and actuation[END_REF], [START_REF] Seyboth | Event-based broadcasting for multi-agent average consensus[END_REF]). This scenario is relevant to reduce the actuators wear as well as the actuators energy consumption by limiting the number of control input updates. It requires that the agents are equipped with local sensors which measure the relative positions with their neighbour at a high frequency or that the agents communicate with their neighbour via a high-bandwidth communication channel. In that way, we can make the approximation that the agents continuously have access to their neighbour relative position.

• Self-triggered control: the agents know their relative position and velocity and update their control input only at t k , k ∈ Z ≥0 (see [START_REF] Dimarogonas | Distributed event-triggered control for multi-agent systems[END_REF], [START_REF] De Persis | Self-triggered coordination with ternary controllers[END_REF], [START_REF] De Persis | Self-triggered rendezvous of gossiping second-order agents[END_REF]). The time instant t k+1 , k ∈ Z ≥0 , is predetermined by the values of p 2 -p 1 and v 2 -v 1 at t k . This scheme reduces both the usage of the CPU and of the agents sensors or of the communication channel. This paradigm neither requires the continuous measurement of the neighbours relative position nor the continuous evaluation of a triggering condition.

• Time-triggered control: the setup is the same as for the item above, except that the sequence t k , k ∈ Z ≥0 , is periodic (and not state-dependent). For related works, see [START_REF] Zhang | Consensus of data-sampled multi-agent systems with random communication delay and packet loss[END_REF] for example.

The proposed strategies ensure the existence of a strictly positive amount of time between two successive event time instants. This property is crucial as it prevents arbitrarily close-in-time events which would exceed the hardware capacities and render the proposed hybrid controllers not realizable.

IV. EVENT-TRIGGERED CONTROL

A. Main result

To define the events, we introduce a variable φ ∈ R, which we call a clock variable. The idea is to reset φ to b > 0 after each event and to trigger the next one when φ becomes equal to a ∈ [0, b). The constants a and b are designed parameters and we explain how to tune these below. Between two successive events, φ is given by the solution to the ordinary differential equation below

φ = -1 σ 1 + φ 2 (∇ψ(z)) 2 , ( 8
)
where σ is any constant in (0, 1 2 ) and we recall that

z = p 2 -p 1 (note that (∇ψ(p 2 -p 1 )) 2 = (∇ψ(p 1 -p 2 ))
2 as ψ is odd). We notice that φ strictly decreases between two successive events in view of [START_REF] Donkers | Output-based event-triggered control with guaranteed L∞-gain and improved and decentralized event-triggering[END_REF]. The clock φ can be locally implemented on any (or both) of the agents provided continuous measurements of z are available. This type of triggering condition is inspired by the work in [START_REF] Carnevale | A Lyapunov proof of an improved maximum allowable transfer interval for networked control systems[END_REF] where the stabilization of nonlinear sampled-data systems is investigated, in which case the dynamics of φ only depends on φ and on some constants which leads to a periodic rule. This technique has then been extended to event-triggered control in [START_REF] Postoyan | Event-triggered and self-triggered stabilization of networked control systems[END_REF] by allowing the φ-dynamics to depend on the system state. In this paper, we show that this approach can be particularly useful to address event-based coordination control problems. We see that the inter-event time depends on the choice of the constants a and b. Taking a small and b large may help enlarging the inter-event time, at the price of a degraded speed of convergence as the evolution of the velocities depend on the sampled control input, see for an illustration the simulation results in Section VII.

We model the overall system using the hybrid formalism of [START_REF] Goebel | Hybrid dynamical systems[END_REF] for which a jump describes a control update

ṗ1 = v 1 v1 = -v 1 + ψ(ẑ) ṗ2 = v 2 v2 = -v 2 + ψ(-ẑ) = -v 2 -ψ(ẑ) ż = 0 φ = -1 σ 1 + φ 2 (∇ψ(p 2 -p 1 )) 2                  φ ∈ [a, b], p + 1 = p 1 v + 1 = v 1 p + 2 = p 2 v + 2 = v 2 ẑ+ = p 2 -p 1 φ + = b                φ = a. (9)
We have used the fact that ψ is odd to obtain the right handside of v2 in [START_REF] Goebel | Hybrid dynamical systems[END_REF]. The proposed event-triggered controllers ensure the rendez-vous of system (9) as formalized by the theorem below whose proof is given in the next subsection.

Theorem 1: Consider system (9). The solutions have a uniform semiglobal dwell-time and the maximal solutions are precompact and approach the set

{(p 1 , v 1 , p 2 , v 2 , ẑ, φ) : p 1 = p 2 , v 1 = v 2 = ẑ = 0 and φ ∈ [a, b]}.

B. Proof of Theorem 1 1) Change of coordinates:

We are interested in the convergence of p 2 -p 1 towards the origin, we therefore use the variable z = p 2 -p 1 . System (9) becomes in the coordinates

(p 1 , z, ẑ, v 1 , v 2 , φ) ṗ1 = v 1 ż = v 2 -v 1 ż = 0 v1 = -v 1 + ψ(ẑ) v2 = -v 2 -ψ(ẑ) φ = -1 σ 1 + φ 2 (∇ψ(z)) 2                  φ ∈ [a, b] p + 1 = p 1 z + = z ẑ+ = z v + 1 = v 1 v + 2 = v 2 φ + = b                φ = a.
(10) For the sake of convenience, we write system (10) as q = f (q) for q ∈ C, q + = g(q) for q ∈ D, (11) where q = (p 1 , z, ẑ, v 1 , v 2 , φ) and

C = q : φ ∈ [a, b] , D = q : φ = a . (12)
It can be noted that f and g are continuous and that C and D are closed, which implies that system (11), ( 12) is well-posed according to Chapter 6 in [START_REF] Goebel | Hybrid dynamical systems[END_REF].

2) Maximal solutions are complete: We first investigate the completeness of the maximal solutions to [START_REF] Heemels | Analysis of event-driven controllers for linear systems[END_REF], [START_REF] Khalil | Nonlinear systems[END_REF]. We define

U (q) := U phys (q) + U cyber (q) ∀q ∈ C ∪ D, (13)
where U phys (q

) := 1 2 (v 2 1 + v 2 2 ) + z 0 ψ(s)
ds is an energy-like function which takes into account the physical component of the system and U cyber (q) := 12 φ ψ(ẑ) -ψ(z) 2 is a term which takes into account the cyberphysical nature of the system. Let q ∈ D, in view of [START_REF] Heemels | Periodic eventtriggered control for linear systems[END_REF],

U (g(q)) = 1 2 (v 2 1 + v 2 2 ) + z 0 ψ(s) ds + 1 2 b(ψ(z) -ψ(z)) ≤ U (g(q)).
(14) Let q ∈ C. The function U is differentiable since ψ is assumed to be continuously differentiable. Hence it holds that, according to [START_REF] Heemels | Periodic eventtriggered control for linear systems[END_REF] and after some direct calculations,

∇U (q), f (q) = -v 2 1 -v 2 2 + (v 1 -v 2 ) ψ(ẑ) -ψ(z) -1 2 1 σ 1 + φ 2 (∇ψ(z)) 2 ψ(ẑ) -ψ(z) 2 -φ ψ(ẑ) -ψ(z) ∇ψ(z)(v 2 -v 1 ). (15)
We introduce e := ψ(ẑ) -ψ(z) and rewrite the equality above as

∇U (q), f (q) = -v 2 1 -v 2 2 + (v 1 -v 2 )e -1 2 1 σ 1 + φ 2 (∇ψ(z)) 2 e 2 -φe∇ψ(z)(v 2 -v 1 ). (16)
We use the bounds below, which follow from the facts that xy ≤ 1 2η x 2 + η 2 y 2 and (x-y) 2 ≤ 2(x 2 +y 2 ) for any x, y ∈ R and η > 0,

(v 1 -v 2 )e ≤ σ 2 (v 1 -v 2 ) 2 + 1 2σ e 2 ≤ σ(v 2 1 + v 2 2 ) + 1 2σ e 2 -φe∇ψ(z)(v 2 -v 1 ) ≤ σ 2 (v 2 -v 1 ) 2 + 1 2σ φ 2 e 2 (∇ψ(z)) 2 ≤ σ(v 2 1 + v 2 2 ) + 1 2σ φ 2 e 2 (∇ψ(z)) 2 , (17)
where σ comes from [START_REF] Heemels | Periodic eventtriggered control for linear systems[END_REF], to derive that

∇U (q), f (q) ≤ -v 2 1 -v 2 2 + σ(v 2 1 + v 2 2 ) + 1 2σ e 2 -1 2 1 σ 1 + φ 2 (∇ψ(z)) 2 e 2 +σ(v 2 1 + v 2 2 ) + 1 2σ φ 2 e 2 (∇ψ(z)) 2 = (-1 + 2σ)(v 2 1 + v 2 2 ). (18
) Let ξ be a maximal solution to [START_REF] Heemels | Analysis of event-driven controllers for linear systems[END_REF], [START_REF] Khalil | Nonlinear systems[END_REF]. We want to prove that ξ is complete. We first need to ensure that ξ is a nontrivial solution. We use Proposition 6.10 in [START_REF] Goebel | Hybrid dynamical systems[END_REF] for that purpose, in particular we aim to prove that for any q ∈ C\D, f (q) belongs to the tangent cone 1 of C at q. Let q ∈ C\D. Consider the case where φ ∈ (a, b), the tangent cone to C at q is R 6 and the desired result holds. Let φ = b, the aforementioned tangent cone is R 5 × (-∞, 0]. In view of the dynamics of φ on flows in [START_REF] Heemels | Periodic eventtriggered control for linear systems[END_REF], we deduce that f (q) ∈ R 5 × (-∞, 0]. Consequently, ξ is not a trivial solution to [START_REF] Heemels | Analysis of event-driven controllers for linear systems[END_REF], [START_REF] Khalil | Nonlinear systems[END_REF] according to Proposition 6.10 in [START_REF] Goebel | Hybrid dynamical systems[END_REF].

The solution ξ cannot leave the flow and the jump sets as g(D) ⊂ C in view of [START_REF] Khalil | Nonlinear systems[END_REF]. Hence, the only potential obstacle to the completeness of ξ is if it explodes in finite time, according to Proposition 6.10 in [START_REF] Goebel | Hybrid dynamical systems[END_REF]. Consider the definition of U in [START_REF] Miskowicz | Send-on-delta concept: An event-based data reporting strategy[END_REF]. The facts that ψ is monotone and odd and that φ ∈ [a, b] ensure that there exist α U , α U ∈ K ∞ such that, for any q ∈ C ∪ D,

α U (|(z, v 1 , v 2 )|) ≤ U (q) ≤ α U (|(z, v 1 , v 2 , ψ(z), ψ(ẑ))|).
(19) On the other hand, we derive from ( 14) and ( 18) that

U (ξ(t, k)) ≤ U (ξ(0, 0)) ∀(t, k) ∈ dom ξ. (20)
Therefore, for all (t, k) ∈ dom ξ,

α U (|(z(t, k), v 1 (t, k), v 2 (t, k))|) ≤ U (q(0, 0)). (21)
We conclude that the (z, v 1 , v 2 )-component of ξ is bounded, from which we derive that ẑ is also bounded in view of [START_REF] Heemels | Periodic eventtriggered control for linear systems[END_REF]. Furthermore, we deduce from ( 10) and ( 21) that p 1 cannot explode in finite time as its dynamics on flows is bounded by a constant. Finally, we note that φ remains in [a, b] by definition of the sets C and D. Consequently, ξ cannot explode in finite time and it is therefore complete.

3) Maximal solutions are precompact: We would like to apply an invariance principle for hybrid systems from [START_REF] Sanfelice | Invariance principles for hybrid systems with connections to detectability and asymptotic stability[END_REF] to [START_REF] Heemels | Analysis of event-driven controllers for linear systems[END_REF], [START_REF] Khalil | Nonlinear systems[END_REF] to conclude about the desired rendezvous property. For this purpose, we need to ensure that the maximal solutions to [START_REF] Heemels | Analysis of event-driven controllers for linear systems[END_REF] are precompact, i.e. these solutions are complete (which is the case) and bounded. Let ξ be a maximal solution to [START_REF] Heemels | Analysis of event-driven controllers for linear systems[END_REF], [START_REF] Khalil | Nonlinear systems[END_REF]. We have already shown above that the components z, ẑ, v 1 , v 2 , φ of ξ are bounded. We focus on p 1 . Let ave(p 1 , p 2 ) = p1+p2 2 and ave(v 1 , v 2 ) = v1+v2 2 (where p 2 = p 1 + z). For almost all t ∈ I k , where

I k = {t : (t, k) ∈ dom ξ} with k ∈ Z ≥0 , d dt ave(p 1 (t, k), p 2 (t, k)) = ave(v 1 (t, k), v 2 (t, k)) d dt ave(v 1 (t, k), v 2 (t, k)) = -ave(v 1 (t, k), v 2 (t, k)) (22) and for any (t, k) ∈ dom ξ such that (t, k + 1) ∈ dom ξ, ave(p 1 (t, k + 1), p 2 (t, k + 1)) = ave(p 1 (t, k), p 2 (t, k)), ave(v 1 (t, k + 1), v 2 (t, k + 1)) = ave(v 1 (t, k), v 2 (t, k)).
(23) As a result, we see that, for any (t, k) ∈ dom ξ,

ave(p 1 (t, k), p 2 (t, k)) = ave(p 1 (0, 0), p 2 (0, 0)) +(1 -exp(-t))ave(v 1 (0, 0), v 2 (0, 0)), (24)
thus showing that ave(p 1 , p 2 ) is bounded. On the other hand,

p 1 = ave(p 1 , p 2 ) + p 1 -p 2 2 = ave(p 1 , p 2 ) - z 2 . ( 25
)
Consequently, the boundedness of z implies the boundedness of the absolute position p 1 . Hence ξ is precompact.

4) Solutions have a uniform semiglobal dwell-time:

We now verify that the conditions of Corollary 4.4 in [START_REF] Sanfelice | Invariance principles for hybrid systems with connections to detectability and asymptotic stability[END_REF] are verified by system [START_REF] Heemels | Analysis of event-driven controllers for linear systems[END_REF], [START_REF] Khalil | Nonlinear systems[END_REF]. We note that (2) in [START_REF] Sanfelice | Invariance principles for hybrid systems with connections to detectability and asymptotic stability[END_REF] holds with u c (q) = (-1 + 2σ)(v 2 1 + v 2 2 ) when q ∈ C and u c (q) = -∞ when q ∈ R 6 \C and u d (q) = 0 when q ∈ D and u d (q) = -∞ when q ∈ R 6 \D in view of ( 14) and [START_REF] De Persis | Self-triggered rendezvous of gossiping second-order agents[END_REF] and that these functions are non-positive (notice that -1 + 2σ < 0 since σ ∈ (0, 1 2 )) as required by Theorem 4.3 in [START_REF] Sanfelice | Invariance principles for hybrid systems with connections to detectability and asymptotic stability[END_REF]. The conclusions of Corollary 4.4 in [START_REF] Sanfelice | Invariance principles for hybrid systems with connections to detectability and asymptotic stability[END_REF] only apply to precompact solutions. We have proved above that any maximal solution to [START_REF] Heemels | Analysis of event-driven controllers for linear systems[END_REF], ( 12) is indeed precompact. The last point to verify before applying Corollary 4.4 in [START_REF] Sanfelice | Invariance principles for hybrid systems with connections to detectability and asymptotic stability[END_REF] is the existence of a dwell-time for any solution to ( 11), [START_REF] Khalil | Nonlinear systems[END_REF], i.e. for any solution ξ, there exist K, γ > 0 such that for all k ≥ K, sup I k -inf I k ≥ γ for any k ∈ Z >0 , where I k = {t : (t, k) ∈ dom ξ}. Let ∆ > 0 and take any maximal solution ξ to ( 11), [START_REF] Khalil | Nonlinear systems[END_REF] such that |ξ(0, 0)| ≤ ∆. According to [START_REF] De Persis | A Lyapunov redesign of coordination algorithms for cyberphysical systems[END_REF], there exists ∆ > 0 (which depends on ∆) such that, for any

(t, k) ∈ dom ξ, α U (|(z(t, k), v 1 (t, k), v 2 (t, k))|) ≤ α U (|(z(0, 0), v 1 (0, 0), v 2 (0, 0), ψ(z(0, 0)), ψ(ẑ(0, 0)))|) ≤ ∆, which implies |z(t, k)| ≤ |(z(t, k), v 1 (t, k), v 2 (t, k))| ≤ α -1 U ( ∆). ( 26
)
On the other hand, when k ≥ 1, the time between two jumps of any solution to [START_REF] Heemels | Analysis of event-driven controllers for linear systems[END_REF], [START_REF] Khalil | Nonlinear systems[END_REF] corresponds to the time it takes for φ to decrease from b to a. This time interval is lower bounded by the time it takes for θ the solution to the differential equation below

θ = -1 σ 1 + θ 2 max z s.t.|z|≤α -1 U ( ∆) (∇ψ(z)) 2 (27)
to decrease from b to a, in view of ( 26) and according to the comparison principle (see Lemma 3.4 in [START_REF] Khalil | Nonlinear systems[END_REF]). Note that the maximum in ( 27) is well-defined since ∇ψ is continuous and since it is taken over a compact set. The aforementioned time interval 2 is obviously a strictly positive constant τ (a, b, ∆) in view of [START_REF] Seyboth | Event-based broadcasting for multi-agent average consensus[END_REF]. This implies that ξ has a dwell-time which is larger than τ (a, b, ∆); we have proved that the solutions to (11), ( 12) have a uniform semiglobal dwell-time (see Definition 1). We note that by using similar arguments, the time between two jumps of ξ is upper-bounded by the time it takes for θ = -1 σ to decrease from b to a, i.e. σ(b -a), which means that ξ has an unbounded hybrid time domain both in continuous and discrete times. The latter point is not necessary to apply the invariance principle but it will be useful in the following. 2 In fact, the rate of change of θ is upper and lower bounded as follows

- 1 σ 1 + b 2 max z s.t. |z|≤α -1 U ( ∆) (∇ψ(z)) 2 } ≤ θ ≤ - 1 σ .
5) Application of the hybrid invariance principle: We apply Corollary 4.4 in [START_REF] Sanfelice | Invariance principles for hybrid systems with connections to detectability and asymptotic stability[END_REF] to conclude that any maximal solution to [START_REF] Heemels | Analysis of event-driven controllers for linear systems[END_REF], [START_REF] Khalil | Nonlinear systems[END_REF] approaches the largest weakly invariant subset S of

U -1 (r) ∩ U ∩ u -1 c (0) (28)
for some r ∈ U (U) where

U = R 5 × [a, b]. The set u -1 c (0) is equal to q : v 1 = v 2 = 0 .
Note that S is non-empty according to Lemma 3.3 in [START_REF] Sanfelice | Invariance principles for hybrid systems with connections to detectability and asymptotic stability[END_REF]. Let q ∈ S and ξ be a precompact solution such that ξ(0, 0) = q and ξ(t, k) ∈ S for any (t, k) ∈ dom ξ. This implies that, in view of (10) and using the fact that S ⊂ u -1 c (0), for almost all t ∈ I k , where

I k = {t : (t, k) ∈ dom ξ} with k ∈ Z ≥0 ,        ż(t, k) = 0 ż(t, k) = 0 0 = 0 + ψ(ẑ(t, k)) 0 = 0 -ψ(ẑ(t, k)) (29)
and for any (t, k) ∈ dom ξ such that (t, k + 1) ∈ dom ξ,

       z(t, k + 1) = z(t, k) ẑ(t, k + 1) = z(t, k) 0 = 0 0 = 0. (30)
The function ψ only cancels at the origin according to Section III, hence ẑ(t, k) = 0 for almost t ∈ I k and thus for all t ∈ I k by continuity of ẑ(•, k) on I k . Moreover, we have seen that the solutions to ( 11), ( 12) have an unbounded hybrid time domain both in the continuous and in the discrete times. Consequently, z(t, k) = ẑ(t, k) = 0 for any (t, k) ∈ dom ξ in view of [START_REF] Wang | Self-triggered feedback control systems with finite-gain L 2 stability[END_REF]. As a result, the point q = ξ(0, 0) verifies z(0, 0) = ẑ(0, 0) = v 1 (0, 0) = v 2 (0, 0) = 0, which implies that S ⊂ {q : (z, ẑ, v 1 , v 2 ) = 0 and φ ∈ [a, b]}. We deduce that any maximal solution to [START_REF] Heemels | Analysis of event-driven controllers for linear systems[END_REF], [START_REF] Khalil | Nonlinear systems[END_REF] approaches the set {q : (z, ẑ, v 1 , v 2 ) = 0 and φ ∈ [a, b]}. This concludes the proof.

V. SELF-TRIGGERED CONTROL

The event-triggering condition proposed in Section IV requires continuous measures of p 2 -p 1 to trigger control updates. This may not be achievable in practice. We propose to emulate the event-triggering policy as a self-triggering rule to overcome this potential issue.

At each transmission instant, the two agents are now assumed to communicate to each other not only their relative position but also their relative velocity, i.e. v 2 -v 1 . We can then estimate the value of p 2 -p 1 at any time between two successive transmission instants and use this estimate to determine when φ reaches a. We can exactly estimate p 2 -p 1 at time (t, k) based on the value of the state at the last jump instant (t k , k). Indeed, let ξ be a solution to [START_REF] Heemels | Analysis of event-driven controllers for linear systems[END_REF], [START_REF] Khalil | Nonlinear systems[END_REF] and denote dom ξ

= k∈Z ≥0 ([t k , t k+1 ], k). For (t, k) ∈ dom ξ p 1 (t, k) = p 1 (t k , k) + t t k v 1 (s, k) ds, (31)
since

v 1 (t, k) = exp(-(t -t k ))v 1 (t k , k) + (1 -exp(t - t k ))ψ(p 2 (t k , k) -p 1 (t k , k
)), we can compute analytically

p 1 (t, k) based on p 1 (t k , k), p 2 (t k , k), v 1 (t k , k).
We can similarly derive the expression of p 2 (t, k). Hence, using the variable z = p 2 -p 1 for the sake of simplicity, one obtains

z(t, k) = z(t k , k) + (1 -exp(-(t -t k ))) ×[v 2 (t k , k) -v 1 (t k , k) + 2ψ(z(t k , k))] -2ψ(z(t k , k))(t -t k ). (32)
We then need to analytically solve the differential equation below

d dt φ(t, k) = -1 σ 1 + φ 2 (∇ψ(z(t, k))) 2 , φ(t k , k) = b
(33) to determine the next time φ reaches a. Notice that the solution exists locally and is unique. As an alternative to the analytic solution of the equation above, one can assume that enough computational power is available so that the solution of the differential equation can be computed instantaneously (implementation issues that arise with the introduction of this assumption are not tackled here). Then at time (t k , k), it is possible to exactly predict the next time (t k+1 , k) at which φ(t k+1 , k) = b.

Remark 1: From (33), we notice that the triggering instants are periodic when ∇ψ is constant, that is when ψ is linear. This particular case is treated in more detail in Section VI. We model the system as follows

ṗ1 = v 1 v1 = -v 1 + ψ(ẑ) ṗ2 = v 2 v2 = -v 2 -ψ(ẑ) ż = 0 τ = -1                τ ≥ 0, p + 1 = p 1 v + 1 = v 1 p + 2 = p 2 v + 2 = v 2 ẑ+ = p 2 -p 1 τ + = T (a, b, p 1 -p 2 , v 1 -v 2 )                τ = 0. (34)
where τ ≥ 0 is a clock used to trigger transmissions and T (a, b, p 1 -p 2 , v 1 -v 2 ) represents the time it takes from the solution φ to the differential equation

d dt φ(t) = -1 σ 1 + φ 2 (∇ψ(z(t))) 2 , φ(0) = b (35) to be equal to a, with z(t) = p 2 -p 1 + (1 -exp(-t))[v 2 -v 1 + 2ψ(p 2 -p 1 )] -2ψ(p 2 -p 1 )t.
(36) The result below is obtained by following similar lines as in the proof of Theorem 1 in view of the developments above.

Theorem 2: Consider system (34). The solutions have a uniform semiglobal dwell-time and the maximal solutions are precompact and approach the set {(p 1 , v 1 , p 2 , v 2 , ẑ, τ ) : VI. TIME-TRIGGERED CONTROL It is also possible to emulate the event-triggering condition in Section IV as a time-triggered rule. In this case, the transmission instants are periodic, and we denote T this period. In view of the analysis of the dwell-times in Section IV-B.4, it is always possible to compute a lower bound on the inter-jump instants of system [START_REF] Goebel | Hybrid dynamical systems[END_REF] and to use this bound as the sampling period T . This constant depends on the ball of initial conditions in general, see Section IV-B.4. In this section, we focus on the case where a global bound can be computed for the sake of simplicity. We make the assumption below for that purpose.

p 1 = p 2 , v 1 = v 2 = ẑ = 0, and τ ∈ [0, σ(b -a)]}. (a, b) = (1, 10) (a, b) = (0.1, 10) (a, b) = (0.1, 50) (i) (ii) (i) (ii) (i) (ii
Assumption 1: There exists M ≥ 0 such that |∇ψ(z)| ≤ M for any z ∈ R.

Assumption 1 is verified when ψ is a linear function and more generally when it is globally Lipschitz. We define the period T as the time it takes from the solution θ to the differential equation

θ = -1 σ (1 + M 2 θ 2 ), θ(0) = b, (37)
to decrease to a, like in [START_REF] Nešić | Explicit computation of the sampling period in emulation of controllers for nonlinear sampled-data systems[END_REF]. The solution to the differential equation given the initial condition θ(0) = b verifies, for t ≥ 0,

arctan(M φ(t)) = arctan(M b) - M σ t, (38)
from which it is inferred that

T := σ M (arctan(M b) -arctan(M a)). (39)
Since a, b can be chosen arbitrarily, the sampling interval can be changed, although it can never be larger than σ M π 2 in view of (39). However, this choice might affect the speed of convergence of the system the evolution of the velocities depend on the sampled control input. We represent the system using the hybrid model below, like in [START_REF] Nešić | Explicit computation of the sampling period in emulation of controllers for nonlinear sampled-data systems[END_REF],

ṗ1 = v 1 v1 = -v 1 + ψ(ẑ) ṗ2 = v 2 v2 = -v 2 -ψ(ẑ) ż = 0 τ = 1                τ ∈ [0, T ] p + 1 = p 1 v + 1 = v 1 p + 2 = p 2 v + 2 = v 2 ẑ+ = p 2 -p 1 τ + = 0                τ = T. ( 40
)
where τ is the time elapsed since the last transmission and T is defined in (39). The theorem below is obtained by following similar lines as in the proof of Theorem 1.

Theorem 3: Consider system (40) and suppose Assumption 1 holds. The solutions have a uniform global dwelltime and the maximal solutions are precompact and approach the set

{(p 1 , v 1 , p 2 , v 2 , ẑ, τ ) : p 1 = p 2 , v 1 = v 2 = ẑ = 0 and τ ∈ [0, T ]}.

VII. SIMULATION RESULTS

Simulations3 have been run for two choices of the function ψ: (i) ψ(z) = z, (ii) ψ(z) = arctan z for z ∈ R. Both satisfy Assumption 1 with M = 1. We have implemented the self-triggering and the time-triggering rules respectively presented in Sections V and VI; recall that the results are equivalent for the event-triggered and the self-triggered policies as explained in Section V. Figure 1 shows the trajectories of p 1 , p 2 , v 1 and v 2 for each triggering rule in case (ii) when p 1 (0, 0) = 10, p 2 (0, 0) = -5, v 1 (0, 0) = v 2 (0, 0) = 0, ẑ(0, 0) = 0, φ(0, 0) = b, τ (0, 0) = 0, σ = 1/4 and (a, b) = (1, 10). We see that the rendez-vous is achieved and that the velocities converge to zero as expected. We now consider 100 initial conditions uniformly distributed such that p 1 (0, 0), v 1 (0, 0) ∈ [-10, 10], p 2 (0, 0), v 2 (0, 0) ∈ [-15, 15], with the same values as above for ẑ(0, 0), φ(0, 0), τ (0, 0) and we have selected σ = 1/4. Table I provides the average number of events for a simulation time of 20s as well as the time t * it takes for the absolute value of the relative position to become smaller than 0.1, which we use as a measure of the time of convergence. We see that the average number of events is the same for (i) and (ii) for time-triggered control, which is in agreement with the analysis as the constant T in (39) is the same in both cases.

We notice that the time-triggered rule generates more events than self-triggered control; except for (i) in which case these are equivalent, see Remark 1. That is not surprising as the time-triggering condition underestimates the next time at which the self-triggering law is violated. That observation justifies the interest of self-triggered control to reduce the number of events. On the other hand, there is obviously a trade-off between this reduction and the performances of the system. We see in Table I that the fewer the number of events, the bigger the time of convergence. The simulation results also confirm the impact of the pair (a, b) on the system, namely the smaller a (equivalently the bigger b), the fewer the number of events. This point is interesting as these parameters can be used to heuristically adapt the number of events to the desired performances.

VIII. CONCLUSIONS

We have proposed a new type of triggering rules to ensure the event-based rendez-vous of two identical systems. Solutions have been presented for event-triggered control, self-triggered control and time-triggered control. In all cases, the existence of a (uniform) minimum amount of time is guaranteed. The extension of these results to the case where an arbitrary finite number of agents are interconnected over a time-invariant connected graph is investigated in [START_REF] De Persis | A Lyapunov redesign of coordination algorithms for cyberphysical systems[END_REF].

Fig. 1 .

 1 Fig. 1. Trajectories of p 1 , p 2 , v 1 and v 2 (self-triggered control (blue) / time-triggered control (green) / crosses indicate triggering instants).

TABLE I AVERAGE

 I NUMBER OF EVENTS AND AVERAGE VALUE OF t * FOR THE SELF-TRIGGERED CONTROL (#: NUMBER, STC: SELF-TRIGGERED CONTROL, TTC: TIME-TRIGGERED CONTROL).

The tangent cone to C at x is the set of all vectors w ∈ R 6 for which there exist x i ∈ C, τ i > 0 with x i → x, τ i → 0 as i → ∞ such that w = lim i→∞ (x i -x)/τ i ; see Definition 5.12 in[START_REF] Goebel | Hybrid dynamical systems[END_REF].

We have used the HyEQ Matlab toolbox ([START_REF] Sanfelice | A toolbox for simulation of hybrid systems in matlab/simulink: hybrid equations (HyEQ) toolbox[END_REF]).

His work is partially supported by the Dutch Organization for Scientific Research (NWO) under the auspices of the project QUICK (QUantized Information Control for formation Keeping). R. His work is partially supported by the ANR under the grant COMPACS (ANR-13-BS03-0004-02).


Benedikt Bollig

Paul Gastin

Jana Schubert

Parameterized Verification of Communicating Automata under Context Bounds

We study the verification problem for parameterized communicating automata (PCA), in which processes synchronize via message passing. A given PCA can be run on any topology of bounded degree (such as pipelines, rings, or ranked trees), and communication may take place between any two processes that are adjacent in the topology. Parameterized verification asks if there is a topology from a given topology class that allows for an accepting run of the given PCA. In general, this problem is undecidable even for synchronous communication and simple pipeline topologies. We therefore consider context-bounded verification, which restricts the behavior of each single process. For several variants of context bounds, we show that parameterized verification over pipelines, rings, and ranked trees is decidable. Our approach is automata-theoretic and uniform. We introduce a notion of graph acceptor that identifies those topologies allowing for an accepting run. Depending on the given topology class, the topology acceptor can then be restricted, or adjusted, so that the verification problem reduces to checking emptiness of finite automata or tree automata.

Introduction

Communicating automata (CA) are a fundamental and well studied model of parallel systems [START_REF] Brand | On communicating finite-state machines[END_REF]. They consist of finite-state machines that exchange messages over channels determined by a fixed and known communication topology. CA are known to be Turing equivalent so that even basic problems of formal verification such as reachability are undecidable. Therefore, modifications and restrictions have been considered which bring back decidability. Reachability is decidable, for example, when the analysis is restricted to executions with a fixed maximum number of pending messages, or when channels are lossy [START_REF] Abdulla | Verifying programs with unreliable channels[END_REF].

In some contexts such as ad-hoc networks, multi-core programming, or communication-protocol verification, assuming a fixed and known communication topology is not appropriate. Lately, there has been a lot of (ongoing) research in the area of parameterized verification [START_REF] Abdulla | All for the price of few[END_REF][START_REF] Aminof | Parameterized model checking of token-passing systems[END_REF][START_REF] Delzanno | On the power of cliques in the parameterized verification of ad hoc networks[END_REF][START_REF] Esparza | Parameterized verification of asynchronous shared-memory systems[END_REF], which aims to validate a given system independently of the number of processes and the communication topology. A lot of different models of such systems have been proposed (cf. [START_REF] Esparza | Keeping a crowd safe: On the complexity of parameterized verification[END_REF] for a recent survey). In this paper, we investigate the reachability problem for parametrized communicating automata (PCAs). A PCA is a collection of finite automata that can be plugged into any communication topology of bounded degree. PCAs have recently been introduced to initiate a logical study of parameterized systems [START_REF] Bollig | Logic for communicating automata with parameterized topology[END_REF]. Their verification problem has not been considered. Roughly, it can be stated as follows: Given a PCA and a regular set T of pipeline, ring, or tree topologies, is there a topology T ∈ T such that A has an accepting run on T ? Here, "regular" means given by some finite automaton (for pipelines and rings) or tree automaton (for tree topologies), which is part of the input. Note that there is also a universal variant of that problem, and our decision procedures will take care of that case as well.

We actually consider a restriction of PCAs with rendez-vous synchronization, albeit distinguishing between send and receive events. This considerably simplifies the presentation, but the overall approach can be extended to systems with asynchronous bounded channels. Note that rendez-vous communication can also be seen as an underapproximation of the latter.

While bounding the channel capacity or imposing rendez-vous communication bring back decidability of reachability for CA with fixed communication topology, this is no longer true in the case of PCA. For various other (undecidable) models of concurrent systems, decidability is achieved by introducing a context (or "phase") bound, limiting the part of the model simulating synchronization or communication of concurrent processes [START_REF] Bouajjani | Bounded phase analysis of message-passing programs[END_REF][START_REF] La Torre | Context-bounded analysis of concurrent queue systems[END_REF][START_REF] Madhusudan | The tree width of auxiliary storage[END_REF][START_REF] Qadeer | Context-bounded model checking of concurrent software[END_REF]. We adopt the general approach, but introduce new definitions of contexts that are suitable for our setting. An interface-context restricts communication of a process to one neighbor in the topology (e.g., the left neighbor in the pipeline). Another context type separates send from receive events while restricting reception to one interface. Note that, in both cases, there may still be an unbounded number of switches between two given threads.

We show that context-bounded parameterized verification is decidable: it is PSPACE-complete for pipelines and rings, and EXPTIME-complete for ranked trees. Our decidablity proof is automata-theoretic and uniform. We transform a given PCA A, in several steps, into a graph acceptor that recognizes the set of acyclic topologies allowing for an accepting run of A. This solves our problem for pipelines and trees. For rings, an additional adjustment is needed, which rules out cyclic behaviors that the graph acceptor is not able to detect on its own. Related Work. Parameterized verification can be classified into verification of multithreaded programs running on a single core, and protocol verification. Context-bounded verification for systems consisting of an unbounded number of threads has already been considered [START_REF] Atig | Context-bounded analysis for concurrent programs with dynamic creation of threads[END_REF][START_REF] La Torre | Model-checking parameterized concurrent programs using linear interfaces[END_REF]. In [START_REF] Atig | Context-bounded analysis for concurrent programs with dynamic creation of threads[END_REF], a model with process creation is presented, in which a context switch is observed when an active thread is interrupted and resumed. In [START_REF] La Torre | Model-checking parameterized concurrent programs using linear interfaces[END_REF], an unbounded number of threads are scheduled in several rounds. In both cases, the context bound does not impose a bound on the number of threads. However, every thread will be resumed and become active a bounded number of times, which is not the case in our framework.

On the other hand, protocol verification is based on the concept of independent (finite-state) processes communicating over a network-like structure. Due to the absence of a global scheduler, the above context definition is not adequate for protocol verification. A versatile framework for parameterized verification, capturing rendez-vous communication in pipelines, rings, and trees, is presented in [START_REF] Abdulla | All for the price of few[END_REF]. The verification problem is phrased in terms of minimal bad configurations, which does not necessitate context bounds. Motivated by ad-hoc networks, [START_REF] Delzanno | On the power of cliques in the parameterized verification of ad hoc networks[END_REF] considers systems modeled by finite automata that communicate in a broadcast or unicast manner. In the case of unicast communication, the recipient is chosen nondeterministically from the set of neighbors, which is incomparable with the unicast communication of PCAs. Direction-aware token-passing systems [START_REF] Aminof | Parameterized model checking of token-passing systems[END_REF][START_REF] Emerson | Parameterized model checking of ring-based message passing systems[END_REF][START_REF] Emerson | On reasoning about rings[END_REF] can be modeled in our framework as far as bounded-degree structures such as rings are concerned. To the best of our knowledge, neither context bounds nor the PCA model have been considered yet for protocol verification.

Outline. Section 2 recapitulates basic notions such as words and finite (tree) automata. In Section 3, we introduce topologies, PCAs, and several contextbounded verification problems. Section 4 is the heart of our automata-theoretic approach, where we first translate PCA into a sort of cellular automaton and, in a second step, into topology acceptors. These constructions will be exploited, in Section 5, to solve the parameterized verification problem for the classes of pipelines, rings, and ranked trees. Missing proofs can be found in the appendix.

Preliminaries

For n ∈ N, we set [n] := {1, . . . , n}. Let A be an alphabet, i.e., a nonempty finite set. The set of finite words over A is denoted by A * , which includes the empty word ε. The concatenation of words w 1 , w 2 ∈ A * is denoted by w 1 • w 2 or w 1 .w 2 . Given an index set I and a tuple a = (a i ) i∈I ∈ A I , we write a| i to denote a i .

A finite automaton over A is a tuple B = (S, =⇒, ι, F ) where S is the finite set of states, ι ∈ S is the initial state, F ⊆ S is the set of final states, and =⇒ ⊆ S × A × S is the transition relation. We write s a =⇒ s ′ instead of (s, a, s ′ ) ∈ =⇒. A run of B on a word w = a 1 . . . a n ∈ A * is a sequence s 0 s 1 . . . s n ∈ S * of states such that s 0 = ι and s i-1 ai =⇒ s i for all i ∈ [n]. The run is accepting if s n ∈ F . Finally, the language of B is defined as L(B) := {w ∈ A * | there is an accepting run of B on w}.

For trees, we fix a (maximal) rank r ∈ N. An r-tree over A is a pair (V, π) where V is a nonempty finite prefix-closed subset of {1, . . . , r} * , and π : V → A is a labeling function. The set V is the set of nodes of the tree, and ε is its root. For u ∈ V and l ∈ [r] with u.l ∈ V , we say that u.l is the l-th child of u. An r-tree automaton over A is a tuple B = (S, ∆, F ) where S is the finite set of states, F ⊆ S is the set of final states, and

∆ ⊆ S × A × (S ⊎ {⊥}) r is the transition relation. A run of B on an r-tree (V, π) is a mapping ρ : V → S such that, for all u ∈ V , (ρ(u), π(u), (s l ) l∈[r] ) ∈ ∆ where s l = ρ(u.l) if u.l ∈ V , and s l = ⊥ if u.l ∈ V . The run is accepting if ρ(ε) ∈ F . By L(B),

Parameterized Communicating Automata

In this section, we introduce our model of a communicating system that can be run on arbitrary topologies of bounded degree.

Topologies. A topology is a graph, whose nodes are connected via interfaces. The idea is that each node runs a finite-state process (of type p, q, . . .). In Figure 1, for example, nodes are arranged in a pipeline, which allows a process to communicate with a left and a right neighbor (if they exist). When a node u emits a message m via its interface right, then m can be received by the neighbor on the right of u, using interface left. Let N = {a, b, c, . . .} and P = {p, q, . . .} be finite sets of interface names and process types, respectively.

Definition 1. A topology over N and P is a tuple T = (V, ν, π) where V is the nonempty finite set of nodes (or processes), π : V → P associates with every node a process type, and ν : V × N ⇀ V is a partial mapping. Intuitively, ν(u, a) = v means that the interface a of u points to v. We suppose that, for all u ∈ V , there is at last one a ∈ N such that ν(u, a) is defined. Moreover, we require that ν(u, a) = v implies (1) u = v, (2) ν(v, b) = u for some b ∈ N , and

(3) ν(u, a ′ ) = v ′ implies [a = a ′ iff v = v ′ ],
for all a ′ ∈ N and v ′ ∈ P .

We write u a b v if ν(u, a) = v and ν(v, b) = u, and we write u v if u a b v for some a, b ∈ N . We call T acyclic if the undirected graph (V, ) is acyclic. This paper will focus on three topology classes: Pipelines. A pipeline over a nonempty finite set P of process types is a topology over N = {left, right} and P. It is of the form T = ({1, . . . , n}, ν, π), with n ≥ 2, such that ν(i, right) = i + 1 and ν(i + 1, left) = i for all i ∈ {1, . . . , n -1}, and ν(1, left) and ν(n, right) are both undefined. A finite automaton B over P can be seen as a pipeline recognizer. Indeed, a pipeline is uniquely given by the sequence π(1) . . . π(n) ∈ P * . So, we let L pipe (B) denote the set of pipelines ({1, . . . , n}, ν, π) over P such that π(1) . . . π(n) ∈ L(B). Instead of B, we may use a classical regular expression. An example pipeline is depicted in Figure 1. It is uniquely given by the word pqpq.

Rings.

A ring over P is a topology over N = {left, right} and P of the form T = ({1, . . . , n}, ν, π), with n ≥ 3, where ν(i, right) = (i mod n) + 1 and ν((i mod n) + 1, left) = i for all i ∈ [n]. Similarly to pipelines, a finite automaton B over P can be used as a ring recognizer: we let L ring (B) denote the set of rings ({1, . . . , n}, ν, π) over P such that there is i ∈ [n] satisfying π(i) . . . π(n)π(1) . . . π(i -1) ∈ L(B). This takes into account that, a priori, rings do not have an "initial" node. Figure 2 depicts a ring with five nodes.

Trees. For r ≥ 2, an r-tree topology over P is a topology T = (V, ν, π) over {father, child 1 , . . . , child r } and P such that (V, π) is an r-tree over P, ν(ε, father) is undefined, and for all u ∈ V and l ∈ [r], we have (1) u.l ∈ V implies ν(u, child l ) = u.l and ν(u.l, father) = u, and (2) u.l ∈ V implies that ν(u, child l ) is undefined. An r-tree automaton B over P can be seeen as a recognizer for tree topologies: we write L tree (B) for the set of r-tree topologies (V, ν, π) such that (V, π) ∈ L(B). A sample 2-tree topology is depicted in Figure 3.

The Automata Model. Next, we introduce our system model. As suggested above, a parameterized communicating automaton is a collection of finite-state processes whose actions refer to an interface. Unless stated otherwise, we assume that N is a fixed nonempty finite set of interface names (or, simply, interfaces). Definition 2. A parameterized communicating automaton (PCA) over N is a tuple A = (P, Msg, (A p ) p∈P ) where P is a nonempty finite set of process types, Msg is a nonempty finite set of messages, and A p is a finite automaton over the set of actions Σ A := {a!m , a?m | a ∈ N and m ∈ Msg}, for every p ∈ P.

A pipeline PCA or ring PCA is a PCA over {left, right}. Moreover, for r ≥ 2, an r-tree PCA is a PCA over {father, child 1 , . . . , child r }.

The idea is the following: When A is run on a topology (V, ν, π) with adjacent processes u a b v, then u runs a copy of A π(u) and can emit a message m through interface a by executing a!m. Process v receives the message if it is ready to execute b?m. We assume that communication is by rendez-vous, i.e., messages are received instantaneously.

For convenience, we write Σ instead of Σ A . Sometimes, we will even mention Σ without any reference to A. However, notice that the alphabet depends on a PCA (more precisely, on N and a set of messages). Let Σ ! := {a!m | a ∈ N and m ∈ Msg} and let Σ ? be defined accordingly. These sets are further refined to Σ a! and Σ a? , containing only those actions that refer to interface a ∈ N .

Semantics of PCAs.

Let A = (P, Msg, (A p ) p∈P ) be a PCA over N , with A p = (S p , =⇒ p , ι p , F p ) for all p ∈ P. The PCA A can be run on any topology T = (V, ν, π) over N and P. The semantics of A wrt. T is a finite automaton

[[A]] T = (S, =⇒, ι, F ) over Σ T ⊆ (Σ ∪ {ε}) V . The alphabet Σ T contains, for all v a b v ′ and m ∈ Msg, the tuple v, m, v ′ := (σ u ) u∈V where σ v = a!m, σ v ′ = b?m, and σ u = ε for all u ∈ V \ {v, v ′ }. For W = γ 1 . . . γ n ∈ (Σ T ) * and u ∈ V , we define the projection of W to u as W | u := (γ 1 | u ) • . . . • (γ n | u ) ∈ Σ * . For u ∈ V , we write A u , S u , =⇒ u , ι u , F u for A π(u) , S π(u) , =⇒ π(u) , ι π(u) , F π(u) , respectively.

The set of states of [[A]]

T is S = u∈V S u , keeping track of the local state of every process in the topology. Accordingly, the initial state is ι = (ι u ) u∈V , and the set of final states is

F = u∈V F u . The transition relation =⇒ ⊆ S × Σ T × S is defined as follows. Let s = (s u ) u∈V ∈ S, s ′ = (s ′ u ) u∈V ∈ S, and σ = (σ u ) u∈V ∈ Σ T . Then, s σ =⇒ s ′ if, for all u ∈ V , we have that σ u = ε implies s u σu = =⇒ u s ′ u , and σ u = ε implies s u = s ′ u . The language of A wrt. T is defined as L(A, T ) := L([[A]] T ).
Example 1. Consider the PCA A = (P, Msg, (A p , A p, A q , A q )) over the set of interfaces N = {left, right}, where P = {p, p, q, q}, Msg = {m}, and the local languages are given as follows:

L(A p ) = {(right!m)} L(A q ) = {(left?m)(right!m)} L(A p) = {(left?m)} L(A q ) = {(right!m)(left?m)}
Let Q be the regular expression (q + q) * . For all pipelines T over P, we have

L(A, T ) = ∅ iff T ∈ L pipe ((pQp) * ).
In particular, for n ≥ 2 and the pipeline T given by pq n-2 p, we have

L(A, T ) = { 1, m, 2 2, m, 3 . . . n -1, m, n }.
When we consider rings instead, the reasoning is less evident. Note that L(A, T ) = ∅ for all T ∈ L ring (q * + q * ): though two successive processes qq or q q match locally, meaning that an open send encounters an open receive, closing a sequence q n or qn towards a ring is not possible due to the causal dependencies that are created. In q n , for example, the receive that remains open is always scheduled before the remaining open send. Thus, matching both will create a cyclic dependency and not lead to a valid run of A. However, pathologic dependencies are "resolved" in a ring over {q, q} whenever it contains q q (which implies that there is also qq when the ring is seen as a cyclic word). We actually have, for all rings T over P, that L(A, T ) = ∅ iff T ∈ L ring ((pQp) * + Qq qQ). Detecting cyclic dependencies will be one challenge when we tackle the verification problem for rings in Section 5.

Context-Bounded Parameterized Emptiness. Next, we define several variants of contexts, which restrict the behavior of each process of a PCA. A word w ∈ Σ * is called an

-(s⊕r)-context if w ∈ Σ * ! ∪ Σ * ? , -(s1+r1)-context if w ∈ (Σ a! ∪ Σ b? ) * for some a, b ∈ N , -(s⊕r1)-context if w ∈ Σ * ! ∪ Σ * a?
for some a ∈ N , and

-intf-context if w ∈ (Σ a! ∪ Σ a? ) * for some a ∈ N .
The case s1⊕r (w ∈ Σ * a! ∪ Σ * ? for some a ∈ N ) is symmetric to s⊕r1, and we only consider the latter. All results hold verbatim when we replace s⊕r1 with s1⊕r.

Let k ≥ 1 and t ∈ {s⊕r, s1+r1, s⊕r1, intf} be a context type. We say that

w ∈ Σ * is (k, t)-bounded if there are w 1 , . . . , w k ∈ Σ * such that w = w 1 • . . . • w k and w i is a t-context, for all i ∈ [k]. The set of all (k, t)-bounded words (over a fixed Σ) is denoted by W (k,t) . For a PCA A = (P, Msg, (A p ) p∈P ) and a topology T = (V, ν, π), we define L (k,t) (A, T ) := {W ∈ L(A, T ) | W | u ∈ W (k,t)
for all u ∈ V }. Note that W (k,t) is a regular word language that is recognized by a finite automaton B (k,t) whose number of states is linear in k and at most quadratic in |N | (but linear for the decidable cases of t). Let A ′ be the PCA Pipeline-Nonemptiness(t)

I: pipeline PCA A = (P, Msg, (Ap)p∈P ) k ≥ 1; finite automaton B over P Q: L (k,t) (A, T ) = ∅ for some T ∈ Lpipe (B) ?
Ring-Nonemptiness(t)

I: ring PCA A = (P, Msg, (Ap)p∈P ) k ≥ 1; finite automaton B over P Q: L (k,t) (A, T ) = ∅ for some T ∈ Lring (B) ?
Treer-Nonemptiness(t) A,T ) for all topologies over {left, right} and {p, p, q, q}.

I: r-tree PCA A = (P, Msg, (Ap)p∈P ) k ≥ 1; r-tree automaton B over P Q: L (k,t) (A, T ) = ∅ for some T ∈ Ltree (B) ? s⊕r1 intf pipelines PSPACE-c PSPACE-c rings PSPACE-c PSPACE-c trees EXPTIME-c EXPTIME-c
L(A, T ) = L (2,s⊕r1) (A, T ) = L (2,intf) (
For t ∈ {s⊕r, s1+r1, s⊕r1, intf}, we consider the problems listed in Table 1. Note that the context bound k is always part of the input. We assume that k is encoded in unary. The table also gives a summary of the positive results of the paper. For some context types, however, all problems are undecidable.

Theorem 1. All problems listed in Table 1 are undecidable for t ∈ {s⊕r, s1+r1}, even when we restrict to one context for each process.

Proof (sketch). Figures 4 and5 demonstrate how to generate grid-like structures of arbitrary height i and width j, using only one context on each single process. Figure 4, for example, visualizes an execution of the form ( 1, m (1,1) , 2 2, m (1,2) , 3 . . . j, m (1,j) , j + 1 ) . . . ( 1, m (i,1) , 2 2, m (i,2) , 3 . . . j, m (i,j) , j + 1 ) .

The idea is now to simulate a Turing machine, using the (unbounded) vertical dimension to encode its tape, which changes along the (unbounded) horizontal line. More precisely, the leftmost process generates a sequence of messages (m (1,1) , . . . , m (i,1) ) that corresponds to the initial configuration with arbitrarily many cells. Each further process may locally change that configuration while passing it to its right neighbor, and so on. In the case of s⊕r, the transfer of a configuration is sometimes accomplished by a receive context. Here, reception is blocking if the messages coming from the right neighbor do not correspond to the next configuration. Obviously, the encoding also works for rings as well as for the (more general) trees. It is important to note that it does not matter if the semantics is via rendez-vous (as it is our case) or asynchronous.

⊓ ⊔

From PCAs to Topology Acceptors

In this section, we lay the basis for a uniform approach to parameterized verification under context bounds of type s⊕r1 or intf. We first show that, assuming a context bound of type s⊕r1 or intf, a given PCA can be simulated by a sort of cellular automaton, which works similarly to PCAs but performs only a bounded number of steps on each process. The idea is that single contexts are summarized to one step of maximally |N | + 1 processes. This transformation works for both context types, with only minor differences. In a further step, which is then independent of a context type, the cellular automaton is translated into a topology acceptor, which no longer has an operational semantics but a "static" one: a run is a tiling of a topology with transitions. When we restrict a topology acceptor to pipelines or tree topologies, we obtain a finite automaton or tree automaton, respectively. Thus, this transformation solves our verification problems for tree and pipeline topologies.

Unfortunately, the topology acceptor is only guaranteed to be correct for acyclic topologies. It may actually accept cyclic topologies that do not admit an accepting run of the given PCA. Nevertheless, for the class of rings, we can enrich a topology acceptor with additional information that helps keeping track of interdependencies between contexts of different processes (cf. Example 1). This will allow us to build a finite automaton recognizing the unfoldings of rings having an accepting PCA run (Lemma 3).

We explain the general idea by means of Figure 6. Assume context type s⊕r1, which is the more difficult case. The figure depicts an execution (in fact, a set of "order"-equivalent executions) that is (3, s⊕r1) bounded. Processes 1, 2, and 3 use three contexts, while 4 and 5 can do with a single one. The dotted areas on a process line suggest that we actually consider an arbitrary number of actions. Our aim is to aggregate these unboundedly many actions in a bounded number of summaries Si so that a finite automaton can read the pipeline (i.e., the word pppqq) from left to right, while verifying that the summaries can be glued together towards an accepting run of the given PCA.

As process 4 alternates between sending to 3 and sending to 5, its summaries have to include the behavior of processes 3 and 5. A summary is then given by a cell transition of the form s pqq --→ s ′ . Here, cell refers to pqq, which represents an isomorphism type of a pipeline of length three. Moreover, s, s ′ ∈ S p × S q × S q denote how states evolve in that particular fragment within a bigger pipeline, for example when executing all actions gathered in S5. Cells have bounded size so that the set of cell transitions can be effectively computed and represented. Now, the behavior of process 4 can only be captured when we use at least two cell transitions (for S5 and S6). The reason is that receives of process 3 from 4 are interrupted by receives from process 2. Similarly, the receive con- text in the middle of process 3 will belong to two different summaries, as it is "interrupted" by a context switch on process 2. The splitting is not unique, as we could have merged S3 and S4. However, the total number of splits can be bounded: a send (receive) context is split whenever the complementary receives (sends, respectively) belong to distinct contexts. Thus, it is divided into at most k • |N | summaries. As a result, any (k, s⊕r1)-bounded execution of a PCA is captured by a sequence of cell transitions such that each process is involved at most k

• (|N | 2 + 2|N | + 1
) times (cf. appendix). This gives us a bounded abstraction of a priori unbounded behaviors so that we can build a finite automaton that guesses such an abstraction and, simultaneously, checks if it corresponds to an accepting run of the PCA. A run of the finite automaton (topology acceptor in the general case) is depicted in Figure 7. We come back to it later.

Let us formalize these ideas. In the following, we do not restrict to pipelines, so N is an arbitrary alphabet of interface names. A topology C = (V, ν, π) is called a cell if there is ū ∈ V such that (1) for all u ∈ V \ {ū}, we have ū u, and (2) for all u, u ′ ∈ V \ {ū}, we do not have u u ′ . We call ū a center of C. Note that C is star-shaped, and we have |V | ≤ |N | + 1.

In the following, we define cell transitions to represent summaries. Let A = (P, Msg, (A p ) p∈P ) be a PCA over N , with A p = (S p , =⇒ p , ι p , F p ). Moreover, let C = (V, ν, π) be a cell (over N and P). Suppose that [[A]] C = (S, =⇒, ι, F ) and s, s ′ ∈ S = u∈V S u . We let

-s C - -→ intf s ′ if |V | = 2 and L((S, =⇒, s, {s ′ })) \ {ε} = ∅ ; -s C - -→ s⊕r1 s ′ if there are a center ū ∈ V of C and a word W ∈ L((S, =⇒, s, {s ′ })) such that W | ū ∈ Σ + ! and W | u ∈ Σ + ?
for all u ∈ V \ {ū}. Thus, if C contains at least three nodes, then there is a unique center, and this center "executes" only send actions.

Next, we apply cell transitions on arbitrary topologies T = (V, ν, π). For t ∈ {s⊕r1, intf}, we define a finite automaton A T t = (S, =⇒ t , ι, F ) where S, ι, and F are as in [[A]] T . Moreover, =⇒ t is a subset of S × Γ × S, where Γ is the set of sub-structures of T that are cells. For states s = (s u ) u∈V and s ′ = (s ′ u ) u∈V from S and a cell C ∈ Γ with set of nodes U ⊆ V , we let s

C = =⇒ t s ′ if we have both (s u ) u∈U C - -→ t (s ′ u ) u∈U and s u = s ′ u for all u ∈ V \ U . For K ≥ 1, we define L K ( A T t ) to be the set of words W = C 1 . . . C n ∈ L( A T t ) such that, for all u ∈ V , we have |{i ∈ [n] | u is a node of C i }| ≤ K. Lemma 1. Let t ∈ {s⊕r1, intf}, k ≥ 1, and K = k • (|N | 2 + 2|N | + 1
). Let A = (P, Msg, (A p ) p∈P ) be a PCA such that L(A p ) ⊆ W (k,t) for all p ∈ P. Then, for all topologies T (over N and P), we have

L K ( A T t ) = ∅ iff L (k,t) (A, T ) = ∅.
Thus, the behavior of a context-bounded PCA can be faithfully represented by a "cellular" automaton that performs a bounded number of transitions on each process. The next step is to translate cellular automata into topology acceptors, which are similar to graph acceptors [START_REF] Thomas | Elements of an automata theory over partial orders[END_REF]. A run of a topology acceptor is a covering of a topology with cell-shaped tilings. Definition 3. A topology acceptor (TA), over N and P, is a pair G = (S, ∆) where S is a finite set of states and ∆ is a finite set of transitions. A transition is a triple (C, ū, ρ) where C = (V, ν, π) is an isomorphism type of a cell, ū ∈ V is a center of C, and ρ : V → S is a mapping.

Let T = (V, ν, π) be a topology and γ : V → S be a mapping. Given ū ∈ V , we denote by cell (T , ū, γ) the triple (C, ū, ρ) where C is the cell induced in T by the center ū (the set of nodes of C being V ′ = {ū} ∪ {u ∈ V | ū u}), and ρ is the restriction of γ to V ′ . We say that γ is a run of G on T if, for all ū ∈ V , we have that cell (T , ū, γ) ∈ ∆. By L(G), we denote the set of topologies for which there is a run. Note that there is no particular acceptance condition in a TA. Lemma 2. Let t ∈ {s⊕r1, intf} and k ≥ 1. Let A be a PCA over N with process types P. In exponential time, we can construct a TA G (of exponential size) such that, for all acyclic topologies T (over N and P), we have

T ∈ L(G) iff L (k,t) (A, T ) = ∅.
Proof. Let A = (P, Msg, (A p ) p∈P ) be the given PCA over N , with A p = (S p , =⇒ p , ι p , F p ). We will assume that the sets S p are pairwise disjoint. We also assume that L(A p ) ⊆ W (k,t) for all p ∈ P. Recall that this can be achieved at the expense of a linear blow-up in the size of A p .

Note that there are |P| • ((|N | • |P|) + 1) |N | isomorphism types C = (V, ν, π) of a cell. For each of them and all states s, s ′ ∈ u∈V S u of the finite automaton [[A]] C , we first determine whether s C --→ t s ′ , as defined above. Once the C, s, s ′ are fixed, this check reduces to a reachability analysis that can be done in polynomial time (since |N | is fixed). Now, we construct the desired TA G = (S, ∆) as follows.

Set K = k • (|N | 2 + 2|N | + 1)
. Recall that K is the bound that we imposed, in Lemma 1, on the number of local steps in the finite automaton A T t . A state from S is an alternating sequence θ = (s 0

τ1 -→ s 1 τ2 -→ . . . τ K --→ s K )
where for some p ∈ P we have s 0 = ι p , s K ∈ F p and all other states are also in S p , and each τ i is either an interface name τ i ∈ N , or a set of interface names τ i ⊆ N , or ε. The sequence θ describes a summary of the run performed by A on some node u of the topology (to which θ is assigned in a run of G). We use τ i ⊆ N to describe a summary step s i-1 τi -→ s i of a cell C in which u is a center and communicates through the interface names in τ i . We use τ i ∈ N to indicate that u is taking part in a summary step s i-1 τi -→ s i of a cell C in which u is not the center and u communicates only through the interface name τ i . Inserting ε-transitions allows us to consider sequences of equal length, which somehow simplifies the presentation. Hence, we assume that s i-1 = s i when τ i = ε.

Let θ, θ ′ ∈ S be sequences with labels τ 1 , . . . , τ K and τ ′ 1 , . . . , τ ′ K , respectively. We let f θ (a, i) = |{ℓ ≤ i | a ∈ τ ℓ ∨ a = τ ℓ }| be the number of times interface a ∈ N was used up to transition i in θ. Also, we say that θ and θ ′ match on a link a b if we have [START_REF] Abdulla | All for the price of few[END_REF]

f θ (a, K) = f θ ′ (b, K), (2) for all i ∈ [K] with a ∈ τ i there exists j ∈ [K] with b = τ ′ j and f θ (a, i) = f θ ′ (b, j)
, and (3) the symmetric condition.

Transitions of G will check that the summary runs guessed locally at each node are compatible. This is illustrated in Figure 7, showing a run of G that corresponds to the PCA run in the adjoining figure. For simplicity, states are omitted. Let C = (V, ν, π) be a cell, ū ∈ V be a center of C, and ρ : V → S. Then, (C, ū, ρ) is a transition of G if the following hold:

(a) For all u ∈ V , the states that occur in ρ(u) are all from S π(u) . (b) For all u ∈ V and a, b ∈ N such that ū a b u in C, the sequences ρ(ū) and ρ(u) match on a b . (c) For all i ∈ [K] such that the i-th transition label of ρ(ū) is τ i ⊆ N , we require that there is a sub-cell D = (V ′ , ν ′ , π ′ ) of C, with center ū and dom(ν ′ (ū)) = τ i , and there is a transition s D --→ t s ′ where s = (s u ) u∈V ′ and s ′ = (s ′ u ) u∈V ′ are states from u∈V ′ S u such that the following hold:

• the i-th transition of ρ(ū) is s ū τi -→ s ′ ū,
and • for all a ∈ τ i , there are u ∈ V ′ and b ∈ N such that ū a b u in D and there is j

∈ [K] such that the j-th transition of ρ(u) is s u b -→ s ′ u and f ρ(ū) (a, i) = f ρ(u) (b, j).
This concludes the construction of G. The correctness proof, which crucially relies on Lemma 1, can be found in the appendix.

⊓ ⊔

The above construction is only correct for acyclic topologies. Consider the PCA from Example 1. Figure 8 illustrates that the corresponding TA G accepts the ring T induced by qqqq, though we have L(A, T ) = ∅. The reason is that G checks locally whether a run encodes a composition of cell transitions, without retrieving cyclic dependencies that violate the run conditions of PCAs.

Context-Bounded Parameterized Verification

When we are only interested in pipelines, rings, or trees, a TA can be translated to a finite automaton or, respectively, tree automaton, which is then checked for emptiness. This allows us to apply the construction and ideas presented in the previous section to context-bounded verification over trees, pipelines, and rings. The case of rings, however, needs some additional subtle argument.

Theorem 2. The problem Tree r -Nonemptiness(t) is EXPTIME-complete, for all r ≥ 2 and t ∈ {s⊕r1, intf}.

Proof. We first show the upper bound. By Lemma 2, we can transform an r-tree PCA with set of process types P into a TA G over {father, child 1 , . . . , child r } and P of exponential size. It is standard to transform the TA G into a tree automaton B (with polynomial blow up) such that, for all r-tree topologies T over P, we have T ∈ L(G) iff T ∈ L tree (B). As emptiness of tree automata is decidable in polynomial time, this gives us an EXPTIME decision procedure.

The lower bound is by reduction from the intersection problem for binarytree automata, which is EXPTIME-complete [START_REF] Seidl | Haskell overloading is DEXPTIME-complete[END_REF]. Without loss of generality, we assume here that tree automata accept only trees where the root and every internal node have exactly two children. Given k ≥ 1 and binary-tree automata B 1 , . . . , B k , we construct, in polynomial time, a PCA A such that, for all 2-tree topologies T , we have

L (2k,s⊕r1) (A, T ) = ∅ iff L (3k,intf) (A, T ) = ∅ iff T ∈ L tree (B 1 ) ∩ . . . ∩ L tree (B k ).
The idea is that each internal node u in the tree topology chooses transitions δ 1 , . . . , δ k of B 1 , . . . , B k , respectively, that are applied at u. These transitions are sent to the children u.1 and u.2 of u. When u.1 (or u.2) receives a transition δ i , it immediately sends a corresponding transition δ ′ i to its own children. This is why the PCA works with 2k and 3k contexts. ⊓ ⊔ Theorem 3. The problem Pipeline-Nonemptiness(t) is PSPACE-complete, for all t ∈ {s⊕r1, intf}.

Proof. For the upper bound, we again use Lemmas 1 and 2, which allow us to transform a PCA into a TA G. The latter, in turn, can be transformed into a finite automaton (we perform a more sophisticated construction below for rings). However, the construction has to be done "on-the-fly" so that it takes only polynomial space. The pre-computation of the cell transitions s C --→ t s ′ can be done in polynomial time. Moreover, a single state of G is representable using polynomial space. Clearly, checking if a sequence of at most three consecutive states of G form a valid transition can be done in polynomial space. Putting all that together, we obtain a PSPACE procedure.

The lower-bound proof is an adaptation of the lower-bound proof for Theorem 2, but uses intersection of finite automata, which is PSPACE-complete. ⊓ ⊔ Theorem 4. The problem Ring-Nonemptiness(t) is PSPACE-complete, for all t ∈ {s⊕r1, intf}.

The rest of this section is devoted to the proof of Theorem 4. Recall that we cannot simply apply Lemma 2, since the constructed TA G is only guaranteed to be correct when running on acyclic topologies. Consider the (2, s⊕r1)-and (2, intf)-bounded PCA A from Example 1. For simplicity, we suppose K = 2 (cf. Lemma 1). Let T be the ring topology induced by qqqq. Though L(A, T ) = ∅, there is a run of the associated TA G on T , which is illustrated in Figure 8. Essentially, the run checks, locally, if two successive local executions fit together. There is, by now, no mechanism that keeps track of the causal dependency between events created during a run. In particular, it does not record that the gray-shaded left-event (which arised from a receive action) is scheduled before the gray-shaded right-event (which arised from a send action). Thus, those events cannot be matched, i.e., the run of G does not reflect a run of A. We will, therefore, enrich G to obtain a decision procedure for rings.

To be able to infer dependencies from cell transitions, we slightly modify the definition of s C --→ s⊕r1 s ′ : we require that there are a center ū ∈ V of C and a word W ∈ L((S, =⇒, s,

{s ′ })) such that (1) W | ū ∈ Σ + ! and |V | = 2, or (2) W | ū ∈ Σ * ! (Σ + left! Σ + right! Σ + left! )Σ * ! ∪ Σ * ! (Σ + right! Σ + left! Σ + right! )Σ * ! . Condition (2)
guarantees that there are at least two direction switches in the sending phase of ū. Note that Lemma 1 is still valid at the cost of a linear blow up of K.

The idea is now to add dependence graphs that keep track of the causal dependencies between cell transitions. They arise naturally when we combine the behavior of two processes in terms of states of G. For processes 1 and 2 in Figure 8, we obtain the dependence graph D qq depicted in Figure 9. There are two kinds of constraints, an undirected one representing synchronizations (the thick gray lines), and a directed one for strict causality (depicted by arrows). The effect of appending a further process of type q can be computed as a composition D qq • D qq , which we obtain by merging the right side of the first graph with the left side of the second, taking the transitive closure of the constraints, and removing the middle nodes (in the figure, we represent the transitive closure by a minimal set of constraints). Now, "closing" the pipeline qqqq towards a ring corresponds to joining the left and right hand side of (D qq ) 4 = (D qq ) 2 , depicted as join((D qq ) 4 ) in Figure 9. But this creates a cycle using at least one constraint of type →, which has to be interpreted as a violation of the run condition of PCAs. However, if the third process is of type q (executing (right!m)(left?m)), D qq is composed with D q q , which results in D qq • D q q . Closing the pipeline corresponds to appending D qq , which resolves the "bad" dependency and results in the graph at the bottom right, whose join is harmless. Let us implement these ideas. Lemma 3. Suppose t ∈ {s⊕r1, intf} and k ≥ 1. Let A be a ring PCA with process types P. We can construct a finite automaton B over P of exponential size such that, for all rings T over P, we have T ∈ L ring (B) iff L (k,t) (A, T ) = ∅.

Proof. We start from the TA G = (S, ∆) over {left, right} and P that we obtain according to the proof of Lemma 2. Recall that a state of G is a sequence s 0 τ1 -→ s 1 τ2 -→ . . . (Ω, → 2 , ∼ 2 ) is obtained as follows. In D 1 , we rename every ⊳ i into ♭ i . Similarly, in D 2 , rename every ⊲ i into ♭ i . The composition is then defined as (Ω, →, ∼) where → is the restriction of

E * • (→ 1 ∪ → 2 ) • E * to Ω, where E = → 1 ∪ ∼ 1 ∪ → 2 ∪ ∼ 2 ,
and ∼ is the restriction of (∼ 1 ∪ ∼ 2 ) + to Ω. We also define a join operation on dependence graphs D = (Ω, →, ∼) and let join(D) be the dependence graph 9).

(Ω, →, ∼ ∪ {(⊲ i , ⊳ i ) , (⊳ i , ⊲ i ) | i ∈ [K]}) (cf. Figure
With a pair (θ, θ ′ ) ∈ S × S, we now associate a dependence graph D θθ ′ . Suppose the labels of θ are τ 1 , . . . , τ K and the labels of the sequence θ ′ are τ ′ 1 , . . . , τ ′ K . Then, we define 8 and9). Let us determine the finite automaton B over P such that T ∈ L ring (B) iff L (k,t) (A, T ) = ∅, for all rings T over P. To allow for a modular construction, we will actually build a finite automaton reading words over P × S. We define B as the product of two finite automata. First, B run accepts those words w = (p 1 , θ 1 ) . . . (p n , θ n ) ∈ (P × S) * of length n ≥ 3 such that the mapping {1 → θ 1 , . . . , n → θ n } is a run of G on the ring with set of nodes V = {1, . . . , n} that is induced by p 1 . . . p n . As is the case for pipelines and trees, this construction is easy and omitted. The second finite automaton, B dep , checks the dependencies that we create during a run. A state of B dep is either ι, or a triple (θ 1 , θ 2 , D) where θ 1 , θ 2 ∈ S denote the very first and, respectively, the last state of G that were read so far (thus, θ 1 is invariant along a run), and D is a dependence graph. Let w = (p 1 , θ 1 )(p 2 , θ 2 ) ∈ (P × S) 2 . We have an initial transition ι w = =⇒ (θ 1 , θ 2 , D θ1θ2 ). For simplicity, we hereby allow B dep to read two letters at once. Now, let θ 1 , θ 2 ∈ S, (p, θ 3 ) ∈ P × S, and D be a dependence graph. Then, we have a transition (θ 1 , θ 2 , D) (p,θ3) = == =⇒ (θ 1 , θ 3 , D • D θ2θ3 ). Thus, the "last" state θ 2 is updated to θ 3 , and the dependence graph is updated to the new dependency created in terms of θ 3 . Finally, (θ 1 , θ 2 , D) is a final state if join(D • D θ2θ1 ) does not have a cycle using edges in → ∪ ∼, and using → at least once. Intuitively, this means that the pipeline can be closed towards a ring.

D θθ ′ = (Ω, →, ∼) by → = {(⊲ i , ⊲ j ) , (⊳ i , ⊳ j ) | 1 ≤ i < j ≤ K} and ∼ = {(⊲ i , ⊳ j ) , (⊳ j , ⊲ i ) | (right ∈ τ i or right = τ i ) and (left ∈ τ ′ j or left = τ ′ j ) and f θ (right, i) = f θ ′ (left, j)} (cf. Figures
We now obtain B as the projection (to P) of the product B run ×B dep . One can show that the dependence graphs faithfully represent the causal dependencies created between the states of the TA assigned to the first and the last process of a pipeline. Thus, the join allows us to verify if the pipeline can be closed. ⊓ ⊔ Proof (of Theorem 4). Like for pipelines, we perform the constructions given in the proofs of Lemmas 2 and 3 on the fly. Since the graphs D θθ ′ , their composition, and their join can be computed in polynomial time, we still get a PSPACE procedure. For the lower bound, we again exploit PSPACE-hardness of intersection of finite automata. The adaptation to rings is straightforward. ⊓ ⊔

Conclusion

We showed that verification of PCAs running on pipelines, rings, and trees is decidable under certain context bounds. Our approach also yields decidability of all universal verification problems: Do all topologies accepted by a finite (tree) automaton allow for an accepting run of the given PCA? This involves complementation of finite (tree) automata. For future work, it will be worthwhile to consider model checking against temporal logics, and automata models that may run over topologies of unbounded degree such as stars and unranked trees.

A Proof of Lemma 1

Lemma 1. Let t ∈ {s⊕r1, intf}, k ≥ 1, and K = k • (|N | 2 + 2|N | + 1
). Let A = (P, Msg, (A p ) p∈P ) be a PCA such that L(A p ) ⊆ W (k,t) for all p ∈ P. Then, for all topologies T (over N and P), we have L K ( A T t ) = ∅ iff L (k,t) (A, T ) = ∅. Proof. We only consider the more difficult case of context type s⊕r1. The case intf follows the same lines (and we get a slightly better bound

K = k + (k • |N |)). So let, in the following, t = s⊕r1. Let k ≥ 1 and set K = k • (|N | 2 + 2|N | + 1
). Let A = (P, Msg, (A p ) p∈P ) be a PCA such that L(A p ) ⊆ W (k,t) for all p ∈ P. Moreover, fix a topology T = (V, ν, π) over N and P. The direction from cell transitions to PCA follows easily from the definitions. We will show

L (k,t) (A, T ) = ∅ =⇒ L K ( A T t ) = ∅ .
The rough idea is to consider an automata model that is able to execute both, PCA transitions and cell transitions, and to transform, step by step, all PCA transitions into cell transitions. To this aim, we define another finite automaton A T t := (S, =⇒ ∪ =⇒ t , ι, F ) over Σ T ∪ Γ where S, =⇒, ι, and F are as in [[A]] T and =⇒ t ⊆ S × Γ × S is as in A T t , i.e., Γ is the set of substructures of T that are cells.

For a word W = γ 1 . . . γ n ∈ (Σ T ∪ Γ ) * and a node u ∈ V , we define the projection of W to u as (γ

1 )| u • . . . • (γ n )| u ∈ (Σ ∪ {⊤}) * . Here, for C ∈ Γ , we let C| u = ⊤ if u is a node of C. Otherwise, C| u = ε.
The definition of contexts for words w ∈ (Σ ∪ {⊤}) * is the same as for words over Σ with one difference: one ocurrence of ⊤ is counted as one context. This naturally leads to an extended definition of (ℓ, t)-boundedness for words from (Σ T ∪ Γ ) * , for ℓ ≥ 1. We let L (ℓ,t) ( A T t ) denote the set of (ℓ, t)-bounded words that are accepted by A T t . An important property of L (ℓ,t) (A, T ), L (ℓ,t) ( A T t ), and L (ℓ,t) ( A T t ) is that they are closed under permutation of independent actions, which are executed by distinct sets of processes. We say that two actions γ, γ ′ ∈ Σ T ∪Γ are independent if loc(γ) ∩ loc(γ ′ ) = ∅, where loc( u, m, v ) = {u, v} and loc(C) is the set of nodes of C. Now, suppose W ∈ L (k,t) (A, T ), which implies W ∈ L (k,t) ( A T t ). Pick some ū ∈ V and a maximal, nonempty set I of positions in W that belong to (1) the first send context of ū, and (2) a nonempty uninterrupted receive context for each involved adjacent node of ū.

Suppose that the receiving processes are U ⊆ V . Moreover, let C be the cell induced by U ∪ {ū} in T . By reordering of independent actions, W is equivalent to some word W ′ = γ 1 . . . γ n ∈ L (k,t) ( A T t ) such that, for some i ≤ j, the infix γ i . . . γ j corresponds to the word induced by the positions I selected in W . Let s 0 s 1 . . . s n ∈ S * be an accepting run of A T t on W ′ . It follows from the definitions that s i-1 C = =⇒ t s j . Thus, s 0 . . . s i-1 s j . . . s n is an accepting run of A T t on W ′′ = γ 1 . . . γ i-1 C γ j+1 . . . γ n . Note that W ′′ is (k +1, t)-bounded, since we possibly split the send context and some receive contexts into two. Now, we choose the next send context on ū and so on. When there are no more send contexts on ū, then we found a word in L( A T t ) whose projection to ū consists of at most k + k • |N | contexts. Moreover, in the projection of each neighbor of ū, we created at most as many (i.e., k + k • |N |) new contexts. We now pick another node ū and so on, until all actions from Σ T were transformed into cell transitions and we end up in a word W ∈ L( A T t ) ∩ Γ * . Putting everything together, we obtain that W is (K, t)-bounded for

K = k + (k • |N |) + (|N | • (k + k • |N |)) = k • (|N | 2 + 2|N | + 1) .
The first summand in the term following K is for "old" contexts, the second summand is for new send contexts, and the third one for new receive contexts (this is why we have a factor |N |). Finally, since W consists of letters from Γ only, we have W ∈ L K ( A T t ). ⊓ ⊔ B Correctness Proof for Lemma 2

Let K = k • (|N | 2 + 2|N | + 1)
. By Lemma 1, it suffices to show that, for all acyclic topologies T over N and P, we have T ∈ L(G) iff L K ( A T t ) = ∅. Assume A T t = (S, =⇒ t , ι, F ), and let T = (V, ν, π) be an acyclic topology. We first show the direction "⇐=". Let W = C 1 . . . C n ∈ L K ( A T t ) and suppose ξ = s 0 s 1 . . . s n is an accepting run of A T t on W . For every i ∈ [n], we fix a center ūi of C i . Let us determine a run γ : V → S of G on T . For u ∈ V , we define γ(u) = (s 0 τ1 -→ s 1 τ2 -→ . . . τ K --→ s K ) as follows. First, s 0 = ι u . Suppose that s i is the j-th state in s 1 . . . s n such that u is a node of C i = (V ′ , ν ′ , π ′ ). Then, we let s j = s i | u . Moreover, τ j = a if ν ′ (u, a) = ūi . Finally, τ j = dom(ν ′ (u)) if u = ūi . The sequences are filled up to length K by ε-labels and repeating the last local state, respectively.

We show that γ is a run of G on T by verifying that, for every u ∈ V , the tuple (C, u, ρ) := cell (T , u, γ) is a transition of G. Note that (C, u, ρ) has to fulfill the properties (a)-(c) in the definition of ∆. Properties (a) and (b) follow directly from the definition of γ. For (c), the argument goes as follows: for all i ∈ [K] such that the i-th transition label of ρ(u) is τ i ⊆ N , there is j ∈ [n] such that τ i was induced by C j . Thus, there is a sub-cell D of C j as required in property (c). Now, we show "=⇒". Let γ : V → S be a run of G on T . This implies that, for every u ∈ V and every i ∈ [K] such that the i-th transition label of γ(u) is τ (u,i) ⊆ N , there is a sub-cell D (u,i) fulfilling (c) in the definition of G. Without loss of generality, we assume that all ε-labels in γ(u) are scheduled at the end.

Let D be the set of these sub-cells D (u,i) . 3 Moreover, let g : D × V ⇀ [K] be a partial mapping that associates with every node v of D (u,i) the corresponding transition j in γ(v). This mapping is well-defined, as for every n ∈ [K], θ ∈ S, and a ∈ N , there is at most one step j in θ such that f θ (a, j) = n and τ j = a.

Let ⊏ ⊆ D×D be defined as the least strict preorder satisfying D (u,i) ⊏ D (v,j) whenever D (u,i) and D (v,j) share a node v ′ such that g(D (u,i) , v ′ ) < g(D (v,j) , v ′ ). The restriction to acyclic topologies guarantees that (D, ⊏) is actually a (strict) partial-order relation. Let W = C 1 . . . C n be a linearization of (D, ⊏). By induction, we will show that W ∈ L( A T t ), which directly implies that W ∈ L K ( A T t ). As there cannot be a D ∈ D such that D ⊏ C 1 , we have g(C 1 , v) = 1 for all v in C 1 . Let s (u,i) denote the state in γ(u) reached after the i-th step. Then, there is a transition ι C1 = =⇒ t (s u ) u∈V in A T t where

s u = s (u,1) if u is a node of C 1 ι u otherwise
Now, assume that we constructed, for a strict prefix C 1 . . . C ℓ of W , a sequence of transitions in A T t of the form ι C1 = =⇒ t . . .

C ℓ = =⇒ t (s u ) u∈V .
By definition of (D, ⊏) and the assumption that W is a linearization, we have s u = s (u,j) for all nodes u of C ℓ+1 and j = g(C ℓ+1 , u) -1. This implies that there is a transition (s u ) u∈V

C ℓ+1 = = =⇒ t (s ′ u ) u∈V with s ′ u =
s (u,j ′ ) if u in C ℓ+1 and j ′ = g(C ℓ+1 , u) s u otherwise.

Obviously, after treating W completely, we end up in a final state of A T t , which proves W ∈ L( A T t ). We deduce L K ( A T t ) = ∅.

Fig. 3 .

 3 Fig. 1. Pipeline

Fig. 4 .Fig. 5 .

 45 Fig. 4. Undecidability for s1+r1

Fig. 6 .Fig. 7 .

 67 Fig. 6. Cell transitions wrt. s⊕r1

Fig. 8 .Fig. 9 .

 89 Fig. 8. Topology acceptor on a ring

  s K where K = 18k (due to the new definition of C --→ s⊕r1 ). First, we introduce dependence graphs. Let Ω = {⊲ 1 , . . . , ⊲ K } ∪ {⊳ 1 , . . . , ⊳ K }. A dependence graph is a graph D = (Ω, →, ∼) where →, ∼ ⊆ Ω × Ω with ∼ symmetric. The composition D 1 • D 2 of two graphs D 1 = (Ω, → 1 , ∼ 1 ) and D 2 =

Table 1 .

 1 Context-bounded nonemptiness problems and summary of results(P, Msg, (A p × B (k,t) ) p∈P ) where A p × B (k,t)is the classical product of two finite automata. It is easy to see that L (k,t) (A, T ) = L(A ′ , T ). This means that the context-bound restriction can be built into the PCA.Applying the definitions to the PCA A from Example 1, we have

We rather deal with a multiset. Several sub-cells may be identical, but we will still distinguish them. In other words, when we write D (u,i) , we actually mean (u, i), but we identify the pair with a cell, since it is convenient.