André Monin

Dynamic Estimation of Linear Systems Constrained by Bounds

Keywords: Speed estimation, Truncated Gaussian pdf, I, INTRODUCTION

This article deals with the minimum variance estimation of a Gaussian process constrained by bounds. A special truncated Gaussian probability is shown to be fairly well adapted to this ltering scheme as its set is linearly closed with respect to convolution and multiplication operations.

used in [START_REF] Simon | Kalman ltering with inequality constraints for turbofan engine health estimation[END_REF]. In [START_REF] Richards | Constrained Kalman ltering using pseudomeasurements[END_REF], the author extends the pseudomeasurement approach, used in the equality constraint case [START_REF] Tahk | Target tracking subject to kinematic constraints[END_REF], to the inequality case. Recall that the pseudomeasurement approach may lead to singularity of the ltering covariance matrix. Often, this singularity has to be arti cially regularized in the nonlinear case [START_REF] Geeter | A smoothly constrained Kalman lter[END_REF]. In [START_REF] Ungarala | Constrained extended Kalman lter for nonlinear state estimation[END_REF], the authors compute a maximum likelihood estimator under constraints using the Lagrangian multiplier tool. Note that it seems that the authors did not observe that this approach is close to the pseudo-measurement approach [START_REF] Tahk | Target tracking subject to kinematic constraints[END_REF]. Finally, in [START_REF] Rao | Constrained state estimation for nonlinear discrete-time systems: Stability and moving horizon approximations[END_REF], the authors employ online optimization using a moving horizon approximation and in [START_REF] Brankart | Optimal nonlinear ltering and smoothing assuming truncated Gaussian probability distributions in a reduced dimension space of adaptive size[END_REF], the author uses classical normalized truncated Gaussian probability density functions (pdf) which are approximated by random sampling. The main drawback of these two last approaches lies in their heavy computational costs.

Here, we suggest the use of a new pdf named Mirrored Gaussian pdf (MGP). It is shown that the MGP set is linearly closed with respect to convolution and multiplication operations. The Gaussian pdf properties are then exploited to derive a ltering algorithm based on Kalman ltering or extended Kalman ltering (EKF) nearby the so-called Gaussian sum lter (GSF) [START_REF] Sorenson | Recursive Bayesian estimation using Gaussian sums[END_REF]. As it is the case for GSF, one observes an increase in the number of MGP devoted to represent the optimal solution. This exponential growth can be reduced using the same kind of heuristics as those used in [START_REF] Sorenson | Recursive Bayesian estimation using Gaussian sums[END_REF] and [START_REF] Alspach | Nonlinear Bayesian estimation using Gaussian sum approximation[END_REF].

Let us consider a linear dynamic system x t 2 R n whose evolution is involved in the classical linear equations:

x t = F x t 1 + w t (1a) y t = Hx t + v t (1b)
where w t and v t are independent white noises and where y t stands for the output. If the noise w t pdf is Gaussian with variance Q = E w t w T t , the transition pdf of the state can be written

p (x t jx t 1 ) = (x t F x t 1 ; Q) (2)
where stands for the Gaussian pdf

(x; Q) , 1 p (2 ) n jQj exp 1 2 x T Q 1 x
Suppose now that one wants to make sure that the rst component of x t , say [x t ] 1 , remains positive for all x t 1 such that [x t 1 ] 1 > 0. The rst idea would be to consider the truncated Gaussian pdf de ned by

p (x t jx t 1 ) = (x t 1 ) I [[xt] 1 0] (x t F x t 1 ; Q)
where I [x>0] stands for the indicator function of the set fx > 0g and where (x t 1 ) is a scaling factor, depending obviously on the Gaussian pdf mean F x t 1 .

Unfortunately, the expression of (x t 1 ) is a little complicated and does not allow simple ltering computation, except for the static case (parameter estimation [START_REF] Monin | Minimum variance estimation of parameters constrained by bounds[END_REF]).

A better choice is accepting a minor distortion of the Gaussian pdf near zero (see Figure 1). This may be achieved by de ning the MGP as follows:

~ (x; x; P ) , I [[x] 1 0] ( (x x; P ) + (x + x; P )) (3)
It is easy to show that this pdf is really a normalized pdf (see Lemma 3 in the Appendix). Thus, let us replace the transition pdf, Expression (2), with the following MGP p (x t jx t 1 ) = ~ (x t ; F x t 1 ; Q)

In the same manner, assume that the rst component of the output y t is positive. One may de ne again the output pdf as a MGP as follows:

p (y t jx t ) = ~ (y t ; Hx t ; R) (4)

II. OPTIMAL FILTERING

A. The linear case

The MGP introduced in this paper has important properties. Indeed, the MGP set is closed with convolution and linearly closed with multiplication (see Appendix I). Recall that the optimal ltering goal is to compute the so-called a posteriori pdf of the state p (x t jy 0:t ) where y 0:t , fy 0 ; : : : ; y t g. Therefore, if the initial pdf of the state is a MGP, then the a posteriori pdf is a linear combination of MGPs.

Theorem 1: If at time t 1 the a posteriori pdf of the state is a weighted MGP sum with N t 1 terms as follows:

p (x t 1 jy 0:t 1 ) = Nt 1 X i=1 i t 1 ~ x t 1 ; xi t 1jt 1 ; P i t 1jt 1
(5) then, at time t, the a posteriori pdf is again a weighted MGP sum with 2 N t 1 terms de ned by

p (x t jy 0:t ) = Nt 1 X i=1 i;1 t ~ x t ; xi;1 tjt ; P i tjt + Nt 1 X i=1 i;2 t ~ x t ; xi;2 tjt ; P i tjt where xi tjt 1 = F xi t 1jt 1 (6a)
P i tjt 1 = F P i t 1jt 1 F T + Q (6b) xi;1 tjt = xi tjt 1 + K i t y t H xi tjt 1 (7a) xi;2 tjt = xi tjt 1 + K i t y t + H xi tjt 1 (7b) i tjt 1 = HP i tjt 1 H T + R (8a)
K i t = P i tjt 1 H T i tjt 1 1 (8b)
P i tjt = P i tjt 1 P i tjt 1 H T i tjt 1 1 HP i tjt 1 (8c) ~ i;1 t = i t 1 I [[yt] 1 >0] y t H xi tjt 1 ; i tjt 1 (9a) ~ i;2 t = i t 1 I [[yt] 1 >0] y t + H xi tjt 1 ; i tjt 1 (9b) i;1 t = ~ i;1 t P Nt 1 i=1 ~ i;1 t + ~ i;2 t i;2 t = ~ i;2 t P Nt 1 i=1 ~ i;1 t + ~ i;2 t
Proof: The so-called Chapman-Kolmogorov theorem applied to Equation (5) leads to

p (x t jy 0:t 1 ) = Z R n p (x t jx t 1 ) p (x t 1 jy 0:t 1 ) dx t 1 = Nt 1 X i=1 i t 1 Z R n ~ (x t ; F x t 1 ; Q) ~ x t 1 ; xi t 1jt 1 ; P i t 1jt 1 dx t 1
Corollary 5 allows one to rewrite this expression as follows:

p (x t jy 0:t 1 ) = Nt 1 X i=1 i t 1 ~ x t ; xi tjt 1 ; P i tjt 1
where

xi tjt 1 = F xi t 1jt 1 P i tjt 1 = F P i t 1jt 1 F T + Q
The correction is then obtained by using the Bayes rule, that is, omitting the scaling term:

p (x t jy 0:t ) / p (y t jx t ) p (x t jy 0:t 1 ) = Nt 1 X i=1 i t 1 ~ (y t ; Hx t ; R) ~ x t ; xi tjt 1 ; P i tjt 1
Lemma 4 then leads to the result.

Clearly, the number of MGP needed for the representation of the ltering solution grows exponentially with time, as it is the case in Gaussian sum ltering ( [START_REF] Sorenson | Recursive Bayesian estimation using Gaussian sums[END_REF] [START_REF] Alspach | Nonlinear Bayesian estimation using Gaussian sum approximation[END_REF]). Note that the MGP number increase is due to the correction step while the Gaussian number pdf increase is due to the prediction step when using the GSF technique.

As in the GSF case, one has to use approximations to reduce the increase in MGP number. The simplest technique consists of maintaining only the N max MGP with greatest weights i t and pruning the other MGPs, N max being the number of MGP well-matched with the computational power allocated to the application.

B. Computing the estimator

If at step t, the a posteriori pdf is , the same values that in the unconstrained case.

p (x t jy 0:t ) = Nt X i=1 i t ~

C. The nonlinear case

Suppose now that the dynamic system is nonlinear:

x t = f (x t 1 ) + w t y t = h (x t ) + v t
In this case, a very popular approximation is based on the linear approximation of functions f and h and leads to the so-called EKF. In our case, such an approximation is still relevant provided by the function h to be an odd function.

Theorem 2: If the function h is an odd function and if at time t 1 the a posteriori pdf of the state is a weighted MGP sum with N t 1 terms, Expression (5), then at time t the a posteriori pdf can be approximated by a weighted MGP sum with 2 N t 1 terms de ned by p (x t jy 0:t ) ' in Expressions ( 7) and ( 9) and nally H with the Jacobian of h evaluated at xi tjt 1 in Expression [START_REF] Monin | Minimum variance estimation of parameters constrained by bounds[END_REF].

III. SIMULATION RESULTS

To illustrate the relevance of such a ltering approach, let us consider the stereovision issue in a very simple case, that is, a mono-dimensional stereovision system. Recall that the classical range estimation of a salient point is achieved via disparity measurement, that is, the difference between the pixel location corresponding to the salient point on the two camera image planes. This disparity d t is then related to the range r t as follows:

d t = bf r t
where b stands for the distance between the two cameras and f is the focal distance of the lens. If f is expressed in pixel units, considering the measurement error equal to one pixel, the measurement may be modeled as follows:

y t = bf r t + v t
where f = N=2, N is the total number of pixels, and where v t is a Gaussian white noise with variance equal to unity. Recall that if the measurement y t < 0, the value is changed in y t = 0. Let us consider that the salient point speed (s t ) moves according to a rst order dynamic system. The range (r t ) evolution may be represented by the following equations:

r t = r t 1 + s t 1 t s t = ks t 1 + w t
where k = 0:95 refers to a friction factor and w t is Gaussian white noise with variance Q. t stands for the sampling period.

We then apply Theorem 2 to achieve the ltering of x t (it is clear that the output function is an odd function). The growth of the MGP number is treated by pruning MGPs with lowest weights and the total number of MGPs is xed to N max = 2 3 = 8. The distance between cameras is xed at b = 0:2 m and the pixel number at N = 640. The true initial range is equal to r 0 = 2 m and the initial pdf is de ned by p (r 0 ) = ~ (r 0 ; r 0 ; P 0 ) with r 0 = c=y 0 and p P 0 = 60 m. The measurement frequency is 1 Hz ( t = 1 s). The standard deviation of w t is set to 10 p t. Our ltering algorithm (MEKF) has been compared with the classical EKF, the algorithm including the projection utility suggested in [START_REF] Simon | Kalman ltering with inequality constraints for turbofan engine health estimation[END_REF] and [START_REF] Kandepu | Constrained state estimation using the unscented Kalman lter[END_REF] (CEKF) and the pseudo-measurement approach (PEKF) suggested in [START_REF] Ungarala | Constrained extended Kalman lter for nonlinear state estimation[END_REF]. Note that, for this example, the approaches in [START_REF] Tugnait | Constrained signal restoration via iterated extended Kalman ltering[END_REF] and [START_REF] Massicote | Incorporation of a positivity constraint into a Kalman-lter-based algorithm for correction of spectrometric data[END_REF] lead to the same results than the CEKF approach. A typical example of range and speed estimations is shown Figures 2 and3 respectively. Clearly, when the true range comes near zero, the EKF range estimator diverges when it locks on a negative value. It is then unable to go back to a positive estimate as it uses the Jacobian of 1=r, which has the wrong sign. In the same situation (true range near zero), the CEKF is unable to get away from zero as the speed estimation has the wrong sign. Finally, the PEKF range estimator remains zero until the real range reaches a value far from zero. On the other hand, our algorithm seems to be always ef cient, even near zero. Note that when the true range is far from zero and before any divergence, all lters are equivalent as they come down to the unconstrained EKF.

H ( ) being the Jacobian of the function h.

Proof: The development of the product is similar to that of Expression [START_REF] Simon | Kalman ltering with inequality constraints for turbofan engine health estimation[END_REF], just replacing Hx with h (x). The linearization of h (x) at the neighborhood of leads to

(y h (x) ; R) (x ; P ) ' (y h ( ) ; ( )) (x ( + K ( ) (y h ( )) ; B ( )))(14)
where , K and B are de ned by Expression [START_REF] Tahk | Target tracking subject to kinematic constraints[END_REF]. In the same manner, the second product of Expression ( 11) becomes

(y + h (x) ; R) (x + ; P ) ' (y + h ( ) ; ( )) (x ( + K ( ) (y h ( )) ; B ( ))) (15)
after linearization of h (x) at the neighborhood of . The function h being odd, the Jacobian H ( ) is even and ( ) = ( ), K ( ) = K ( ) and B ( ) = B ( ). Equations ( 14) and ( 15) can then be combined in

(y h ( ) ; ( )) ~ (x; + K ( ) (y h ( )) ; B ( ))
The same computation is applied to the second product.

= Z R + [x] 1 [x] 1 [ x] 1 ; [P ] 1 1 d [x] 1 + Z R + [x] 1 [x] 1 + [ x] 1 ; [P ] 1 1 d [x] 1 [x] 1 [ x] 1 ; P
+ 1 2 1 + erf [ x] 1 = q 2 [P ] 1 1 [ x] 1 1 2 1 erf [ x] 1 = q 2 [P ] 1 1 [ x] 1
which leads to the result.

Fig. 1 .

 1 Fig. 1. Example of the distorsion induced by the truncation.

Fig. 3 .

 3 Fig. 2. Range estimation

Corollary 7 : 8 : 1 [ 2 [P ] 1 1 [ x] 1

 781211 If h is an odd function, one has Z R n ~ (y; h (x) ; R) ~ (x; ; P ) dx ' ~ (y; h ( ) ; ( ))with ( ) = H ( ) P H ( ) T + Rwhere H is the Jacobian of h. Proof: The integration of Expression (12) leads directly to the result.Proposition The mean [x] 1 of the constrained state [x] 1 with pdf ~ (x; x; P ) has the following expression[x] 1 = 2 [P ] 1 x] 1 ; [P ] 1 1 + erf [ x] 1 =q Proof: The expectation of [x] 1 is de ned by[x] 1 , x; P ) dx

  1 1 being the marginal pdf of [x] 1 .

								Re-
	call that Z 1 0 x (x x; P ) dx =	p	1 2 P	Z 1 0	x exp	1 2	(x x) 2 =P
	Noting that
	x exp	1 2	(x x) 2 =P		= x exp	1 2	(x x) 2 =P
						P	d dx	exp	1 2	(x x) 2 =P
	an integration by part leads to
	Z 1	x (x x; P ) dx
	0 p 2 P 1 P p 2 P x = P ( x; P ) + = Z 1 0 exp exp 1 p 2 P 1 2 = P ( x; P ) + 1 2 1 + erf x= 1 (x x) 2 =P dx 2 1 (x x) 2 =P 0 x Z 1 exp 1 (x x) 2 =P dx 2 0 p 2P x
	Therefore
	[x] 1 = 2 [P ] 1

1 [ x] 1 ; [P ] 1 1

IV. CONCLUSION

A new pdf devoted to perform positive variables has been proposed here. This pdf appears to be is welladapted to ltering when one component of the variable to be estimated is assumed to be positive. A new ltering algorithm based on these pdfs has been proposed compared with EKF in an academic example. One should imagine an extension to constraints de ned by several bounds (an interval, for instance) provided to grow the Gaussian pdf number devoted to represent the MGP.

APPENDIX I TRUNCATED GAUSSIAN FORMULA

Lemma 3: The MGP de ned by Expression (3) is a normalized pdf.

Proof:

using the fact that (x; P ) = ( x; P ).

Lemma 4: The product of two truncated Gaussian pdf is a linear combination of truncated Gaussian pdfs:

Recall the classical Gaussian product formula usually used to compute the Kalman lter [START_REF] Jazwinski | Stochastic Processes and Filtering Theory[END_REF] (y Hx; R) (x ; P ) = (y H ; ) (x ( + K (y H ) ; B))

where

Let us take into account the rst two Gaussian pdf products of Expression [START_REF] Simon | Kalman ltering with inequality constraints for turbofan engine health estimation[END_REF]. Note that the second term is derived from the rst one by replacing y ! y and ! . Thus, one has


Benedikt Bollig
email: benedikt.bollig@ens-paris-saclay.fr

Alain Finkel
email: alain.finkel@ens-paris-saclay.fr

Amrita Suresh
email: amrita.suresh@ens-paris-saclay.fr

Bounded Reachability Problems are Decidable in FIFO Machines

Keywords: 2012 ACM Subject Classification Theory of computation FIFO machines, reachability, underapproximation, counter machines 1

The undecidability of basic decision problems for general FIFO machines such as reachability and unboundedness is well-known. In this paper, we provide an underapproximation for the general model by considering only runs that are input-bounded (i.e. the sequence of messages sent through a particular channel belongs to a given bounded language). We prove, by reducing this model to a counter machine with restricted zero tests, that the rational-reachability problem (and by extension, control-state reachability, unboundedness, deadlock, etc.) is decidable. This class of machines subsumes input-letter-bounded machines, flat machines, linear FIFO nets, and monogeneous machines, for which some of these problems were already shown to be decidable. These theoretical results can form the foundations to build a tool to verify general FIFO machines based on the analysis of input-bounded machines.

Introduction

Context. Asynchronous distributed processes communicating using First In First Out (FIFO) channels are being widely used for distributed and concurrent programming, and more recently, for web service choreographies. Since systems of processes communicating through (at least two) one-directional FIFO channels, or equivalently, machines having a unique control-structure with a single FIFO channel (acting as a buffer) simulate Turing machines, most properties, such as unboundedness of a channel, are undecidable for such systems [START_REF] Vauquelin | Automates a file[END_REF][START_REF] Brand | On communicating finite-state machines[END_REF][START_REF] Memmi | An introduction to fifo nets-monogeneous nets: A subclass of fifo nets[END_REF]. Reachability in FIFO machines. If one restricts to runs with B-bounded channels (the number of messages in every channel does not exceed B), then reachability becomes decidable for existentially-bounded and universally-bounded FIFO systems [START_REF] Genest | On communicating automata with bounded channels[END_REF]. When limiting the number of phases, the bounded-context reachability problem is in 2-EXPTIME, even for recursive FIFO systems [START_REF] La | Context-bounded analysis of concurrent queue systems[END_REF][START_REF] Heußner | Reachability analysis of communicating pushdown systems[END_REF]. For non-confluent topology, reachability is in EXPTIME for recursive FIFO systems with 1-bounded channels [START_REF] Heußner | Reachability analysis of communicating pushdown systems[END_REF]. The notion of k-synchronous computations was introduced in [START_REF] Bouajjani | On the completeness of verifying message passing programs under bounded asynchrony[END_REF]. Reachability under this restriction and checking ksynchronizability are both PSPACE-complete [START_REF] Di Giusto | On the k-synchronizability of systems[END_REF]. Reachability is in PTIME in half-duplex systems [START_REF] Cécé | Verification of programs with half-duplex communication[END_REF] with two processes (moreover, the reachability set is recognizable and effectively computable), but the natural extension to three processes leads to undecidability. Lossy FIFO systems (where the channels can lose messages) [START_REF] Parosh | Using forward reachability analysis for verification of lossy channel systems[END_REF][START_REF] Finkel | Decidability of the termination problem for completely specified protocols[END_REF] have been shown to be well-structured and have a decidable (but non-elementary) reachability problem [START_REF] Chambart | The ordinal recursive complexity of lossy channel systems[END_REF]. In [START_REF] Madhusudan | The tree width of auxiliary storage[END_REF][START_REF] Aiswarya | Verifying communicating multi-pushdown systems via split-width[END_REF], uniform criteria for decidability of reachability and model-checking questions are established for communicating recursive systems whose restricted architecture or communication mechanism gives rise to behaviours of bounded tree-width. Input-bounded FIFO machines. Many papers, starting in the 80s until today, have studied FIFO machines in which the input-language of a channel (i.e. the set of words that record the messages entering a channel) is included in the set Pref (w * 1 w * 2 . . . w * n ) of prefixes of a bounded language w * 1 w * 2 . . . w * n . We call this class of FIFO machines input-bounded. If the set of letters that may enter a channel c is reduced to a unique letter a c , then the input-language of c is included in a * c and this subclass trivially reduces to VASS and Petri nets [START_REF] Yu | Unboundedness detection for a class of communicating finite-state machines[END_REF]. Also note that, in general, the behaviour of those FIFO machines does not have bounded tree-width. Monogeneous FIFO nets [START_REF] Finkel | About monogeneous fifo Petri nets[END_REF][START_REF] Memmi | An introduction to fifo nets-monogeneous nets: A subclass of fifo nets[END_REF][START_REF] Finkel | Well-structured transition systems everywhere![END_REF] (input-languages of channels c are included in LF (u c v * c ) where u c , v c are two words associated with c) and linear FIFO nets [START_REF] Finkel | Simulation of linear fifo nets by Petri nets having a structured set of terminal markings[END_REF] (input-languages are included in Pref (a * 1 a * 2 . . . a * n ) where each a i is a letter and a i = a j iff i = j) both generalize Petri nets with still a decidable reachability problem. A variant of the reachability problem, the deadlock problem, is shown decidable for input-letter-bounded FIFO systems in [START_REF] Gouda | On deadlock detection in systems of communicating finite state machines[END_REF] by reducing to reachability for VASS, but the extension to general input-bounded machines was left open.

Flat machines are another subclass of input-bounded machines in which the language of their control-graph, considered as a finite automaton, is a bounded language. For flat FIFO machines, control-state reachability is NP-complete [START_REF] Esparza | A perfect model for bounded verification[END_REF]; this result has recently been extended to reachability, channel unboundedness, and other classical properties [START_REF] Finkel | Verification of flat FIFO systems[END_REF].

To the best of our knowledge, the decidability status of control-state reachability, reachability, deadlock, and termination was not known for input-bounded FIFO machines, which strictly include all the classes discussed above such as flat, input-letter-bounded, monogeneous, and linear FIFO machines (the last three types contain VASS and they are all incomparable). The unboundedness problem of input-bounded FIFO machines was shown decidable in [START_REF] Jéron | Testing for unboundedness of FIFO channels[END_REF] by using the well-structured concepts but with no extension to decidability of reachability.

Our contributions:

We solve a problem that was left open in [START_REF] Gouda | On deadlock detection in systems of communicating finite state machines[END_REF], the decidability of the reachability problem for input-bounded FIFO machines. We present a simulation of input-bounded FIFO machines by counter machines with restricted zero tests. The main idea is to associate a counter with each word in the bounded language, and to ensure that the counters are incremented and decremented in a way that corresponds to the FIFO order. Since we can have repeated letters, and ambiguities in the FIFO machine, we first need to construct a normal form of the FIFO machine. Furthermore, we ensure that for every run in the FIFO machine, we can construct an equivalent run in the counter machine and vice-versa.

As we actually solve the general rational-reachability problem, we can deduce the decidability of other verification properties like control-state reachability, deadlock, unboundedness, and termination. We unify various definitions from the literature, survey the (not well-known) results, and generalize them.

Semi-Linear Sets. A linear set X (of dimension d ≥ 1) is defined as a subset of N d for which there exist a basis b ∈ N d and a finite set of periods {p 1 , . . . , p m } ⊆ N d such that X = {b + m i=1 λ i p i | λ 1 , . . . , λ m ∈ N}. A semi-linear set is defined as a finite union of linear sets.

Transition Systems. A labeled transition system is a quadruple T = (S, A, →, init) where S is the (potentially infinite) set of configurations 1 , A is a finite alphabet, init ∈ S is the initial configuration, and → ⊆ S × A × S is the transition relation.

For s, s ∈ S, let s → s if s a -→ s for some a ∈ A. For w ∈ A * , we write s w -→ s if there is a w-labeled path from s to s . Formally, s ε -→ s if s = s , and s aw --→ s if there is t ∈ S such that s a -→ t and t w -→ s . We let Traces(T ) = {w ∈ A * | init w -→ s for some s ∈ S}. Given w ∈ A * , we let Reach T (w) = {s ∈ S | init w -→ s}. Moreover, for L ⊆ A * , Reach T (L) = w∈L Reach T (w) is the set of configurations that are reachable via a word from L. Finally, the reachability set of T is defined as Reach T = Reach T (A * ). We call T finite if Reach T is finite (and this is the case if S is finite). Otherwise, T is called infinite. FIFO Machines. We consider FIFO machines having a sequential control graph rather than systems of communicating processes that are distributed systems. It is clear that, given a distributed system, one may compute the Cartesian product of all processes to obtain a FIFO machine (the converse is not always true).

Definition 2.

A FIFO machine is a tuple M = (Q, Ch, Σ, T, q 0 ) where Q is a finite set of control states, q 0 ∈ Q is an initial control state, and Ch is a finite set of channels. Moreover, Σ is a finite message alphabet. It is partitioned into Σ = c∈Ch Σ c where Σ c contains the messages that can be sent through channel c. Finally,

T ⊆ Q × A M × Q is a transition relation where A M = { c!a | c ∈ Ch and a ∈ Σ c } ∪ { c?a | c ∈ Ch and a ∈ Σ c }
is the set of send and receive actions.

Example 3 (Connection-Deconnection Protocol). A model for the (simplified) connectiondeconnection protocol, CDP, between two processes is described as follows (see Figure 1): We model the protocol with two automata (representing the two processes) and two (infinite) channels. The first processes (on the left) can open a session (this is denoted by sending the message "a" through channel c 1 to the other process). Once a session is open, the first process can close it (by sending message "b" to the other process), or on the demand of the second process (if it receives the message "e"). This protocol has been studied in [START_REF] Thierry | Testing for unboundedness of FIFO channels[END_REF].

In the example, it is natural to have two separate processes. However, following Definition 2, we formalize this in terms of the Cartesian product of the two processes. That is, the CDP is modeled as the FIFO machine M = (Q, Ch, Σ, T, q 0 ) where Q = {0, 1} × {0, 1} (the Cartesian product of the local state spaces) with initial state q 0 = (0, 0), Ch = {c 1 , c 2 }, Σ = Σ c1 Σ c2 with Σ c1 = {a, b} and Σ c2 = {e}. Moreover, the transition relation T contains, amongst others, ((0, 0), c 1 !a , (1, 0)) and ((1, 0), c 1 ?a , (1, 1)). 0 1 A FIFO machine M = (Q, Ch, Σ, T, q 0 ) induces a (potentially infinite) transition system

c 1 c 2 0 1 c 1 !a c 1 !b c 2 ?e c 1 ?a c 1 ?b c 2 !e
T M = (S M , A M , → M , init M ). Its set of configurations is S M = Q× c∈Ch Σ * c .
In (q, w) ∈ S M , the first component q denotes the current control state and w = (w c ) c∈Ch determines the contents w c ∈ Σ * c for every channel c ∈ Ch. The initial configuration is init M = (q 0 , ε) where ε = (ε, . . . , ε), i.e., every channel is empty. The transitions are given as follows:

(q, w)

c!a ---→ M (q , w ) if (q, c!a , q ) ∈ T , w c = w c • a, and w d = w d for all d ∈ Ch \ {c}; (q, w) c?a ---→ M (q , w ) if (q, c?a , q ) ∈ T , w c = a • w c ,
((0, 0), (ε, ε)) c1!a ----→ ((1, 0), (a, ε)) c1?a ----→ ((1, 1), (ε, ε)) c2!e ---→ ((1, 0), (ε, e)).
As for the reachability set, we have, e.g., ((1, 1), ((ba) * , ε))) ⊆ Reach M and ((0, 0), (b(ab) * , e)) ⊆ Reach M . Let us remark that CDP is not half-duplex because there are reachable configurations with both channels non-empty, e.g., ((0, 0), (b, e)); moreover, it is neither monogeneous, nor linear, nor input-letter-bounded.

Counter Machines. We next recall the notion of counter machines, where multiple counters can take non-negative integer values, be incremented and decremented, and be tested for zero (though in a restricted fashion). Definition 5. A counter machine (with zero tests) is a tuple C = (Q, Cnt, T, q 0 ). Like in a FIFO machine, Q is the finite set of control states and q 0 ∈ Q is the initial control state.

Moreover, Cnt is a finite set of counters and T ⊆

Q × A C × Q is the transition relation where A C = {inc(x), dec(x) | x ∈ Cnt} × 2 Cnt .
The counter machine C induces a transition system T C = (S C , A C , → C , init C ) with set of configurations S C = Q×N Cnt . In (q, v) ∈ S C , q is the current control state and v = (v x ) x∈Cnt represents the counter values. The initial configuration is init C = (q 0 , 0) where 0 maps all counters to 0. For op ∈ {inc, dec}, x ∈ Cnt, and Z ⊆ Cnt (the counters tested for zero), there is a transition (q, v)

(op(x),Z) ------→ C (q , v ) if (q, (op(x), Z), q ) ∈ T , v y = 0 for all y ∈ Z (applies the zero tests), v x = v x + 1 if op = inc and v x = v x -1 if op = dec, and v y = v y for all y ∈ Cnt \ {x}.
The reachability set of C is defined as

Reach C = Reach T C . For L ⊆ A * C , we also let Reach C (L) = Reach T C (L). Moreover, Traces(C) = Traces(T C ).
To get decidability of reachability in counter machines, we impose the restriction that, once a counter has been tested for zero, it cannot be incremented or decremented anymore. This is clearly an extension of VASS. To define this, let L zero C be the set of words (op 1 (x 1 ), Z 1 ) . . .

(op n (x n ), Z n ) ∈ A *
C such that, for every two positions 1 ≤ i ≤ j ≤ n, we have x j ∈ Z i .

Theorem 6. The following problem is decidable (though inherently non-elementary): Given a counter machine

C = (Q, Cnt, T, q 0 ), a regular language L ⊆ A * C , a control state q ∈ Q, and a semi-linear set V ⊆ N Cnt , do we have (q, v) ∈ Reach C (L zero C ∩ L) for some v ∈ V ?
Proof sketch. Reachability in presence of a semi-linear target set and restricted zero tests straightforwardly reduces to configuration-reachability in counter machines without zero tests (i.e., VASS and Petri nets). The latter is decidable [START_REF] Mayr | An algorithm for the general petri net reachability problem[END_REF], though inherently non-elementary [START_REF] Czerwinski | The reachability problem for petri nets is not elementary[END_REF]. First, zero tests are postponed to the very end of an execution and, to this aim, stored in the control-state. Second, to check whether a counter valuation is contained in V , we can branch, whenever we are in the given control-state q, into a new component that decrements counters accordingly and eventually checks whether they are all zero.

3

The Input-Bounded Rational-Reachability Problem

It is very well known that the following reachability problem is undecidable: Given a FIFO machine M = (Q, Ch, Σ, T, q 0 ), a configuration (q, w) ∈ S M , and a regular language L ⊆ A * M , do we have (q, w) ∈ Reach M (L)? Of course, the problem is already undecidable when we impose L = A * M . Motivated by this negative result, we are looking for language classes C that render the problem decidable under the restriction that L ∈ C.

We say that a FIFO machine M = (Q, Ch, Σ, T, q 0 ) has a bounded reachability set if there is a tuple (L c ) c∈Ch of regular bounded languages L c ⊆ Σ * c such that, for all (q, w) ∈ Reach M , we have w ∈ c∈Ch L c . We observe that restricting the reachability set to be bounded is not sufficient to obtain a decidable reachability problem. We show this by simulating any two counter Minsky machine by a FIFO machine with fixed languages L c .

Theorem 7. The reachability problem is undecidable for FIFO machines with a (given) bounded reachability set.

We therefore consider a different restriction to obtain decidability. For a given FIFO machine M = (Q, Ch, Σ, T, q 0 ), we are interested in Reach M (L) where L ⊆ A * M is inputbounded in the following sense: For every channel c, the sequence of messages that are sent through channel c is from a given regular bounded language L c ⊆ Σ * c .

Let us be more formal. For c ∈ Ch, we let proj c! : A * M → Σ * c be the homomorphism defined by proj c! ( c!a ) = a for all a ∈ Σ c , and proj c! (β) = ε if β ∈ A M is not of the form c!a for some a ∈ Σ c . We define proj c? :

A * M → Σ * c accordingly. With this, given a tuple ℒ = (L c ) c∈Ch of bounded languages L c ⊆ Σ * c , we set ℒ ! = {σ ∈ A * M | proj c! (σ) ∈ L c for all c ∈ Ch} and ℒ ? = {σ ∈ A * M | proj c? (σ) ∈ L c
for all c ∈ Ch}. We observe that, if all L c are regular, then so are ℒ ! and ℒ ? . Definition 8. The input-bounded (IB) reachability problem asks whether a given configuration (q, w) is reachable along a sequence of actions from ℒ ! , i.e., whether (q, w) ∈ Reach M (ℒ ! ).

Note that, if (q 0 , ε) σ -→ M (q, w) and σ ∈ ℒ ! , then we also have σ ∈ Pref (ℒ ? ) due to the FIFO policy. Thus, Reach M (ℒ ! ) = Reach M (ℒ ! ∩ Pref (ℒ ? )) so that we can restrict to action sequences from ℒ ! ∩ Pref (ℒ ? ). We will call ℒ ! ∩ Pref (ℒ ? ) the set of valid words.

Example 9. Let us come back to the protocol CDP M from Example 3 and Figure 1, which is neither monogeneous nor linear nor flat. Since the "input-languages" of the two channels (i.e. the languages of words that record the messages entering a channel) contain {a, ab} * and e * , resp., and since {a, ab} * is not a bounded language, we have Traces(M ) ⊆ ℒ ! for every pair of bounded languages ℒ. In other words, M is not input-bounded. However, when we look at the reachability set obtained by considering the tuple of bounded languages ℒ = (L c1 , L c2 ) where L c1 = (ab) * (a + ε)(ab) * is a bounded language over (ab, a, ab), and L c2 = e * is a bounded language over (e), we still obtain the entire reachability set. That is, we have Reach M = Reach M (ℒ ! ). Hence, even though the input-languages of the system are not all bounded, we can still compute the reachability set by restricting our exploration to a tuple of (regular) bounded languages ℒ.

Actually, instead of reachability of a single configuration as stated in Definition 8, we study a more general problem, called the input-bounded rational-reachability problem. It asks whether a configuration (q, w) is reachable for some channel contents w from a given rational relation. So let us define rational relations.

Rational and Recognizable Relations. Consider a relation ℛ ⊆ c∈Ch Σ * c . We say that ℛ is rational if there is a regular word language R ⊆ Θ * over the alphabet Θ = c∈Ch (Σ c ∪ {ε})

such that ℛ = {(a 1 c • . . . • a n c ) c∈Ch | a 1 . . . a n ∈ R with n ∈ N and a i = (a i c ) c∈Ch ∈ Θ for i ∈ {1, . . . , n}}. Here, a 1 c • . . . • a n c ∈ Σ * c
is the concatenation of all a i c ∈ Σ c ∪ {ε} while ignoring the neutral element ε. For example, in the presence of two channels,

ℛ = {(a m , b n ) | m ≥ n} is a rational relation, witnessed by R = ((a, b) + (a, ε)) * .
In the following, we will always assume that a rational relation is given in terms of a finite automaton for the underlying regular language R.

A relation ℛ ⊆ c∈Ch Σ * c is called recognizable if it is the finite union of relations of the form c∈Ch R c where all R c ⊆ Σ * c are regular languages. Note that every recognizable relation is rational while the converse is, in general, false.

We define the Parikh image of a relation

ℛ ⊆ c∈Ch Σ * c as Parikh(ℛ) = {(π a ) a∈Σ ∈ N Σ | ∃w = (w c ) c∈Ch ∈ ℛ : π a = |w c | a for all c ∈ Ch and a ∈ Σ c }. It is well known that, if ℛ is rational, then Parikh(ℛ) is semi-linear.
For more background on rational relations and their subclasses, we refer to [START_REF] Berstel | Transductions and context-free languages[END_REF]10].

The IB Rational-Reachability Problem. We are now prepared to define the input-bounded (IB) rational-reachability problem and to state its decidability:

Definition 10. The IB rational-reachability problem is defined as follows: Given a FIFO machine M = (Q, Ch, Σ, T, q 0 ), a tuple ℒ = (L c ) c∈Ch of non-empty regular bounded languages L c ⊆ Σ * c (each given in terms of a finite automaton), a control state q ∈ Q, and a rational relation ℛ ⊆ c∈Ch Σ * c . Do we have (q, w) ∈ Reach M (ℒ ! ) for some w ∈ ℛ?

Theorem 11. IB rational-reachability is decidable for FIFO machines.

The remainder of this section is devoted to the proof of Theorem 11.

Let M = (Q, Ch, Σ, T, q 0 ) and let ℒ = (L c ) c∈Ch be a tuple of non-empty regular bounded languages L c ⊆ Σ * c over (w c,1 , . . . , w c,nc ). We proceed by reduction to counter machines. The rough idea is to represent the contents of channel c in terms of several counters, one for every component w c,i . To have a faithful simulation, we rely on a normal form of M and its bounded languages, which can be achieved at the expense of an exponential blow-up of the FIFO machine. Definition 12. We say that M and ℒ are in normal form if the following hold:

1. For all c ∈ Ch, Σ c ⊆ Alph(L c ) and L c is distinct-letter. 2. We have Traces((Q, A M , T, q 0 )) ⊆ Pref (V) where V = ℒ ! ∩ Pref (ℒ ? ). Note that (Q, A M , T, q 0
) is the finite transition system induced by the control graph of M .

Given a FIFO machine M = ( Q, Ch, Σ, T , q0 ) and the tuple L = ( Lc ) c∈Ch of nonempty regular bounded languages Lc ⊆ Σ * c , we now construct M = (Q, Ch, Σ, T, q 0 ) and ℒ = (L c ) c∈Ch in normal form such that a reachability query in the former can be transformed into a reachability query in the latter (made precise in Lemma 15 below). We determine the language L c over (a 1 a 2 , a 3 ) (omitting the superscript c in the letters). The homomorphism

Distinct-Letter

h c : {a 1 , a 2 , a 3 } * → {a, b} * is given by h c (a 1 ) = a and h c (a 2 ) = h c (a 3 ) = b. We have h -1 c ( Lc ) = (a 1 (a 2 + a 3 )) * (a 2 + a 3 )(a 2 + a 3 ) * , which we intersect with (a 1 a 2 ) * a * 3 .
We thus get the regular bounded language L c = (a 1 a 2 ) * a 3 a * 3 over (a 1 a 2 , a 3 ). All letters from {a 1 , a 2 , a 3 } occur in L c so that we are done.

Trace Property. In the next step, we build the FIFO machine

M = (Q, Ch, Σ, T, q 0 ) such that Traces((Q, A M , T, q 0 )) ⊆ Pref (V) with V = ℒ ! ∩ Pref (ℒ ?
). First, to take care of the homomorphisms h c , we define the transition relation h

-1 ( T ) = {(q, c!ℯ , q ) | (q, c!a , q ) ∈ T and ℯ ∈ h -1 c (a)} ∪ {(q, c?ℯ , q ) | (q, c?a , q ) ∈ T and ℯ ∈ h -1 c (a)}. Thus, the set of actions of M will be A M = { c!ℯ | c ∈ Ch and ℯ ∈ Σ c } ∪ { c?ℯ | c ∈ Ch and ℯ ∈ Σ c }.
To continue our above example, a transition (q, c!b , q ) would be replaced with the two transitions (q, c!a 2 , q ) and (q, c!a 3 , q ), and similarly for (q, c?b , q ).

q 0 q 1 M Lc = (ab) * bb * L c = (a 1 a 2 ) * a 3 a * 3 !a | !b | ?a ?b ?b q 0 q 1 h -1 ( M ) M L R A for V = ℒ ! ∩ Pref (ℒ ? ) M L R !a 1 | !a 2 | !a 3 | ?a 1 ?a 2 | ?a 3 ?a 2 | ?a 3 !a 1 !a 2 !a 3 !a 3 ?a 1 ?a 2 ?a 3 ?a 3 q 0 L,M M q 0 M,M q 0 R,M q 1 R,R q 0 L,L q 0 M,L q 0 R,L q 1 R,M !a 1 !a 2 !a 1 !a 2 ?a 1 !a 3 !a 3 ?a 1 ?a 1 !a 3 !a 3 ?a 3 ?a 2 ?a 3 ?a 3 q 0 L,M C q 0 M,M q 0 R,M q 1 R,R q 0 L,L q 0 M,L q 0 R,L q 1 R,M inc(x) inc(x) inc(x) inc(x) dec(x) inc(y) inc(y) dec(x) dec(x) inc(y) inc(y) dec(y) x = 0 dec(x) dec(y) x = 0 dec(y) x = 0
Figure 2 For a FIFO machine M with a single channel c and the bounded language Lc = (ab) * bb * over (ab , b) (top leftmost), we construct a FIFO machine M (bottom left), together with Lc = (a1a2) * a3a * 3 , in normal form as the product of h -1 ( M ) and an automaton for V (top right). From M , we then obtain the counter machine C (bottom right).

To guarantee trace inclusion in Pref (V), we will consider a deterministic (not necessarily complete) finite automaton

A = (Q A , A M , T A , q 0 A , F A ), with set of final states F A ⊆ Q A , whose language is L(A) = V
and where, from every state, a final state is reachable in the finite graph (Q A , T A ). With this, we define M as the product of the FIFO machine h -1 ( M ) = ( Q, Ch, Σ, h -1 ( T ), q0 ) and A in the expected manner. In particular, the set of control states of M is Q × Q A , and its initial state is the pair (q 0 , q 0 A ).

Example 14. Figure 2 illustrates the result of the normalization procedure for a FIFO machine M with one single channel c (which is therefore omitted) and its bounded language Lc = (ab) * bb * over (ab , b). Recall from Example 13 that the corresponding homomorphism h c maps a 1 to a and both a 2 and a 3 to b, and that we obtain L c = (a 1 a 2 ) * a 3 a * 3 . Moreover, M is the product of h -1 ( M ) (depicted in the top center) and a finite automaton A for V = ℒ ! ∩ Pref (ℒ ? ) (obtained as the shuffle of the two finite automata on the top right). The state names in M reflect the states of M and A they originate from. We depict only accessible states of M from which we can still complete the word read so far to a word in V. For example, (q 1 , M, L) and (q 1 , L, R) would no longer allow us to reach the final state R of the ℒ ! -component. Now suppose we are given a reachability query for M in terms of q ∈ Q and a rational relation R ⊆ c∈Ch Σ * c . The lemma below shows how to reduce it to a reachability query in M . Here, for w

= (w c ) c∈Ch ∈ c∈Ch Σ * c , we define h(w) = (h c (w c )) c∈Ch ∈ c∈Ch Σ * c . Note that h -1 ( R) is rational. Lemma 15. We have (q, ŵ) ∈ Reach M ( L! ) for some ŵ ∈ R iff ((q, q A ), w) ∈ Reach M (ℒ ! ) for some q A ∈ Q A and w ∈ h -1 ( R).

Reduction of Normal Form to Counter Machine

Henceforth, we suppose that M = (Q, Ch, Σ, T, q 0 ) and ℒ = (L c ) c∈Ch are in normal form, where L c is a bounded language over (w c,1 , . . . , w c,nc ). In particular, for every letter a ∈ Σ c , there is a unique index i ∈ {1, . . . , n c } such that a ∈ Σ c,i where Σ c,i = Alph(w c,i ). We denote this index i by i a .

We build a counter machine C such that the IB rational-reachability problem for M can be solved by answering a reachability query in C, using Theorem 6. Each run in C will simulate a run in M . In particular, we want a configuration of C to allow us to draw conclusions about the simulated configuration in M . The difficulty here is that counter values are just natural numbers and a priori store less information than channel contents with their messages. To overcome this, the idea is to represent each word w c,i of a tuple (w c,1 , . . . , w c,nc ) as a counter x (c,i) . Since the set of possible action sequences is "guided" by a bounded language, we can replace send actions with increments and receive actions with decrements. More precisely, c!a becomes (inc(x (c,ia) ), ∅), thus incrementing the counter associated with the unique word w c,i in which a occurs. Similarly, c?a translates to (dec(x (c,ia) ), Z) (for suitable Z).

This alone does not put us in a position yet where, from a counter valuation, we can infer a unique channel contents. However, when we additionally keep track of the last messages that have been sent for each channel, we can reconstruct a unique channel contents.

There is one more thing to consider here. While the counters x (c,i) for a given channel c are kind of independent, the FIFO policy would not allow us to receive a letter from w c,j while a letter from w c,i with i < j is in transit. Translated to the counter setting, this means that performing dec(x (c,j) ) should require all counters x (c,i) with i < j to be 0, so this is where zero tests come into play. As the L c are bounded languages and thanks to the normal form, however, a counter that has been tested for zero does not need to be modified anymore.

We can directly implement these ideas formally and define C = (Q, Cnt, T , q 0 ) as follows (note that Q and q 0 remain unchanged):

The set of counters is Cnt = {x (c,i) | c ∈ Ch and i ∈ {1, . . . , n c }}.

For every (q, c!a , q ) ∈ T , we have (q, (inc(x (c,ia) ), ∅), q ) ∈ T .

For every (q, c?a , q ) ∈ T , we have (q, (dec(x (c,ia) ), Z), q ) ∈ T where the set of counters to be tested for zero is

Z = {x (c,j) | j < i a }.
Example 16. Figure 2 illustrates the construction of C from a FIFO machine M in normal form (cf. Example 14). Recall that we have one channel c and the bounded language L c = (a 1 a 2 ) * a 3 a * 3 over (a 1 a 2 , a 3 ). Thus, C will have two counters, say x for a 1 a 2 and y for a 3 . Note that performing dec(y) indeed comes with a test of x for zero.

Let us first observe that it is actually important that the FIFO machine satisfies the trace property. Suppose that, rather than from M , we constructed the counter machine directly from h -1 ( M ). Then, configuration (q 1 , (1, 0)) would be reachable in the counter machine via inc(x)inc(x)dec(x), which arises from c!a 1 c!a 2 c?a 2 . However the only corresponding trace from Pref (V) is c!a 1 c!a 2 c?a 1 , which in the FIFO machine h -1 ( M ) leads to q 0 . So consider M and its counter machine C. A channel contents w ∈ Σ * c (here, we have one channel) has a natural counter analogue ⟪w⟫ = (|w| a1 + |w| a2 , |w| a3 ). In fact, if (q, w) is reachable in M , then following the corresponding transitions in C will lead us to (q, ⟪w⟫). For example, ((q 0 , R, L), a 2 a 3 a 3 ) is reachable in M along the trace c!a 1 c!a 2 c?a 1 c!a 3 c!a 3 , and so is ((q 0 , R, L), (1, 2)) in C along inc(x)inc(x)dec(x)inc(y)inc(y) (all zero tests are empty).

But how about the converse? In general, one may associate with a counter valuation such as (4, 0) several channel contents. Actually, both a 1 a 2 a 1 a 2 and a 2 a 1 a 2 a 1 seem suitable. However, if we know the most recent message that has been sent, say a 1 , then this leaves only one option, namely a 2 a 1 a 2 a 1 . In this way, we can associate with each counter valuation v and message a i ∈ Σ c a unique (if it exists at all) possible channel contents v ai . Suppose that τ is a trace in C arising from a trace σ in M whose last sent message is a i . If (q, v) is reachable in C via τ , then (q, v ai ) is reachable in M via σ. For example, τ = inc(x)inc(x)dec(x) allows us to go to configuration ((q 0 , M, L), (1, 0)). It arises from σ = c!a 1 c!a 2 c?a 1 ∈ Pref (V), whose last sent message is a 2 . We have (1, 0) a2 = a 2 . Indeed, σ leads to ((q 0 , M, L), a 2 ).

Relation between FIFO Machine and Counter Machine

Recall that the FIFO machine M = (Q, Ch, Σ, T, q 0 ) and ℒ = (L c ) c∈Ch are in normal form, where L c is a bounded language over (w c,1 , . . . , w c,nc ). Let C = (Q, Cnt, T , q 0 ) be the associated counter machine. We will now formalize the tight forth-and-back correspondence that allows us to solve reachability queries in M in terms of reachability queries in C.

We start with a simple observation concerning the traces of M and C. Conversely, we will associate, with counter values and traces of C the corresponding objects in the FIFO machine. Because of the inherent ambiguity, this is, however, less straightforward. First, we define a partial mapping . : A * C → A * M (that is not a homomorphism). For τ ∈ A * C , we let τ be the unique (if it exists) word σ ∈ Pref (V) such that ⟪σ⟫ = τ . Next, we associate with a counter valuation a corresponding channel contents. As explained above, there is no unique choice unless we make an assumption on the last messages that have been sent. For c ∈ Ch, we set Σ ⊥ c = Σ c {⊥}. Let a ∈ Σ ⊥ c and w ∈ Σ * c . We say that a is good for w if w ∈ Infix(L c ) and either w = ε or w = u.a for some u ∈ Σ * c . Intuitively, it may be possible to obtain contents w in channel c when a is the last message sent (no message was sent yet through c if a = ⊥). Note that the set of words w ∈ Σ * c such that a is good for w is a regular language. Moreover, with w ∈ c∈Ch Σ * c , we associate the finite set G(w) ⊆ c∈Ch Σ ⊥ c of tuples a = (a c ) c∈Ch such that, for all c ∈ Ch, a c is good for w c . Let v ∈ N Cnt and a ∈ c∈Ch Σ ⊥ c . Abusing notation, we will associate with v and a the channel contents v a ∈ c∈Ch Σ * c (if it exists). We let v a = w if ⟪w⟫ = v and a ∈ G(w). There is at most one such w so that this is well-defined. Note that ⟪ v a ⟫ = v.

Example 18. If we have one channel c and our bounded language is L c = (a 1 a 2 a 3 ) * (a 4 ) * , then (4, 0) a2 = a 2 a 3 a 1 a 2 and (2, 1) a4 = a 2 a 3 a 4 , whereas [START_REF] Bardin | FAST: Acceleration from theory to practice[END_REF][START_REF] Parosh | Using forward reachability analysis for verification of lossy channel systems[END_REF]

a3 is undefined. Moreover, G(a 2 a 3 ) = {a 3 } and G(ε) = {a 1 , a 2 , a 3 , a 4 , ⊥}.
Given v and a, we can easily compute v a since there are only finitely many words w for a given v such that ⟪w⟫ = v. Furthermore, we can also compute G(w) for a given w as we have finitely many possibilities of a.

Finally, for a ∈ c∈Ch Σ ⊥ c , we let L last a ⊆ A * M be the set of words σ such that, for all c ∈ Ch, a c is the last message sent to c in σ (no message was sent if a c = ⊥). We are now ready to state that runs in the FIFO machine are faithfully simulated by runs in the counter machine (the proof is by induction on the length of the trace):

Proposition 19. Let σ ∈ A * M .
For all (q, w) ∈ S M and a ∈ c∈Ch Σ ⊥ c such that σ ∈ L last a , we have: (q 0 , ε) σ -→ M (q, w) =⇒ (q 0 , 0) ⟪σ⟫ --→ C (q, ⟪w⟫) and a ∈ G(w) .

Conversely, we can show that runs of the counter machine can be retrieved in the FIFO machine (again, the proof proceeds by induction on the length of the trace):

Proposition 20. Let τ ∈ A * C . For all (q, v) ∈ S C and a ∈ c∈Ch Σ ⊥ c such that τ ∈ ⟪Pref (V) ∩ L last a ⟫, we have: (q 0 , 0) τ -→ C (q, v) =⇒ (q 0 , ε) τ --→ M (q, v a ) .
From Propositions 19 and 20 and Lemma 17, we obtain the following corollary.

Corollary 21. For all (q, w) ∈ S M , we have:

(q, w) ∈ Reach M (ℒ ! ) ⇐⇒ (q, ⟪w⟫) ∈ Reach C (L zero C ∩ ⟪V ∩ a∈G(w) L last a ⟫) .
From Theorem 6, we know that verifying whether (q, ⟪w⟫)

∈ Reach C (L zero C ∩ L) where L = ⟪V ∩ a∈G(w) L last
a ⟫ is decidable. Hence, we can already deduce decidability of the (configuration-)reachability problem. In fact, using Propositions 19 and 20, we can solve the more general IB rational-reachability problem. For this, it is actually enough to check, in the counter machine, the reachability of a counter value that belongs to a semi-linear set. For a ∈ c∈Ch Σ ⊥ c and a rational relation

ℛ ⊆ c∈Ch Σ * c , let V a (ℛ) = {v ∈ N Cnt | v a ∈ ℛ}. Lemma 22. The set V a (ℛ) is effectively semi-linear.
Using this property, we finally reduce the IB rational-reachability problem to a reachability problem in counter machines: Corollary 23. For every q ∈ Q, we have:

(q, w) ∈ Reach M (ℒ ! ) for some w ∈ ℛ ⇐⇒ (q, v) ∈ Reach C (L zero C ∩ ⟪V ∩ L last a ⟫) for some a ∈ c∈Ch Σ ⊥ c and v ∈ V a (ℛ) .
By Theorem 6, we can now deduce Theorem 11, i.e., decidability of IB rational-reachability.

Reachability, Deadlock, Unboundedness, and Termination

We now address some other commonly studied reachability problems, which, as it turns out, can be reduced to the IB rational-reachability problem studied in the previous section.

A configuration (q, w) of a FIFO machine M is a deadlock if there is no (q , w ) such that (q, w) → M (q , w ).

Definition 24 (IB decision problems). Given a FIFO machine

M = (Q, Ch, Σ, T, q 0 ), a control-state q ∈ Q, a configuration s ∈ S M ,

Reachability and Deadlock

In [START_REF] Finkel | Verification of flat FIFO systems[END_REF], it was shown that reachability reduces to control-state reachability for flat FIFO machines but the converse is not true. However, using the same reductions as in [START_REF] Finkel | Verification of flat FIFO systems[END_REF], we obtain the following results: Proposition 25. IB reachability is (a) recursively equivalent to IB control-state reachability for FIFO machines, and (b) recursively reducible to IB deadlock for FIFO machines.

If, for a given q ∈ Q, we set ℛ to be the universal relation c∈Ch Σ * c , IB rationalreachability captures IB control-state reachability, and if we set ℛ = {w}, we can decide if the configuration (q, w) is reachable. In order to reduce IB deadlock to IB rationalreachability, we first explore the control states in order to find the set of states Q ⊆ Q which allow only receptions (no control states with sends can be part of a deadlock). This set can easily be computed from the set of transitions of the machine. Then, for each q ∈ Q , we can see if there exists a reachable configuration (q, w) such that, for all c, we have

w c ∈ K c = {ε} ∪ {a.u | u ∈ Σ *
c and a ∈ Σ c such that there is no transition (q, c?a , q ) in M }. Note that ℛ q = c∈Ch K c is recognizable and, therefore, rational. Furthermore, if there exists such a reachable (q, w) with w ∈ ℛ q , then it is a deadlock. Hence, using the fact that generalized IB rational-reachability is decidable (Theorem 11), we immediately deduce the following corollary:

Corollary 26. The problems IB reachability, IB control-state reachability, and IB deadlock are decidable for FIFO machines.

Remark. Since input-bounded FIFO machines subsume VASS (a VASS can be seen as an input-bounded FIFO machine with an alphabet reduced to a unique letter), the complexity of IB reachability is not elementary, which is inherited from the lower bound for VASS [START_REF] Czerwinski | The reachability problem for petri nets is not elementary[END_REF].

Unboundedness and Termination

IB unboundedness in FIFO machines reduces to an equivalent problem in counter machines. Given a FIFO machine M and L, the associated FIFO machine M in normal form (with the corresponding tuple ℒ of distinct-letter languages), as well as the associated counter machine C, the following result can be derived.

Proposition 27. Reach M ( L! ) is infinite iff Reach M (ℒ ! ) is infinite iff Reach C (L zero C ∩ ⟪V⟫) is infinite.
This statement also applies to prefix-closed languages so we have Reach M (Pref ( L! )), Reach M (Pref (ℒ ! )), and Reach C (L zero C ∩ ⟪Pref (V)⟫) are either all infinite or all finite. The latter-most is decidable as we establish in the following. Recall that, by the construction of C, we have

Reach C = Reach C (L zero C ∩ ⟪Pref (V)⟫).
The main idea that follows is the reduction of unboundedness of the counter machine to reachability in a modified counter machine. It is not immediate that we can use the results in the literature (for example [START_REF] Dufourd | Polynomial-Time Many-One Reductions for Petri Nets[END_REF]) which reduce boundedness to reachability in Petri nets/VASS. This is because the property of monotonicity does not extend to zero tests; if one can execute a zero test at (q, v), it is not necessarily the case that it can be executed at (q, v ) with v ≤ v , where we let v ≤ v if v x ≤ v x for all x ∈ Cnt. However, we show that, for the counter machine that we construct from the FIFO machine, this property does hold. If we are able to show this, the constructions used in the case of VASS can be adapted. Lemma 28. For every execution in C of the form (q 0 , 0) σ -→ (q, v) σ -→ (q, v ) such that v ≤ v , the following holds: The only counters that are tested to zero during σ already evaluate to zero at (q, v), and do not change their value throughout the execution of σ .

Proof. Let us assume to the contrary that there is at least one counter which is incremented or decremented during σ and also tested to zero during the execution. Without loss of generality, let us consider x (c,i) to be the first counter along the execution σ that is tested to zero during σ and also incremented/decremented before it was tested to zero.

Case (1): It has a non-zero value at (q, v), and is then either decremented, or first incremented and then decremented, and finally tested to zero. Since we know that σ.σ ∈ L zero C , no counter tested to zero can then be incremented. Hence, its value will remain zero. But this is a contradiction to our assumption that v ≤ v . Hence, all the counters with non-zero values at (q, v) cannot be tested to zero during σ . Case (2): It has value zero in (q, v), and is incremented, then decremented, then tested to zero during σ . This implies that it first has to be incremented. Consider now some sub-execution σ ∈ Pref (σ ) where (q, v) σ --→ (q 1 , v 1 ) such that the value of x (c,i) in the configuration (q 1 , v 1 ) is non-zero. Since there are no "new" zero-tests along the execution σ (by our assumption), we can execute σ from (q, v ) (by the monotonicity and trace property). However, we cannot increment the counter x (c,i) along σ , because it was tested to zero during the run (q 0 , 0) σ.σ --→ (q, v ). Hence, we once again have a contradiction. Now, we can use results from [START_REF] Finkel | Well-structured transition systems everywhere![END_REF] to show the following:

Proposition 29. The set Reach C is infinite iff there exist σ, σ ∈ A * C , q ∈ Q, and v, v ∈ N Cnt such that (q 0 , 0) σ -→ (q, v) σ -→ (q, v ) and v < v (i.e., v ≤ v and v = v ).
Construction of modified counter machine. We modify the counter machine C and construct a new counter machine C such that Reach C is infinite iff a configuration belonging to a finite set is reachable in C . The construction is loosely based on the reduction of boundedness to reachability for Petri Nets in [START_REF] Dufourd | Polynomial-Time Many-One Reductions for Petri Nets[END_REF]. Since we do not know the values of v and v a priori, we will try to characterize the general condition. The difference vv is a non negative vector, with at least one strictly positive component. We add a duplicate set of counters for every counter in the system. The intuition is that the counter machine non-deterministically moves from operating on both sets to a configuration from where it only operates on this second set. The first set will remain unchanged (with the value v), and the second set will keep track of the values (until it reaches v ). From this configuration (which represents (q, v )), we move to a new control state, q reach . Here, we check for the condition vv > 0 by first decrementing each counter in the first set which has a non-zero value in tandem with the corresponding counter in the second set. We do this until all the counters in the first set are equal to zero. If vv > 0, then there is at least one counter in the second set with a non-zero counter value. We non-deterministically decrement all the counters in the second set until we reach a configuration that has some counter c in the second set with a value of 1, and all other counters evaluate to zero. Since there are finitely many such configurations, we can just check every case.

Note that we can extend all these results for the case of termination as well. The only difference is that we now consider configurations (q, v) and (q, v ) such that v ≤ v . Once again, we can follow a similar argument to reduce the termination to the reachability of a configuration in this same modified counter machine.

Hence, we obtain the following theorem:

Theorem 30. IB unboundedness and IB termination are decidable for FIFO machines.

Remark. Gouda et al, stated that unboundedness is in EXPSPACE for letter-bounded systems [START_REF] Gouda | On deadlock detection in systems of communicating finite state machines[END_REF]. However, they only give an idea of the proof, stating that it can be done in a similar fashion as for the deadlock problem. In the construction for solving the deadlock problem, they reduce the input language to tally letter-bounded languages (tally means that the input-language is included in a * where a is a letter). They add as many channels as letters in the original letter-bounded-language. Furthermore, in order to ensure that every channel is empty before the next channel is read, they ensure that in all control states where a later channel is being read, there are reception transitions of previous channel contents which lead to a sink state (where there is never a deadlock). Notice that it is still possible to leave a channel non-empty before the next channel is read. But one never reaches a deadlock in such an "incorrect" run, since there is always the option of reading the unread channel contents of the previous channels and reach the sink state.

However, when we consider this model for unboundedness, there may exist unbounded "incorrect" runs since we can leave a channel non-empty and proceed to the next and may have an unbounded run. Hence, it seems that one still needs some reachability test to check if the runs are correct as we cannot ensure that some channels are zero in an unbounded run.

Conclusion and Perspectives

We extend recent results of the bounded verification of communicating finite-state machines (equivalently FIFO machines) [START_REF] Esparza | A perfect model for bounded verification[END_REF] and of flat FIFO machines [START_REF] Finkel | Verification of flat FIFO systems[END_REF] by using bounded languages for controlling the input-languages of FIFO channels (and not for controlling the runs of the machine). We extend old and recent results about input-bounded FIFO machines (see Table 1). In particular, we introduce the rational-reachability problem, which subsumes most of the well-known variants of reachability problems like: the (classical) reachability problem, the control-state reachability problem, and the deadlock problem. We also unify the terminology to facilitate the comparison between results. Moreover, note that, for most problems (except general/rational reachability), we can reduce output-bounded reachability to an equivalent input-bounded problem. There are still many open problems and challenges: What is the precise complexity of the five problems for input-bounded FIFO machines with a fixed number of channels? What is the precise complexity of control-state reachability, deadlock, unboundedness, and termination for input-bounded FIFO machines?

The size of the counter machine associated with a FIFO machine and a tuple of bounded languages is exponential, but only polynomial when we start from a normal form. It will be interesting to see whether the use of existing tools for counter machines is feasible for the verification of FIFO machines from case studies. Case studies shall also reveal how many FIFO machines/systems are actually boundable and/or flattable.

Towards a theory of boundable FIFO machines. In Example 9, we have seen that all configurations that are reachable in the CDP protocol are already reachable in presence of a suitable collection ℒ of bounded input-languages. By analogy with the well-established theory of flattable machines [START_REF] Bardin | FAST: Acceleration from theory to practice[END_REF][START_REF] Demri | Model-checking CTL * over flat Presburger counter systems[END_REF][START_REF] Chambart | Forward analysis and model checking for trace bounded WSTS[END_REF], we propose the following definition.

Definition 31.

Let M be a FIFO machine and let ℒ be a tuple of regular bounded languages. We say that M is ℒ-boundable if Reach M = Reach M (ℒ ! ). We say that M is boundable if there exists a tuple ℒ of regular bounded languages such that M is ℒ-boundable.

A Missing Proofs for Section 3

Theorem 7. The reachability problem is undecidable for FIFO machines with a (given) bounded reachability set.

Proof. We prove this by simulating a (two) counter Minsky machine by a FIFO machine with a bounded reachability set.

Consider a Minsky machine C = (Q, Cnt, T, q 0 ), where Q is the set of states, Cnt = {x 1 , x 2 } is the set of counters, q 0 the initial state, and T = {δ 1 , . . . , δ n } is the set of transition rules, which can be of two types: δ i : x j := x j + 1; goto q; δ i : if x j > 0 then (x j := x j -1; goto q) else goto q ; for j = {1, 2} and q, q ∈ Q.

We can construct a FIFO machine M = (Q , Ch, Σ, T, q 0 ) with a bounded reachability set as follows:

Q = Q Q , where Q is a set of intermediate states; Σ = {a, b, #, $, &}. There is a single channel, hence |Ch| = 1. We consider the language L ∈ $ * a * # * b * & * $ * a * # * b * & * ,
and we start with queue contents as $#&, where the letters #, $, & are used as markers during the test for zero. Intuitively, the number of occurrences of the letter a (resp. b) correspond to the counter valuations for x 1 (resp. x 2 ) in the configurations of the Minsky machine, and we rotate the tape contents in such a way that the contents always belong to L. For every state q ∈ Q, and every transition from it with the rule δ i : x 1 := x 1 + 1; goto q; for some q ∈ Q, we create the following transition sequence. We see that at every intermediate configuration, the channel contents still belong to L.

q q k ?$.!$ ?a !a ?# !a !# ?b !b ?&.!& Figure 3 Incrementing x1 .
Likewise, a transition of the form

δ i : if x 1 > 0 then (x 1 := x 1 -1; goto q) else goto q ;
can be constructed as follows. We see that the input language of the above machine is not bounded, since if we have a transition from q in the original machine of the following kind: δ i : x j := x j + 1; goto q; (a loop), the input language of the machine would be (a * #b * &) * for this transition, which is not bounded. Furthermore, the machine is not flat either, since there can be control states that are in more than one elementary loop.

q q l q k ?#.!# ?a ?a !a ?# !a !# ?b !b ?&.!& ?b!b ?&.!&
Lemma 15. We have (q, ŵ)

∈ Reach M ( L! ) for some ŵ ∈ R iff ((q, q A ), w) ∈ Reach M (ℒ ! ) for some q A ∈ Q A and w ∈ h -1 ( R).
Proof. Let us assume we have (q, ŵ) ∈ Reach M ( L! ) for some ŵ ∈ R. Hence, there exists

σ ∈ L! such that (q 0 , ε) σ -→ (q, ŵ). For channel c, let ŵc = proj c! (σ). Since σ ∈ L! , we have ŵc ∈ Lc for all c ∈ Ch. Let w c ∈ L c = h -1 c ( Lc ) ∩ (w c,1 ) * . . . (w c,nc ) * such that h c (w c ) = ŵc . There is a unique σ ∈ A *
M such that h(σ) = σ and proj c! (σ) = w c and proj c? (σ) ∈ Pref (w c ) for all c ∈ Ch. Here, h : Σ * → Σ * is defined by h(a) = h c (a) for all c ∈ Ch and a ∈ Σ c , and we extend this to h : A * M → A * M in the expected manner. Note that σ ∈ ℒ ! ∩ Pref (ℒ ? ). Hence, we know that in the FIFO machine h -1 ( M ), one has (q 0 , ε) σ -→ (q, w) for some w (by construction of h -1 ( T )), and that σ ∈ L(A). Therefore, since M is a product of the two machines, we can deduce that there is a run in M of the kind ((q 0 , q 0 A ), ε) σ -→ (q, q A ), w), for some value of q A . Furthermore, by h(σ) = σ, we have h(w) = ŵ. Hence, w ∈ h -1 ( R).

Conversely, let us assume that ((q, q A ), w) ∈ Reach M (ℒ ! ) for some q A ∈ Q A and channel contents w ∈ h -1 ( R). Then, we know that there exists σ ∈ ℒ ! such that ((q 0 , q 0 A ), ε)

σ -→ (q, q A ), w). Let σ = h(σ). Since σ ∈ ℒ ! , we have proj c! (σ) ∈ L c for all c ∈ Ch. In particular, proj c! (σ) ∈ h -1
c ( Lc ) and, therefore, h c (proj c! (σ)) = proj c! (h(σ)) ∈ Lc . We deduce σ ∈ L! . Furthermore, we can execute σ in M (by construction) to reach configuration (q, ŵ) for some ŵ. By σ = h(σ), we have ŵ = h(w). Therefore, ŵ ∈ R. Proof. Observe that Traces(M ) ⊆ Traces((Q, A M , T, q 0 )) ⊆ Pref (V). Thus, the first property holds.

For the second statement, consider

(q 0 , 0) = (q 0 , v 0 ) α1 -→ C (q 1 , v 1 ) α2 -→ C . . . αn --→ C (q n , v n )
and let τ = α 1 . . . α n . Thus, τ ∈ Traces(C). Suppose that we apply a zero test at position ∈ {1, . . . , n}, i.e., α = (dec(x (c,j) ), Z) for some (c, j), where Z contains the counters x (c,i) with i < j. Then, there is k < such that α k = (inc(x (c,j) ), ∅). By the construction of C, we have transitions (q k-1 , c!a , q k ) and (q -1 , c?b , q ) in M for some a, b ∈ Σ c,j . By the trace property of M , none of the actions "reachable" from q in M employs a message from Σ c,i , for all i < j. Thus, none of the actions α m with ≤ m modifies a counter from Z. We deduce that τ ∈ L zero C .

Proposition 19. Let σ ∈ A * M . For all (q, w) ∈ S M and a ∈ c∈Ch Σ ⊥ c such that σ ∈ L last a , we have: (q 0 , ε) σ -→ M (q, w) =⇒ (q 0 , 0) ⟪σ⟫ --→ C (q, ⟪w⟫) and a ∈ G(w) .

Proof. We will prove the statement by induction on the length of σ. In the base case, |σ| = 0. The only value of σ such that |σ| = 0 is σ = ε. Furthermore, ε ∈ Pref (V) ∩ L last a where a = (⊥) Ch . The initial configuration (q 0 , ε) ∈ S M is the only configuration reachable by ε. In T C , the only configuration reachable via ⟪ε⟫ = ε is (q 0 , 0) = (q, ⟪ε⟫), and ⟪ε⟫ ∈ L zero C . Finally, we also see that a ∈ G(ε). Therefore, the base case is valid.

We suppose that the statement is true for all σ ∈ A * M such that |σ| = n. We will now show that it is true for σ ∈ A * M where |σ | = n + 1. Let a ∈ c∈Ch Σ ⊥ c and suppose σ ∈ Pref (V) ∩ L last a . We write σ = σ.β such that σ ∈ Pref (V) ∩ L last a for some a ∈ c∈Ch Σ ⊥ c , |σ| = n, and β ∈ A M . There exists such a σ since the set Pref (V) is prefix-closed.

Let (q , w ) ∈ S M such that (q 0 , ε) σ -→ M (q , w ). Then, there is (q, w) ∈ S M such that (q 0 , ε) σ -→ M (q, w) β -→ M (q , w ). Hence, there exists t = (q, β, q ) ∈ T in the FIFO machine. By construction of C, we know that there is a transition t = (q, inc(x (c,ia) ), ∅, q ) ∈ T in C, and by the definition of ⟪ . ⟫, we also have ⟪β⟫ = (inc(x (c,ia) ), ∅). By induction hypothesis, we have (q 0 , 0) ⟪σ⟫ --→ (q, v) where v = ⟪w⟫. Since ⟪β⟫ increases a counter, we have (q, v) ⟪β⟫ --→ (q , v ) for the counter valuation v such that v x = v x + 1 for x = x (c,ia) and v y = v y for all y ∈ Cnt \ {x}. Hence, ⟪w ⟫ = v and we have (q 0 , 0) ⟪σ.β⟫ ----→ (q , ⟪w ⟫). Note that, by Lemma By construction of C, we know that there is a transition t = (q, dec(x (c,ia) ), Z, q ) ∈ T in C where Z = {(x (c,j) ) | j < i a }. By the definition of ⟪ . ⟫, we also have ⟪β⟫ = (dec(x (c,ia) ), Z).

By the induction hypothesis, we have (q 0 , 0) ⟪σ⟫ --→ (q, ⟪w⟫). Furthermore, recall that w c = a.w c . This implies that a is at the head of the channel c in the configuration (q, w). Hence, all the letters b such that i b < i a are not present in the channel. Therefore, in the configuration (q, ⟪w⟫), all the counters x (c,i b ) are equal to zero for i b < i a . Hence, we can execute the transition t from (q, ⟪w⟫), and we have (q 0 , 0) ⟪σ⟫ --→ (q, ⟪w⟫) ⟪β⟫ --→ (q , v ) for some counter valuation v . By Lemma 17, we have ⟪σ.β⟫ ∈ L zero C . We write v = ⟪w⟫, and from the counter machine transition relation, we know that v x = v x -1 for x = x (c,ia) and v y = v y for all y ∈ Cnt \ {x}. Hence, ⟪w ⟫ = v .

From the induction hypothesis, we know that a ∈ G(w). In order to show that a ∈ G(w ), we only need to address the case of the channel c, since the values of a d , w d remain unchanged for all d = c. We know from the induction hypothesis that w c ∈ Infix(L c ). Hence, we can immediately deduce that w c ∈ Suf (w c ) ⊆ Infix(L c ).

Furthermore, we know that w c = u.a c for some u ∈ Σ * c . If u = ε, then we can deduce that w c = ε. If u = ε, then we have w c = u .a c such that a.u = u. Hence, a ∈ G(w ).

Proposition 20. Let τ ∈ A *

C . For all (q, v) ∈ S C and a ∈ c∈Ch Σ ⊥ c such that τ ∈ ⟪Pref (V) ∩ L last a ⟫, we have:

(q 0 , 0) τ -→ C (q, v) =⇒ (q 0 , ε) τ --→ M (q, v a ) .
Proof. We proceed by induction on the length of τ . In the base case, |τ | = 0. The only value of τ such that |τ | = 0 is τ = ε. Furthermore, ε ∈ ⟪Pref (V) ∩ L last a ⟫ where a c = ⊥ for all c ∈ Ch. The only configuration reachable via ε is (q 0 , 0). In the FIFO machine, the configuration (q 0 , ε) is the only configuration reachable via ε = ε. We know that the initial contents is ε = 0 a . Hence, the base case is valid.

Let us suppose that the statement holds for τ ∈ A * C where |τ | = n. We show that it is true for τ with |τ | = n + 1. Let a such that τ ∈ ⟪Pref (V) ∩ L last a ⟫. Then we can write τ = τ.α for some τ ∈ A * C and α ∈ A C . There exists σ ∈ Pref (V) ∩ L last a such that ⟪σ ⟫ = τ . Furthermore, since ⟪ . ⟫ is a homomorphism, we can express σ = σ.β for some σ ∈ A * M and β ∈ A M where ⟪β⟫ = α and ⟪σ⟫ = τ . Since Pref (V) is prefix-closed, we have σ ∈ Pref (V) ∩ L last a for some a ∈ c∈Ch Σ ⊥ c . Therefore, τ ∈ ⟪Pref (V) ∩ L last a ⟫. Let (q 0 , 0) τ -→ C (q , v ). Note that, by Lemma 17, we have τ ∈ L zero C . We will prove that (q 0 , ε) τ --→ M (q, w ) where w = v a . Since τ = τ.α, there is (q, v) ∈ S C such that (q 0 , 0) τ -→ (q, v) α -→ (q , v ). Hence, there exists a transition t = (q, α, q ) ∈ T . By the induction hypothesis, we know that (q 0 , ε) τ --→ M (q, w) where w = v a .

Case (1): Suppose α = (inc(x (c,i) ), ∅) for c ∈ Ch and i ∈ {1, . . . , n c }. We have v x = v x + 1 for x = x (c,i) and v y = v y and for all y ∈ Cnt \ {x}.

By construction of C, we know that there is a transition t = (q, γ, q ) ∈ T in M with γ = c!a for some a ∈ Σ c such that i a = i. Thanks to the trace property (Definition 12 (2.)), we have β = γ. Let w be given by w c = w c .a and w d = w d for all d ∈ Ch \ {c}. Then, (q, w) β -→ M (q , w ). Furthermore, since i a = i and ⟪w⟫ = v, we can deduce that ⟪w ⟫ = v . Moreover, recall that ⟪σ.β⟫ = τ.α, hence, σ = σ.β = τ .

Since σ = σ.β and β = c!a , we can deduce that a c = a and a d = a d for all d = c. This is because the only change in the last sent letters between σ and σ is in the channel c.

We recall that ⟪w ⟫ = v . From the induction hypothesis, we know that v a = w. Hence, in order to show that v a = w , we only need to address the case of the channel c, since the values of a d , w d remain unchanged for all d = c. We know that w c = w c .a c . Since σ ∈ Pref (ℒ ! ), we have w c .a c ∈ Infix(L c ). Therefore, w = v a .

Case (2): Suppose α = (dec(x (c,i) ), Z), for c ∈ Ch, i ∈ {1, . . . , n c } and Z = {x (c,j) | j < i}. We have v x = v x -1 for x = x (c,i) and v y = v y for all y ∈ Cnt \ {x}.

By construction of C, we know that there is a transition t = (q, γ, q ) ∈ T in M with γ = c?a for some a ∈ Σ c such that i a = i. Again, by the trace property (Definition 12 (2.)), we get β = γ. In order to execute t from (q, w), it is necessary that we have w c = a.u for some word u.

Since σ.β ∈ Pref (ℒ ? ) and proj c? (σ).w c = proj c! (σ), we can deduce that w c = a.u for some word u. Hence, the transition t can be executed to reach a configuration (q , w ) such that w c = a • w c , and w d = w d for all d ∈ Ch \ {c}. Furthermore, since i a = i and ⟪w⟫ = v, we can deduce that ⟪w ⟫ = v . Moreover, recall that ⟪σ.β⟫ = τ.α, hence, σ = σ.β = τ .

Since σ = σ.β and β = c?a , we can deduce that a = a. This is because no letters are sent between σ and σ .

We also know from the induction hypothesis that w = v a . Also recall that ⟪w ⟫ = v . In order to show that w = v a , we only need to address the case of the channel c, since the values of a d , w d remain unchanged for all d = c.

We know from the induction hypothesis that w c is contained in Infix(L c ) and, thus, so is w c . Furthermore, we know that w c = u.a c for some u ∈ Σ * c . If u = ε, then we can deduce that w c = ε. On the other hand, if u = ε, then we know that w c = u .a c such that a.u = u. We also recall that ⟪w ⟫ = v . Hence, w = v a . Lemma 22. The set V a (ℛ) is effectively semi-linear.

Proof. For c ∈ Ch, let G c be the set of words w ∈ Σ * c such that a c is good for w. Moreover, let = c∈Ch G c . As G c is regular for every c ∈ Ch, the relation is recognizable. As the intersection of a rational and a recognizable relation is rational, we have that ℛ ∩ is rational. It follows that Parikh(ℛ ∩ ) is semi-linear. From the definitions, we obtain

v a ∈ ℛ ⇐⇒ ∃w ∈ ℛ ∩ : ∀x (c,i) ∈ Cnt : v x (c,i) = a∈Σc,i |w c | a ⇐⇒ ∃π ∈ Parikh(ℛ ∩ ) : ∀x (c,i) ∈ Cnt : v x (c,i) = a∈Σc,i π a Thus, V a (ℛ) = {v ∈ N Cnt | v a ∈ ℛ} = a∈Σc,i π a x (c,i) ∈Cnt | π ∈ Parikh(ℛ ∩ ) .
Let ϕ((X a ) a∈Σ ) be a Presburger formula defining Parikh(ℛ ∩ ). Then, by the above equivalence, the following Presburger formula defines V a (ℛ):

ψ c ((Z y ) y∈Cnt ) = ∃(X a ) a∈Σ : ϕ((X a ) a∈Σ ) ∧ y∈Cnt Z y = a∈Σy X a
where, for y = x (c,i) ∈ Cnt, we let Σ y = Σ c,i . It follows that V a (ℛ) is effectively semilinear.

Corollary 23. For every q ∈ Q, we have:

(q, w) ∈ Reach M (ℒ ! ) for some w ∈ ℛ ⇐⇒ (q, v) ∈ Reach C (L zero C ∩ ⟪V ∩ L last a ⟫) for some a ∈ c∈Ch Σ ⊥ c and v ∈ V a (ℛ) .
Proof. Suppose (q, w) ∈ Reach M (ℒ ! ) with w ∈ ℛ. There are a ∈ c∈Ch Σ ⊥ c and σ ∈ V∩L last a such that (q 0 , ε) σ -→ M (q, w). By Proposition 19 and Lemma 17, we have (q 0 , 0) ⟪σ⟫ --→ C (q, ⟪w⟫) and ⟪σ⟫ ∈ L zero C and a ∈ G(w). By definition, the latter implies w = ⟪w⟫ a and hence ⟪w⟫ ∈ V a (ℛ).

Conversely, suppose we have (q 0 , 0) Proof. We show both parts of the lemma.

⟪σ⟫ --→ C (q, v) where σ ∈ V ∩ L last a , ⟪σ⟫ ∈ L zero C , and v ∈ V a (ℛ). By Proposition 20, we get (q 0 , ε) ⟪σ⟫ ---→ M (q, v a ). Note that ⟪σ⟫ = σ ∈ ℒ ! . Moreover, v ∈ V a (ℛ) implies v a ∈ ℛ,

Part (a):

Let us consider a FIFO machine M = (Q, Ch, Σ, T, q 0 ), a control-state q, a configuration (q, w) and a tuple ℒ = (L c ) c∈Ch of regular bounded languages L c ⊆ Σ * c . We let m = |Ch|.

We first reduce IB reachability to IB control-state reachability. Another machine M (q,w) = (Q , Ch, Σ , T , q 0 ) is constructed as follows:

Q = Q ∪ {q end } such that q end / ∈ Q, Σ = Σ ∪ {$} such that $ ∈ Σ. A path q σ -→ q end is
added from the control state q. We write σ = (σ 1 . . . σ m ). For c ∈ Ch, we have

σ c = c!$ • c?w c (1) • • • c?w c (|w c |) • c?$ if |w c | > 0. c!$ • c?$ otherwise.
The configuration (q, w) is in Reach M (ℒ ! ) iff the control state q end is in Reach M (q,w) (ℒ ! ) where ℒ = (L c .w c .$) c∈Ch . Furthermore, ℒ is bounded if ℒ bounded, since concatenation of a finite word with a bounded language results in a bounded language. Therefore, IB reachability reduces to IB control-state reachability for FIFO machines. Conversely, in order to show that IB control-state reachability is reducible to IB reachability, we construct M q as follows. To M , we add |Σ| × m self-loops from and to the control state q as follows: q c?a --→ q for all c ∈ Ch and a ∈ Σ c . The control-state q is reachable in M iff there exists w such that (q, w) is reachable in M iff (q, ε) is reachable in M q . Furthermore, consider σ ∈ Pref (ℒ ! ) such that (q 0 , ε) σ -→ M (q, w) for some channel contents w. Let us append to σ a set of actions σ = σ 1 • • • σ m such that σ c = c?w c for all c ∈ Ch, where c?w c is to be understood as a sequence of transitions whose effect is to consume the string w c from the channel c. By construction, we have, (q 0 , ε) σ•σ ---→ Mq (q, ε). Furthermore, the following property holds true: proj c! (σ) = proj c! (σ •σ ) for all c ∈ Ch. Hence, σ • σ ∈ Pref (ℒ ! ) and we can conclude that (q, w) ∈ Reach M (ℒ ! ) iff (q, ε) ∈ Reach Mq (ℒ ! ). Therefore, IB control-state reachability reduces to IB reachability for FIFO machines.

Part (b):

Given a FIFO machine M = (Q, Ch, Σ, T, q 0 ), a configuration (q, w) and a tuple ℒ = (L c ) c∈Ch of non-empty regular bounded languages L c ⊆ Σ * c , we construct M (q,w) as in the case of reducing reachability to control state reachability (see proof of Prop. 25). We then modify M (q,w) to M as follows. We add a new channel d to the existing set of channels Ch (the set of channels is now Ch ). For all q = q end , we add the following transition: (q, d!$ , q). Hence, except for q end , every control state has at least one send action. Finally, we also construct a new tuple ℒ = (L c ) c∈Chm such that L c = L c .$ for all c ∈ Ch and L d = $ * .

Claim: (q, w) is in Reach M (ℒ ! ) if and only if we can reach a deadlock s in Reach M (ℒ ! ). To see this, first, we observe that if there is a deadlock in Reach M (ℒ ! ), then the associated control state would be q end since if we are in any configuration s such that the associated control state q = q end , the transition (q , d!$ , q ) can always be taken, and hence, there will never be a deadlock.

Let us now suppose that the configuration (q, w) is in Reach M (ℒ ! ). We can execute the same set of transitions as in M and reach the control state q with the channel contents w via an execution σ in M . Having done that, we can then execute the path q σ -→ q end as described in T in order to reach q end . Also observe that the execution σ .σ ∈ ℒ ! . Since there are no transitions from this control state, we reach a deadlock.

Suppose now that (q, w) is not in Reach M (ℒ ! ). Hence, we cannot reach (q, w) in M and thus, cannot execute q σ -→ q end . Furthermore, as we saw previously, we can never be in a deadlock as we can always send $ to the channel d. Proof. We first show that unboundedness is preserved by the normal-form construction. This essentially follows from Lemma 15.

If (q, ŵ) ∈ Reach M ( L! ), then ((q, q A ), w) ∈ Reach M (ℒ ! ) for some q A and w such that h(w) = ŵ. Thus, if Reach M ( L! ) is infinite, then so is Reach M (ℒ ! ).

Conversely, if ((q, q A ), w) ∈ Reach M (ℒ ! ), then (q, h(w)) ∈ Reach M ( L! ). Thus, if Reach M (ℒ ! ) is infinite, then so is Reach M ( L! ). Now, let us assume that Reach M (ℒ ! ) is infinite. Hence, there are infinitely many configurations (q, w) ∈ S M which are reachable from (q 0 , ε). From Corollary 21, for each of these configurations, there is a configuration (q, ⟪w⟫) reachable in C such that (q, ⟪w⟫) ∈ Reach C (L), where L = L zero C ∩ ⟪ℒ ! ∩ Pref (ℒ ? ) ∩ a∈G(w) L last a ⟫. Since L ⊆ L zero C ∩ ⟪ℒ ! ∩ Pref (ℒ ? )⟫, we have (q, ⟪w⟫) ∈ Reach C (L zero C ∩⟪ℒ ! ∩Pref (ℒ ? )⟫). Furthermore, there are only finitely many configurations (q, w) ∈ S M that correspond to a configuration (q, ⟪w⟫) ∈ S C . Hence, if Reach M (ℒ ! ) is infinite, Reach C (L zero C ∩ ⟪ℒ ! ∩ Pref (ℒ ? )⟫) is infinite. For the converse direction, let us assume that Reach C (L zero C ∩ ⟪ℒ ! ∩ Pref (ℒ ? )⟫) is infinite. Hence, there are infinitely many configurations (q, v) reachable from (q 0 , 0) via τ such that τ ∈ L zero C ∩ ⟪ℒ ! ∩ Pref (ℒ ? )⟫. For each τ , there exists a unique σ such that ⟪σ⟫ = τ . Consider the vector a such that σ ∈ L last a . We let v a = w for some channel contents w, then we have ⟪w⟫ = v. Hence, (q, ⟪w⟫) ∈ Reach C (L zero C ∩ ⟪ℒ ! ∩ Pref (ℒ ? ) ∩ a∈G(w) L last a ⟫). From Corollary 21, we can deduce that (q, w) ∈ Reach M (ℒ ! ). Therefore, for every v such that (q, v) is reachable, there is a corresponding configuration (q, w) reachable in Reach M (ℒ ! ). Proposition 29. The set Reach C is infinite iff there exist σ, σ ∈ A * C , q ∈ Q, and v, v ∈ N Cnt such that (q 0 , 0) σ -→ (q, v) σ -→ (q, v ) and v < v (i.e., v ≤ v and v = v ).

Proof. Let us assume that Reach C is infinite. As in [START_REF] Finkel | Well-structured transition systems everywhere![END_REF], we consider the tree of all prefixes of computations. We prune this tree by removing all prefixes where there is at least a loop, i.e. containing two nodes that are labeled by the same configuration. Since every reachable configuration can be reached without a loop, we still have infinite number of prefixes in the pruned tree. For every configuration (q, v) in the tree, there are finitely many successors (as the TS is finitely branching). Hence, in order for the tree to be infinite, there is at least one infinitely long execution (by König's lemma). This execution has no loop. Therefore, by Dickson's lemma, there are infinitely many configurations s i = (q 1 , v 1 ), s j = (q 2 , v 2 ), . . . such that v 1 < v 2 < . . . and i < j. Once we extract this sequence, since there are only finitely many control states in Q, we know that there is at least one pair (q, v), (q, v ) such that (q 0 , 0) σ -→ (q, v) σ -→ (q, v ) and v < v .

Conversely, let us assume that there is an execution (q 0 , 0)

σ -→ (q, v) σ -→ (q, v ) such that v < v .
We know from Lemma 28 that the only counters which may be tested for zero during σ already evaluate to zero at (q, v), and do not change their value throughout the execution of σ . Therefore, all the transitions of the counter system in σ can be considered as VASS operations. Hence, the property of monotonicity holds, i.e. if (q, v) σ -→ (q, v ) and (q, v) < (q, v ), then we know there exists an infinite sequence s i = (q, v 1 ), s j = (q, v 2 ), . . . such that v 1 < v 2 < . . . reachable from (q, v ). Hence, we see that Reach C is infinite if and only if there exist σ, σ such that (q 0 , 0) σ -→ (q, v) σ -→ (q, v ) and v < v . value of v . Hence, the second set is strictly greater, and we can reach some configuration in Conf, by decrementing all the counters until there is exactly one counter left with a non-zero value, more precisely, with the value 1.

Hence, we can reach some configuration in Conf in C iff Reach C is infinite.

For the case of termination, the same arguments can be adapted. We modify Conf to contain just the single configuration (q reach , (0, . . . , 0)). We can reach the configuration (q reach , (0, . . . , 0)) in C iff there is a non-terminating execution in C belonging to L zero C ∩ ⟪Pref (ℒ ! ∩ ℒ ? )⟫.

Figure 1

 1 Figure 1The model of the connection-deconnection protocol

4 .

 4 and w d = w d for all d ∈ Ch \ {c}. The index M may be omitted whenever M is clear from the context. The reachability set of M is defined as the reachability set of T M , i.e., Reach M = Reach T M and, for L ⊆ A * M , Reach M (L) = Reach T M (L). Moreover, we let Traces(M ) = Traces(T M ). Example An example run of the FIFO machine M from Example 3 and Figure 1 is

Example 13 .

 13 Property. Consider the bounded language Lc over ( ŵc,1 , . . . , ŵc,nc ). For i ∈ {1, . . . , n c }, let m i = | ŵc,1 | + . . . + | ŵc,i | be the number of letters in the first i words. Moreover, m = m nc . Let Σ c denote the alphabet {a c 1 , . . . , a c m }. It contains the "distinct" letters for the bounded language L c over (w c,1 , . . . , w c,nc ), where we let w c,1 = a c 1 . . . a c m1 and w c,i = a c mi-1+1 . . . a c mi for i ≥ 2. In other words, the letters in (w c,1 , . . . , w c,nc ) are numbered consecutively. In order to obtain the language L c , we first consider the homomorphism h c : Σ * c → Σ * c where h c (a c i ) is the i-th letter in the word ŵc,1 . . . ŵc,nc . We obtain L c as h -1 c ( Lc ) ∩ (w c,1 ) * . . . (w c,nc ) * , hence preserving regularity and boundedness. We then remove those words from (w c,1 , . . . , w c,nc ) (and their letters from Σ c ) whose letters do not occur in L c . We have Σ c ⊆ Alph(L c ). For example, suppose we have one channel c and Lc = (ab) * bb * over (ab , b).

Lemma 17 .

 17 We have Traces(M ) ⊆ Pref (V) and Traces(C) ⊆ L zero C . With every channel contents w ∈ c∈Ch Σ * c of the FIFO machine M , we associate a counter valuation ⟪w⟫ = v ∈ N Cnt where, for each counter x (c,i) , we let v x (c,i) = a∈Σc,i |w c | a . Furthermore, abusing notation, we define a homomorphism ⟪ . ⟫ : A * M → A * C which maps a sequence of actions of M to a sequence of actions of C. It is defined by ⟪ c!a ⟫ = (inc(x (c,ia) ), ∅) and ⟪ c?a ⟫ = (dec(x (c,ia) ), Z) where Z = {x (c,j) | j < i a }.

-→ s 1 β2-→ s 2 β3-

 12 and a tuple ℒ = (L c ) c∈Ch of non-empty regular bounded languages L c ⊆ Σ * c . IB reachability: Do we have s ∈ Reach M (ℒ ! ) ? IB control-state reachability: Do we have (q, w) ∈ Reach M (ℒ ! ) for some w ? IB deadlock: Does Reach M (ℒ ! ) contain a deadlock ? IB unboundedness: Is Reach M (Pref (ℒ ! )) infinite? IB termination: Is there no infinite execution of the form init M β1 → . . . such that, for all i ∈ N, we have s i ∈ S M , β i ∈ A M , and β 1 . . . β i ∈ Pref (ℒ ! )?

Figure 4

 4 Figure 4 Decrementing x1

Lemma 17 .

 17 We have Traces(M ) ⊆ Pref (V) and Traces(C) ⊆ L zero C .

Case ( 1 ):

 1 Suppose β = c!a , for some c ∈ Ch and a ∈ Σ c . Hence, we have w c = w c .a, and w d = w d for all d ∈ Ch \ {c}. Moreover, since σ = σ.β and β = c!a , we can deduce that a c = a and a d = a d for all d = c. This is because the only change in the last sent letters between σ and σ is in the channel c.

  17, we have ⟪σ.β⟫ ∈ L zero C . From the induction hypothesis, we know that a ∈ G(w). In order to show that a ∈ G(w ), we only need to address the case of the channel c, since the values of a d , w d remain unchanged for all d = c. We know that w c = w c .a c . By induction hypothesis, w c ∈ Infix(L c ). Since σ ∈ Pref (ℒ ! ), we also have w c .a c ∈ Infix(L c ). Hence, a ∈ G(w ). Case (2): Suppose β = c?a , for some c ∈ Ch and a ∈ Σ c . We have w c = a.w c , and w d = w d for all d ∈ Ch \ {c}. Since σ = σ.β and β = c?a , we can deduce that a = a. This is because there is no change in the last letter sent between σ and σ .

B Missing Proofs for Section 4 Proposition 25 .

 425 which concludes the proof. IB reachability is (a) recursively equivalent to IB control-state reachability for FIFO machines, and (b) recursively reducible to IB deadlock for FIFO machines.

Proposition 27 .

 27 Reach M ( L! ) is infinite iff Reach M (ℒ ! ) is infinite iff Reach C (L zero C ∩ ⟪V⟫) is infinite.

Table 1

 1 Summary of key results; results for all other extensions are subsumed by these results (D stands for decidable).Hence, we deduce that reachability is decidable for ℒ-boundable FIFO machines, which is a strictly larger class than input-bounded machines. CDP is not input-bounded but it is ℒ CDP -boundable with ℒ CDP = ((ab) * (a + ε)(ab) * , e * ). Let us also remark that CDP is flattable by using the bounded set of runs (!a!b) * !a!e?e(!a!b) * + (!a!b) * (where we omit channel information for readability), because it covers the reachability set which is equal to (ab)

		Flat	Letter-bounded	Bounded
	UNBOUND	NP-C ([18])	D ([23])	D ([26])
	TERM	NP-C ([18])	D	D
	REACH	NP-C ([18])	D	D, not ELEM
	CS-REACH	NP-C ([14, 18])	D	D
	DEADLOCK	D	D ([23])	D

* (a + ε)(ab) * on control-state (0, 0). It is not clear whether reachability is decidable for boundable machines. A strategy that would fairly enumerate all regular bounded families ℒ 1 , ℒ 2 , . . . , ℒ n , . . . will necessarily find the good one, if M is boundable, but this is not sufficient because we must be able to recognize Reach M . Observe that boundable machines are more robust than flat machines. Consider a system S = (A 1 , A 2 , . . . , A n ) of n flat finite automata A i communicating peer to peer (P2P) through one-directional FIFO channels. Let M S denote FIFO the machine obtained as the Cartesian product of all automata A i of S; there is no reason to assume that M S is flattable but it is input-bounded and thus M S is ℒ-boundable where ℒ is computable from S.

We say configurations rather than states to distinguish them from the control states used in FIFO and counter machines.

Proposition 32. Reach C is infinite iff some configuration from the set Conf is reachable in C .

Proof. Let C = (Q, Cnt, T, q 0 ). Recall that Reach C is infinite iff there is a run (q 0 , 0) σ -→ (q, v) σ -→ (q, v ) such that v < v .

To check this condition, we build a modified counter system C = (Q , Cnt , T , q 0 ) as follows.

For every transition q

------→ q we have the following transitions. q (op(x,1),op(x,2),Z )

------------→ q ∈ T where Z = Z × {1, 2}. These transitions go from the same control states as in the original counter machine, but increment both sets of counters.

(q b , q) (op(x,2),Z ) -------→ (q b , q ) ∈ T for all q b ∈ Q where Z = Z × {2}. These transitions are executed from the new pair of states that have been created, but the first component is unchanged, and the second component go from the same control states as in the original counter machine. Notice however, that only the second set of counters are modified now. q (op(x,2),Z ) -------→ (q, q ) ∈ T for all q b ∈ Q where Z = Z × {2}. In this case, the transition goes from the original set to one of the pairs of states. We add a few more transitions to the set T .

(q, q) nop --→ q reach ∈ T for all q ∈ Q. This set ensures that we reach the control state q reach . (Note that we add a new type of transition called nop which does not change any of the counter values. This type of transition can be eliminated by adding a fresh counter, if needed.) Then we add some self loops to the state q reach to decrement all the counters. q reach (dec(x,1),dec(x,2),Z) -------------→ q reach ∈ T for all x = x (c,i) ∈ Cnt and Z = {x (c,j) | j < i} × {1, 2}. (This decrements all the counters (x, 1) along with (x, 2)). q reach (dec(x,2),Z) -------→ q reach ∈ T for all x = x (c,i) ∈ Cnt {x sum } and Z = {x (c,j) | j < i} × {1, 2}. (This decrements only the set Cnt × {2}). We define the set Conf as follows. Conf = {(q reach , v) | v (x,2) = 1 and v (x,1) = 0 for some x ∈ Cnt and v (y,j) = 0 for all y ∈ Cnt \ {x} and j ∈ {1, 2}}.

We first show that if we can reach some configuration in Conf, then Reach C is unbounded. The transitions are organised such that first the counter machine will increment both sets of counters while staying in Q ⊆ Q . In order to reach the control state q reach , it will non-deterministically move to one of the subsets {q} × Q. It will only modify the second set of counters, and will finally move to the control state q reach iff it is in the state (q, q). Notice however, that in order to visit q reach in C , the original counter system must have a transition sequence that visits the same control state q twice. The first visit is needed to ensure that we reach the subset {q} × Q and the second visit to reach (q, q). Now, in q reach , the transitions that decrement the first set of counters also decrement the second set. Therefore, the second set should have at least the same value as the first set in order for the first set to reach zero. This is only possible if there was a strict difference from the first set to the second set, i.e. v < v .

On the hand, if the set Reach C is infinite, then there is a σ, σ ∈ A * C and (q, v), (q , v ) ∈ S C such that (q 0 , 0) σ -→ (q, v) σ -→ (q , v ) and (q, v) < (q , v ). Hence, we stay in Q until the end of σ, then move to {q} × Q until we reach (q, q). Then we can take the nop transition to reach q reach . Observe that the first set of counters give us the value of v, and the second the


domain: phys chim

text:
Maël Le Marre

Philippe Mandin

Praveen Thappily

Erik Zlliox

Jean-Louis Lanoisellé

Thierry Sauvage

Coupling Micro-Hydropower with electrolyzing, case study

à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Coupling Micro-Hydropower with electrolyzing, case study

Maël Le Marre 1,2 Philippe Mandin 1,2 Praveen Thappily 1,2 Erik Zlliox 2 Jean-Louis Lanoisellé 1 Thierry Sauvage 2 1 Université de Bretagne Sud, IRDL, UMR CNRS 6027, Lorient (France) 2 GIP Campus Esprit Industries, Redon (France) mael.le-marre@univ-ubs.fr philippe.mandin@univ-ubs.fr

The energy used to pump and treat water for residents and industry represents betweenand 3% of the world's energy consumption {1}. The consumption can be reduced by 25% trough solutions like microhydropower (MHP). Pressure reducing valve (PRV) are installed in the water distribution network (WDN) to reduce the leakage losses, which is directly related to the pressure in pipe {2}. The reducing of pressure in PRVs lead to hydraulic losses into thermal losses, replace PRV with MHP system is a good solution to recover a part of those losses. On the other hand, the transport area, with thermal motor, is one of the main issues for slowing the global warming. Replace thermal motor with electrical motor supplied by fuel cells is a good solution. One of the biggest water tanks in Rennes (France) called "Les Gallets" is an interesting site to implement MHP installation, the huge site area allows to implement a electrolyze installation to supply hydrogen cars. Coupling the production of hydrogen with MHP system is a solution to get a green energy production. The scheme of the installation is presented in figure 1.

The site "Les Gallets" is composed of two water tanks, one is called "Les Gallets Haut", the other one is called "Les Gallets Bas". Two MHP systems can be installed, one upstream the first water tank, and one between both water tanks. Conventional turbines are not massively available on the market, hence they are expensive and lead to strong payback periods for MHP, to face this problem, the use of pumps in reverse mode (pumps as turbines) is a solution {3}. Indeed, those pumps have a good accuracy (between 50 to 85%) and can divided by 10 times the payback period of an installation compared to conventional turbines installations. For this study, an average efficiency of 65% for Pumps as turbines installations is considered. Flow conditions of both installations are detailed in table 1. The total electricity production in "Les Gallets" will reach about 197MWh per year. Considering that the electrolyzer absorb 60 kWh of electricity to create 1kg of Hydrogen. The electrolyzer will be able to produce about 3285kg of H 2 per year. Considering a conventional Hydrogen car, with an autonomy of 500km, and a Hydrogen's consumption of 1kg of H 2 /100km, it will be possible to load the car's fuel cell 625 times per year.

Site

  Marchis et al., 2014, Procedia Engineering: "Energy recovery in water distribution networks. Implementation of pumps as turbine in a dynamic numerical mode" {2}: Colombo et al., 2002, Water Resour. Plan. Manag, 128, 441-450: "Energy and costs of leaky pipes: Toward Comprehensive Picture " {3}: Chappallaz et al., 1992, "Manual on pumps used as turbines"

Figure 1 :

 1 Figure 1: Installation's scheme

Table 1 :

 1 Flow conditions of Gallets sites

		Flow rate (l/s)	Head (m)	Load factor (h/year) E lost (MWh/year)	Producible (MWh/year) H 2 Producible (kg H 2 /year)
	Gallets Haut	208	11	7366	165,7	107,705	1795
	Gallets Bas	100	19	6647	137,6	89,44	1490