Irene Márquez-Corbella

Edgar Martínez-Moro

Ruud Pellikaan
email: g.r.pellikaan@tue.nl

The non-gap sequence of a subcode of a generalized Reed-Solomon code

Keywords: Berger-Loidreau cryptosystem, square code, GRS codes, gaps of a code

.

Introduction

The notion of a Public-Key Cryptosystem (PKC) was first introduced in 1976 by Diffie and Hellman in [START_REF] Diffie | New Directions in Cryptography[END_REF]. Most PKC are based on hard number-theoretic problems such as integer factorization (like the RSA cryptosystem) or taking discrete logarithms in finite groups (like the El Gamal cryptosystem).

In [START_REF] Mceliece | A public-key cryptosystem based on algebraic coding theory[END_REF] McEliece introduced the first PKC based on the theory of errorcorrecting codes which resist precisely the attacks to which the RSA and El Gamal cryptosystem are vulnerable. This property makes McEliece scheme an interesting candidate for post-quantum cryptography (see [START_REF] Overbeck | Code-based cryptography[END_REF]2] for an overview of the state of the art). Later, Niederreiter presents a dual version of the previous cryptosystem which is equivalent in terms of security (see [START_REF] Li | On the equivalence of McEliece's and Niederreiter's public-key cryptosystems[END_REF]). In its original paper [START_REF] Niederreiter | Knapsack-type crypto systems and algebraic coding theory[END_REF] Niederreiter proposed the class of Generalized Reed-Solomon (GRS) codes over F 2 m . However, Sidelnikov and Shestakov in [START_REF] Sidelnikov | On the insecurity of cryptosystems based on generalized Reed-Solomon codes[END_REF] introduced an algorithm that, in polynomial time, permits us to discover the structure of the secret GRS code used in the cryptosystem. Therefore, the initial Niederreiter scheme is completely broken.

That is why Berger and Loidreau in [START_REF] Berger | How to mask the structure of codes for a cryptographic use[END_REF] propose another version of the Niederreiter scheme which is designed to resist the Sidelnikov-Shestakov attack. The main idea of this variant is to work with subcodes of the original GRS code rather than using the complete GRS code.

However, in [START_REF] Wieschebrink | An attack on the modified Niederreiter encryption scheme[END_REF] Wieschebrink presents the first feasible attack to the Berger-Loidreau cryptosystem that allows us to recover the secret key if the chosen subcode is large enough, which is impractical for small subcodes. Furthermore, in [START_REF] Wieschebrink | Cryptoanalysis of the Niederreiter public key scheme based on GRS subcodes[END_REF] Wieschebrink notes that if the double code of a subcode of a GRS code of parameters [n, k] is itself a GRS code of dimension 2k-1 (what he says that seems to happen with high probability) then we can apply the Sidelnikov-Shestakov attack and thus reconstruct the secret key in polynomial time.

The main task of this paper is to confirm the previous question and give a characterization of the possible parameters that should be used to avoid attacks on the Berger-Loidreau cryptosystem.

The structure of this paper is as follows. First we give a brief review of basic concepts from Coding Theory that are relevant to this work and thus establish the notation that will be used throughout the paper. Furthermore, after discussing about the basic attributes and structure of GRS Codes we introduce the non-gap sequence associated to subcodes of such codes and we define some properties that characterize these subcodes in terms of this sequence. The final result of this section even allows us to count the number of subcodes of a GRS code if we identify all possible associated non-gap sequence.

The main objective of the second section is to study the probability that an arbitrary subcode of a GRS code is itself a GRS code. To achieve our goal it would be enough to analyze the non-gaps sequences associated to subcodes with the required properties, which provides an upper bound on the number of such subcodes and, consequently, we could estimate the probability of the occurrence that we are looking for.

Finally we introduce the square code of a subcode of a GRS code. Wieschebrink in [START_REF] Wieschebrink | Cryptoanalysis of the Niederreiter public key scheme based on GRS subcodes[END_REF] stated that this code is often a GRS code. In the last section we give some clues on how to solve this question but the final result will appear in a subsequent paper. However, we establish some properties that the non-gap sequence of the analyzed subcode must verify to have a square code which is a GRS code and has dimension 2k -1. Therefore, the weak subcodes for the Berger-Loidreau cryptosystem are completely characterized.

In order to shorten this abstract we will show all the results without proofs.

Gaps of a code

Let us start fixing the notation and introducing some basic definitions and some known results from coding theory. Let F q be a finite field with q elements and let n, k ∈ N such that 1 ≤ k ≤ n ≤ q.

We define the set

L k = {f ∈ F q [X] : deg(f (X)) ≤ k -1}.
Then for each a, b ∈ F n q the evaluation map at these elements is given by:

ev a,b : L k -→ F n q f → ev a,b (f (X)) = (f (a 1 )b 1 , . . . , f (a n )b n )
We will denote the map ev a,b by ev a if b is the all one vector. For all vector b ∈ (F q \ {0}) n this evaluation map is injective, since f ∈ L k has at most k ≤ n zeros.

Let a be a vector of mutually distinct elements of F q and b a vector consisting of n nonzero entries of F q then the generalized Reed-Solomon code (or

GRS code) is defined by GRS k (a, b) := {ev a,b (f (X)) : f ∈ L k }.
That is, for every codeword c ∈ GRS k (a, b) there exists a unique polynomial

f c ∈ L k , known as polynomial associated to c, such that c = ev a,b (f c (X)).
For a, b ∈ F n q we define the Schur or star product a * b ∈ F n q by:

a * b = (a 1 • b 1 , . . . , a n • b n ) .
Let 1 be the all one vector.

Then GRS k (a, b) = b * GRS k (a, 1). Furthermore ev a,b (f (X)g(X)) = ev a,1 (f (X)) * ev a,b (g(X)).
From now on, let l be an integer such that 1 ≤ l ≤ k ≤ n ≤ q then C denotes an l-dimensional subcode of the code GRS k (a, b) and we denote by

C i = C i (a, b) := C ∩ GRS i (a, b).
We have the following nice embedding property:

C 0 ⊆ C 1 ⊆ . . . ⊆ C k = C ∩ GRS k (a, b) = C. Definition 1. i ∈ Z ≥0 is called an (a, b)-gap of the code C or simply a gap of C if C i = C i+1 .
The next Proposition show us how to identify all the (a, b) non-gaps of any l-dimensional subcode of the code GRS k (a, b).

Proposition 1. i ∈ Z ≥0 is an (a, b) non-gap of C if and only if there exists f ∈ F q [X] with deg(f (X)) = i such that ev a,b (f (X)) ∈ C.
We define an associated (a, b) non-gap sequence of C by

I(C, a, b) = I(C) = {i ∈ Z ≥0 : i is a non-gap of C}.
Using the previous characterization proposition we have the following result that allows us to define any subcode C ⊆ GRS k (a, b) as the subspace generated by polynomials in F q [X] whose degree is an element of the associated (a, b) non-gap sequence of C. Corollary 1. Let C be an l-dimensional subcode of the code GRS k (a, b) with associated non-gap sequence I(C). Then:

1. I(C) = {i : ∃f ∈ F q [X] with deg(f (X)) = i < k such that ev a,b (f (X)) ∈ C}. 2. C = {ev a,b (f (X)) : f = 0 or f ∈ F q [X] and deg(f (X)) ∈ I(C)}.
Furthermore applying elementary operations to the above result we obtain a basis of any l-dimensional subcode C ⊆ GRS k (a, b) just studying the associated (a, b) non-gap sequence of C. Proposition 2. There is a set I consisting of the strictly increasing sequence of non-negative integers i 1 , . . . , i l and there are polynomials f 1 , . . . , f l in the unique normal form Therefore Proposition 2 allows us to count the number of l-dimensional subcodes C by identifying all possible associated non-gaps sequences (i.e. analyzing all subsets of the set of integers {0, . . . , k -1}). Proposition 3. Let I be a set consisting of the strictly increasing sequence of non-negative integers i 1 , . . . , i l . Let

f j (X) = X ij + s<ij s / ∈I f j,s X s ∈ F q [X], for all j = 1, . . . , l,
e(I) = i 1 l + (i 2 -i 1 -1)(l -1) + • • • + (i l -i l-1 -1) = l s=1 (i s -i s-1 -1)(l -s + 1)
where i 0 = -1. Then the number of l-dimensional subcodes of the code GRS k (a, b) over F q with a given non-gap sequence I is equal to q e(I) .

The number e(I) is minimal and equal to 0 for I = {0, 1, . . . , l -1} and it is maximal and equal to l(kl) for I = {kl, . . . , k -2, k -1}.

Accordingly to a well-known result and by Proposition 3 we have that the number of l-dimensional subcodes of the code GRS k (a, b) over F q is equal to the Gaussian binomial:

(q k -1)(q k -q) • • • (q k -q l-1 ) (q l -1)(q l -q) • • • (q l -q l-1 ) := k l q = I⊆{0,...,k-1} |I|=l q e(I)
.

Hence this number is polynomial in q with non-negative integers as coefficients.

GRS subcodes of GRS codes

In this section we study the particular case of l-dimensional subcodes C of the code GRS k (a, b) that are themselves GRS codes. The simplest case is when C = GRS l (a, b) with 2 ≤ l ≤ k. The result presented bellow characterize uniquely such subcodes. Corollary 2. There is exactly one l-dimensional subcode of the code GRS k (a, b) over F q with non-gap sequence {0, . . . , l -1}, that is GRS l (a, b).

Another special case is when C = GRS l (a, a i * b) with i+l < k. The following results allow us to give an upper bound on the number of such subcodes. Proposition 5. Let i l be the largest non-gap of C and let c = ev a (f (X))

for f ∈ F q [X] of degree i. If i + i l < k, then I(c * C) = i + I(C).
Let us define a i by induction: a 0 = 1, a 1 = a and a i+1 = a * a i .

Corollary 3. If i + l ≤ k, then the non-gap sequence of the code GRS l (a, a i * b) is equal to {i, i + 1, . . . , i + l -1}.
Note that the converse is not true in general.

Corollary 4. The number of l-dimensional subcodes of the code GRS k (a, b) over F q with l consecutive non-gaps is equal to

k l=1 k-l i=0 q il .
Now we consider the general case i.e. we consider C = GRS l (c, d) an ldimensional subcode of the code GRS k (a, b). First we give the necessary conditions that C must verified to be a subcode of the code GRS l (a, b) and how is its associated non-gap sequence. Then, with an additional assumption, we show the converse (which are the necessary conditions that the associated non-gap sequence of C must verified to be a subcode of the code GRS k (a, b)). With these two results we can give an upper bound on the number of such subcodes. Proposition 6. Let l ≥ 2 and let a be a vector of n mutually distinct elements of F q and b a vector consisting of n nonzero entries of F q . Let g 0 , h 1 ∈ F q [X]. Let d 0 = deg(g 0 (X)) and d 1 = d 0 + deg(h 1 (X)). Suppose that ev a (h 1 (X)) = c is a vector of n mutually distinct elements of F q and ev a,b (g 0 (X)) = d is a vector consisting of nonzero entries. If

d 0 < d 1 and d 0 + (l -1)(d 1 -d 0 ) < k, then GRS l (c, d) is an l dimensional subcode of the code GRS k (a, b) with (a, b) non-gap sequence: d 0 , . . . , d 0 + j(d 1 -d 0 ), . . . , d 0 + (l -1)(d 1 -d 0 ).
If 2k -2 < n and l ≥ 2, then there is a converse of the above Proposition given by the following result. c,d) where c is a vector of n mutually distinct elements of F q and d is a vector consisting of nonzero entries. Then there exist g

0 , h 1 ∈ F q [X] such that d 0 = deg(g 0 (X)), d 1 = d 0 + deg(h 1 (X)), ev a (h 1 (X)) = c and ev a,b (g 0 (X)) = d.
Corollary 5. If 2k -2 < n and 2 ≤ l ≤ k. Then the number of l-dimensional subcodes of the code GRS k (a, b) over F q that are a GRS code is at most q k-l+3 .

With the previous assumptions i.e. let 2 ≤ l ≤ k and 2k -2 < n ≤ q, then Corollary 5 and Proposition 3 imply that the probability that an arbitrary l-dimensional subcode of the code GRS k (a, b) is a generalized Reed-Solomon code is at most

q k-l+3 k l q ≤ q k-l+3 q l(k-l) = q -(l-1)(k-l)+3
This fraction tends to zero for k → ∞ or (kl) → ∞.

4 The square of a code Definition 2. We define the square code of a [n, k] linear code C over F q and we denoted by D = C * C as the code generated by the set {r i * r j : 1 ≤ i ≤ j ≤ k} where r 1 , . . . , r k denotes the rows of a generator matrix of the code C. Now let C be an l-dimensional subcode of the code GRS k (a, b), let r 1 , . . . , r l be the rows of a generator matrix of C and let f 1 , . . . , f l be the polynomials associated to those rows, then r i * r j for all i, j ∈ {1, . . . , l} has the form:

r i * r j = b 2 1 f i (a 1 )f j (a 1 ), . . . , b 2 n f i (a n )f j (a n ) where deg(f i (X)f j (X)) = deg(f i (X)) + deg(f j (X)) ≤ 2k -2. That is, the code D = C * C := r i * r j : 1 ≤ i ≤ j ≤ j is a subcode of the code GRS 2k-1 (a, b * b).
Similarly to what we did in the previous section we denote by

D i = D i (a, b * b) := D ∩ GRS i (a, b * b). In this case i ∈ Z ≥0 is called an (a, b * b) gap of D if D i = D i+1 .
Define the following set of non-gaps

J (D) = {j ∈ Z ≥0 : j is an (a, b * b) non-gap of D}.
From now on we assume that k, l are integers such that 2 ≤ l ≤ k ≤ n ≤ q and 2k -1 ≤ n.

(X)) ∈ C for f ∈ F q [X] of degree i 1 .
Then, if i 1 + i l < 2k -1, we have that

I(c * C) = i 1 + I(C) ⊆ J (D).
However, the previous equality does not hold in general.

I(C) ⊆ d 0 2 , . . . , d 0 + (r -1)(d 1 -d 0 ) 2
where d 0 < d 1 and d 0 + (r -1)(d 1 -d 0 ) < 2k -1.
The aim of this section is to obtain a characterization of the l-dimensional subcodes C of the code GRS k (a, b) such that its square code is exactly the code GRS 2k-1 (a, b * b).

The first possibility occurs when C is itself a GRS code. The following two results are related to this special case.

GRS 2k-1 (a, b * b), then |{ (u, v) : i u + i v ≥ t and 1 ≤ u ≤ v ≤ l }| ≥ 2k -t -1 for all t = 0, . . . , 2k -2.
which is in agreement with Proposition 10. 2. The cases t = 2k -2, t = 2k -3 and t = 2k -5 imply that i Assume that we have two polynomials f (X), g(X) ∈ L k , that is, both polynomials can be written as:

l = k -1, i l-1 = k -2 and i l-2 ≥ k -4.
f (X) = k-1 r=0 f r X r and g(X) = k-1 s=0 g s X s
with f r , g s ∈ F q for r, s ∈ {0, . . . , k -1}.

The product of these polynomials give us another polynomial in L 2k-2

f (X)g(X) = h(X) = h 0 + h 1 X + . . . + h 2k-2 X 2k-2 ∈ L 2k-2 .
This can be expressed in matrix form as follows:

R(f )S(g) T =           h 2k-2 h 2k-3 . . . h k-1 . . . h 0          
, where R(f ) is a matrix of size (2k -1) × (3k -2) over F q with the following form:

R(f ) =           f 0 f 1 • • • f k-1 0 • • • 0 0 • • • 0 0 f 0 • • • f k-2 f k-1
0 0 • • • 0 0 • • • f 0 f 1 • • • f k-1          
and S(g) is a matrix of size 1 × (3k -2) over F q with S(g) = ( 0

• • • 0 k-1 g k-1 • • • g 0 0 • • • 0 k-1
).

  such that the evaluation of these elements with respect to (a, b) form a basis of the code C. Furthermore I(C) = I and dim(C) = |I(C)|.

Proposition 4 .

 4 C = GRS l (a, b) if and only if I(C) = {0, . . . , l -1}.

Proposition 7 .

 7 Let d 0 < d 1 be the first two elements of the (a, b) non-gap sequence of C and suppose that C = GRS l (

Remark 1 .

 1 i is an (a, b * b) non-gap of D if and only if there exists a polynomial g ∈ F q [X] with deg(g(X)) = i such that ev a,b * b (g(X)) ∈ D. This result is directly consequence of Proposition 1. Next Proposition shows the relationship between the (a, b) non-gap sequence associated to the subcode C, i.e. I(C), and the (a, b * b) non-gap sequence associated to the square code D, i.e. J (D).

Proposition 8 .

 8 I(C) + I(C) = {i + j : i, j ∈ I(C)} ⊆ J (D). Furthermore: 1. If 0 is an (a, b) non-gap of C then I(C) ⊆ J (D). 2. Otherwise let i 1 , i l be the first and last element, respectively of the (a, b) non-gap sequence of C. Let c = ev a,b (f

Proposition 9 . 2 . 3 .

 923 dim(D) ≤ min{2k -1, l+1 2 }. Furthermore: 1. If D = GRS r (a, b * b) then the associated (a, b) non-gap sequence of the code C verifies that I(C) ⊆ {0, . . . , ⌊ r-1 2 ⌋}. 2. If D = GRS r (a, a i * b * b) then the associated (a, b) non-gap sequence of the code C verifies that I(C) ⊆ i 2 , . . . , i + r -1 If D = GRS r (c, d) then the associated (a, b) non-gap sequence of the code C verifies that

Proposition 10 .Corollary 6 .

 106 GRS k (a, b) * GRS l (a, c) = GRS k+l-1 (a, b * c). In particular, GRS 2l-1 (a, b * b) the square of the code GRS l (a, b). If the associated (a, b) non-gap sequence of the subcode C is precisely I(C) = {0, . . . , l -1} then the (a, b * b) non-gap sequence associated to the square code D is J (D) = {0, . . . , 2l -2}, that is D = GRS 2l-2 (a, b * b). The converse is not true in general. Next Proposition determines a property that must verified all the elements of the (a, b) non-gap sequence of C to have that the square code D is exactly the code GRS 2k-1 (a, b * b). Proposition 11. Let the increasing sequence i 1 , . . . , i l be an enumeration of the (a, b) non-gap sequence of C. If the square of C is equal to

Remark 3 .

 3 If I(C) = {kl, . . . , k -1}, then this non-gap sequence satisfies the conditions of Proposition 11 for all t. However not all the square codes of a subcode C of the code GRS k (a, b) with such associated non-gap sequence are exactly the code GRS 2k-1 (a, b * b). A case example is the subcode C = ev a,b (X i ) : i = kl, . . . , k -1 .

Remark 2. If the square code of C is equal to GRS 2k-1 (a, b * b), then:

1. The special case t = 0 of Proposition 11 implies that 2k -1 ≤ l+1 Now let C be an l-dimensional subcode of the code GRS k (a, b) with associated (a, b) non-gap sequence I(C) = {i 1 , . . . , i l } then by Proposition 2 there exists l polynomials f j ∈ L k for j ∈ {1, . . . , l} in normal form of degree i j such that C = ev a,b (f 1 (X)), . . . , ev a,b (f l (X)) .

Furthermore we know that the elements ev a,b * b (f u (X)f v (X)) generate the double code of C, denoted by D with 1 ≤ u ≤ v ≤ l.

If we denote by

the polynomial obtained by multiplying the polynomials f u and f v for 1 ≤ u ≤ v ≤ l then the following matrix is a generator matrix of the square code D.

. . . . . . . . . . . . . . . . . . . . . . . .

where G D is a matrix of size (2k -1) × l+1 2 over F q .

We define

Then RS T = G D .

Remark 4. The following properties are necessary conditions to have that the square code D of the code C is the code GRS 2k-1 (a, b * b).

3. The matrix G D has full rank, i.e. rank(R(f 1 ), . . . , R(f l )) = 2k -1.

We are aiming to prove in a subsequent paper that the square of almost all l-dimensional subcodes of GRS k (a, b) is equal to GRS 2k-1 (a, b).


Pierre Ganty

Rupak Majumdar

Benjamin Monmege

Bounded Underapproximations

We show a new and constructive proof of the following language-theoretic result: for every context-free language L, there is a bounded context-free language L ⊆ L which has the same Parikh (commutative) image as L. Bounded languages, introduced by Ginsburg and Spanier, are subsets of regular languages of the form w * 1 w * 2 • • • w * k for some w1, . . . , w k ∈ Σ * . In particular bounded context-free languages have nice structural and decidability properties. Our proof proceeds in two parts. First, using Newton's iterations on the language semiring, we construct a context-free subset LN of L that can be represented as a sequence of substitutions on a linear language and has the same Parikh image as L. Second, we inductively construct a Parikh-equivalent bounded contextfree subset of LN . As an application of this result in model checking, we show how to underapproximate the reachable state space of multithreaded procedural programs. The bounded language constructed above provides a decidable underapproximation for the original problem. By iterating the construction, we get a semi-algorithm for the original problems that constructs a sequence of underapproximations such that no two underapproximations of the sequence can be compared. This provides a progress guarantee: every word w ∈ L is in some underapproximation of the sequence, and hence, a program bug is guaranteed to be found. In particular, we show that verification with bounded languages generalizes context-bounded reachability for multithreaded programs.

Introduction

Many problems in program analysis reduce to undecidable problems about context-free languages. For example, checking safety properties of multithreaded recursive programs reduces to checking emptiness of the intersection of contextfree languages [START_REF] Ramalingam | Context-sensitive synchronization-sensitive analysis is undecidable[END_REF][START_REF] Bouajjani | A generic approach to the static analysis of concurrent programs with procedures[END_REF].

We study underapproximations of these problems, with the intent of building tools to find bugs in systems. In particular, we study underapproximations in which one or more context-free languages arising in the analysis are replaced by their subsets in a way that (P1) the resulting problem after the replacement becomes decidable and (P2) the subset preserves "many" strings from the original language. Condition (P1) ensures that we have an algorithmic check for the underapproximation. Condition (P2) ensures that we are likely to retain behaviors that would cause a bug in the original analysis.

We show in this paper an underapproximation scheme using bounded languages [START_REF] Ginsburg | Bounded ALGOL-like languages[END_REF][START_REF] Ginsburg | The Mathematical Theory of Context-Free Languages[END_REF]. A language L is bounded if there exist k ∈ N and finite words w 1 , w 2 , . . . , w k such that L is a subset of the regular language w * 1 • • • w * k . In particular, context-free bounded languages (hereunder bounded languages for short) have stronger properties than general context-free languages: for example, it is decidable to check if the intersection of a context-free language and a bounded language is non-empty [START_REF] Ginsburg | Bounded ALGOL-like languages[END_REF]. For our application to verification, these decidability results ensure condition (P1) above.

The key to condition (P2) is the following Parikh-boundedness property: for every context-free language L, there is a bounded language L ⊆ L such that the Parikh images of L and L coincide. (The Parikh image of a word w maps each symbol of the alphabet to the number of times it appears in w, the Parikh image of a language is the set of Parikh images of all words in the language.) A language L meeting the above conditions is called a Parikh-equivalent bounded subset of L. Intuitively, L preserves "many" behaviors as for every string in L, there is a permutation of its symbols that matches a string in L .

The Parikh-boundedness property was first proved in [START_REF] Latteux | Une propriété de la famille GRE[END_REF][START_REF] Blattner | Parikh-bounded languages[END_REF], however, the chain of reasoning used in these papers made it difficult to see how to explicitly construct the Parikh-equivalent bounded subset. Our paper gives a direct and constructive proof of the theorem. We identify two contributions in this paper. Explicit construction of Parikh-equivalent bounded subsets. Our constructive proof has two parts. First, using Newton's iteration [START_REF] Esparza | On fixed point equations over commutative semirings[END_REF] on the semiring of languages, we construct, for a given context-free language L, a finite sequence of linear substitutions which denotes a Parikh-equivalent (but not necessarily bounded) subset of L. (A linear substitution maps a symbol to a language defined by a linear grammar, that is, a context-free grammar where each rule has at most one non-terminal on the right-hand side.) The Parikh equivalence follows from a convergence property of Newton's iteration on the related commutative semiring.

Second, we provide a direct constructive proof that takes as input such a sequence of linear substitutions, and constructs by induction a Parikh-equivalent bounded subset of the language denoted by the sequence.

Reachability analysis of multithreaded programs with procedures. Using the above construction, we obtain a semi-algorithm for reachability analysis of multithreaded programs with the intent of finding bugs. To check if configuration (c 1 , c 2 ) of a recursive 2-threaded program is reachable, we construct the context-free languages L 0 1 = L(c 1 ) and L 0 2 = L(c 2 ) respectively given by the execution paths whose last configurations are c 1 and c 2 , and check if either

L 1 ∩ L 0 2 or L 0 1 ∩ L 2 is non-empty, where L 1 = L 0 1 ∩ w * 1 • • • w * k and L 2 = L 0 2 ∩ v * 1 • • • v * l
are two Parikh-equivalent bounded subsets of L 0 1 and L 0 2 , respectively. If either intersection is non-empty, we have found a witness trace. Otherwise, we construct

L 1 1 = L 0 1 ∩ w * 1 • • • w * k and L 1 2 = L 0 2 ∩ v * 1 • • • v *
l in order to exclude, from the subsequent analyses, the execution paths we already inspected. We continue by rerunning the above analysis on L 1 1 and L 1 2 . If (c 1 , c 2 ) is reachable, the iteration is guaranteed to terminate; if not, it could potentially run forever. Moreover, we show our technique subsumes and generalizes context-bounded reachability [START_REF] Qadeer | Context-bounded model checking of concurrent software[END_REF].

We omit proofs for space reasons. Detailed proofs, as well as one more application of our result, can be found in [START_REF] Ganty | Bounded Underapproximations[END_REF].

Related Work. Bounded languages were introduced and studied by Ginsburg and Spanier [START_REF] Ginsburg | Bounded ALGOL-like languages[END_REF] (see also [START_REF] Ginsburg | The Mathematical Theory of Context-Free Languages[END_REF]). The existence of a bounded, Parikh-equivalent subset for a context-free language was shown in [START_REF] Blattner | Parikh-bounded languages[END_REF] using previous results on languages in the Greibach hierarchy [START_REF] Latteux | Une propriété de la famille GRE[END_REF]. The existence of a language representable as a sequence of linear transformations of a linear language which is Parikh-equivalent to a context-free language was independently shown in [START_REF] Esparza | Newton's Method for ω-Continuous Semirings[END_REF].

Bounded languages have been recently proposed by Kahlon for tractable reachability analysis of multithreaded programs [START_REF] Kahlon | Tractable analysis for concurrent programs via bounded languages[END_REF]. His observation is that in many practical instances of multithreaded reachability, the languages are actually bounded. If this is true, his algorithm checks the emptiness of the intersection (using the algorithm in [START_REF] Ginsburg | Bounded ALGOL-like languages[END_REF]). In contrast, our results are applicable even if the boundedness property does not hold.

For multithreaded reachability, context-bounded reachability [START_REF] Qadeer | Context-bounded model checking of concurrent software[END_REF][START_REF] Suwimonteerabuth | Symbolic Context-Bounded Analysis of Multithreaded Java Programs[END_REF] is a popular underapproximation technique which tackles the undecidability by limiting the search to those runs where the active thread changes at most k times. Our algorithm using bounded languages subsumes context-bounded reachability, and can capture unboundedly many synchronizations in one analysis. We leave the empirical evaluation of our algorithms for future work.

Preliminaries

We assume the reader is familiar with the basics of language theory (see [START_REF] Hopcroft | Introduction to Automata Theory, Languages, and Computation[END_REF]). An alphabet Σ is a finite non-empty set of symbols. The concatenation L • L of two languages L, L ⊆ Σ * is defined using word concatenation as

L • L = {l • l | l ∈ L ∧ l ∈ L }.
An elementary bounded language over Σ is a language of the form w

* 1 • • • w * k for some fixed w 1 , . . . , w k ∈ Σ * .
Vectors. For p ∈ N, we write Z p and N p for the set of p-dim vectors (or simply vectors) of integers and naturals, respectively. We write 0 for the vector (0, . . . , 0) and e i the vector (z 1 , . . . , z p ) ∈ N p such that z j = 1 if j = i and z j = 0 otherwise. Addition on p-dim vectors is the componentwise extension of its scalar counterpart, that is, given (x 1 , . . . , x p ), (y 1 , . . . , y p ) ∈ Z p (x 1 , . . . , x p ) + (y 1 , . . . , y p ) = (x 1 + y 1 , . . . , x p + y p ). Using vector addition, we define the operation on sets of vectors as follows: given Z, Z ⊆ N p , let

Z Z = {z + z | z ∈ Z ∧ z ∈ Z }.
Parikh Image. Give Σ a fixed linear order: Σ = {a 1 , . . . , a p }. The Parikh image of a symbol a i ∈ Σ, written Π Σ (a i ), is e i . The Parikh image is extended to words of Σ * as follows:

Π Σ (ε) = 0 and Π Σ (u • v) = Π Σ (u) + Π Σ (v). Finally,
the Parikh image of a language on Σ * is the set of Parikh images of its words. Thus, the Parikh image maps 2 Σ * to 2 N p . We also define the inverse of the Parikh image

Π -1 Σ : 2 N p → 2 Σ * as follows: given a subset M of N p , Π -1 Σ (M ) is the set {y ∈ Σ * | ∃m ∈ M : m = Π Σ (y)}.
When it is clear from the context we generally omit the subscript in Π Σ and Π -1 Σ . Context-free Languages. A context-free grammar G is a tuple (X , Σ, δ) where X is a finite non-empty set of variables (non-terminal letters), Σ is an alphabet of terminal letters and δ ⊆ X × (Σ ∪ X ) * a finite set of productions (the production (X, w) may also be noted X → w). Given two strings u, v ∈ (Σ ∪ X ) * we define the relation u ⇒ v, if there exists a production (X, w) ∈ δ and some words y, z ∈ (Σ ∪ X ) * such that u = yXz and v = ywz. We use ⇒ * for the reflexive transitive closure of ⇒. A word w ∈ Σ * is recognized by the grammar G from the state X ∈ X if X ⇒ * w. Given X ∈ X , the language L X (G) is given by {w ∈ Σ * | X ⇒ * w}. A language L is context-free (written CFL) if there exists a context-free grammar G = (X , Σ, δ) and an initial variable X ∈ X such that is L = L X (G). A linear grammar G is a context-free grammar where each production is in X × Σ * (X ∪ {ε})Σ * . A language L is linear if L = L X (G) for some linear grammar G and initial variable X of G. A CFL L is bounded if it is a subset of some elementary bounded language. Proof Plan. The main result of the paper is the following. Theorem 1. For every CFL L, there is an effectively computable CFL L such that (i) L ⊆ L, (ii) Π(L) = Π(L ), and (iii) L is bounded.

We actually solve the following related problem in our proof.

Problem 1. Given a CFL L, compute an elementary bounded language B such that Π(L ∩ B) = Π(L).

If we can compute such a B, then we can compute the CFL L = B ∩ L which satisfies conditions (i) to (iii) of the Th. 1. Thus, solving Pb. 1 proves the theorem constructively.

We solve Pb. 1 for a language L as follows: (1) we find an L such that L ⊆ L, Π(L ) = Π(L), and L has a "simple" structure (Sect. 3) and (2) then show how to find an elementary bounded B with Π(L ∩ B) = Π(L ), assuming this structure (Sect. 4). Observe that if L ⊆ L and Π(L) = Π(L ), then for every elementary bounded B, we have 2) is a solution for L as well. Section 5 provides an application of the result for multithreaded program analysis and compares it with an existing technique.

Π(L ∩ B) = Π(L ) implies Π(L ∩ B) = Π(L) as well. So the solution B for L in step (
Semiring. A semiring S is a tuple S, ⊕, , 0, 1 , where S is a set with 0, 1 ∈ S, S, ⊕, 0 is a commutative monoid with neutral element 0, S, , 1 is a monoid with neutral element 1, 0 is an annihilator w.r.t. , i.e. 0 a = a 0 = 0 for all a ∈ S, and distributes over ⊕, i. Parikh Semiring. The tuple P = 2 N p , ∪, , ∅, {0} is the idempotent ωcontinuous commutative semiring of Parikh vectors. The natural order is again given by ⊆.

Valuation, polynomial.

In what follows, let X be a finite set of variables and S = S, ⊕, , 0, 1 be an ω-continuous semiring.

A valuation v is a mapping X → S. We denote by S X the set of all valuations and by 0 the valuation which maps each variable to 0. We define . ⊆ S X × S X as the order given by v . v if and only if v(X) v (X) for every X ∈ X . A monomial is a mapping S X → S given by a finite expression

m = a 1 X 1 a 2 • • • a k X k a k+1 where k ≥ 0, a 1 , . . . , a k+1 ∈ S and X 1 , . . . , X k ∈ X such that m(v) = a 1 v(X 1 ) a 2 • • • a k v(X k ) a k+1 for v ∈ S X . A polynomial is a finite combination of monomials: f = m 1 ⊕ • • • ⊕ m k
where k ≥ 0 and m 1 , . . . , m k are monomials. The set of polynomials w.r.t. S and X will be denoted by S[X ]. Finally, a polynomial transformation F is a mapping S X → S X described by the set {F X ∈ S[X ] | X ∈ X } of polynomials: hence, for every vector v ∈ S X , F (v) is a valuation of each variable X ∈ X to F X (v). Least Fixpoint. Recall that a mapping f :

S → S is monotone if a b im- plies f (a)
f (b), and continuous if for any infinite chain a 0 , a 1 , a 2 , . . . we have sup{f (a i )} = f (sup{a i }). The definition can be extended to mappings F : S X → S X in the obvious way (using .

). Then we may formulate the following proposition (cf. [START_REF] Kuich | Semirings and formal power series: their relevance to formal languages and automata[END_REF]). Proposition 1. Let F be a polynomial transformation. The mapping induced by F is monotone and continuous and F has a unique least fixpoint µF .

Fixpoints of polynomial transformations relates to CFLs as follows. Given a grammar G = (X , Σ, δ), let L(G) be the valuation which maps each variable X ∈ X to the language L X (G). We first characterize the valuation L(G) as the least fixpoint of a polynomial transformation F defined as follows: each F X of F is given by the combination of α's for (X, α) ∈ δ where α is interpreted as a monomial on the semiring L. From [START_REF] Chomsky | The algebraic theory of context-free languages[END_REF] we know that L(G) = µF .

Example 1. Let G = ({X 0 , X 1 }, {a, b}, δ) where δ = {(X 0 → aX 1 |a), (X 1 → X 0 b|aX 1 bX 0 )}. It defines the polynomial transformation F on L X such that F X0 = a • X 1 ∪ a and F X1 = X 0 • b ∪ a • X 1 • b • X 0 ,
and L(G) is the least fixpoint of F in the language semiring.

Relating the Language and Parikh Semirings

Given a polynomial transformation F , we now characterize the relationship between the least fixpoints µF taken over the language and the Parikh semiring, respectively. Either fixpoint is given by the limit of a sequence of iterates which is defined by Newton's iteration scheme [START_REF] Esparza | An extension of Newton's method to ω-continuous semirings[END_REF][START_REF] Esparza | On fixed point equations over commutative semirings[END_REF]. Our characterization operates at the level of those iterates: we inductively relate the iterates of each iteration sequence (over the Parikh and language semirings). We use Newton's iteration instead of the usual Kleene's iteration sequence because Newton's iteration is guaranteed to converge on the Parikh semiring in a finite number of steps, a property that we shall exploit. Kleene's iteration sequence, on the other hand, may not converge. Due to lack of space, we refer the reader to [START_REF] Esparza | An extension of Newton's method to ω-continuous semirings[END_REF][START_REF] Esparza | On fixed point equations over commutative semirings[END_REF] for the definition of Newton's iteration scheme.

We first extend the definition of the Parikh image to a valuation v ∈ L X as the valuation of P X defined for each variable X by: Π(v)(X) = Π(v(X)). Then, given F L : L X → L X , a polynomial transformation, we define a polynomial transformation F P : P X → P X such that: for every X ∈ X we have F P X = Π • F LX • Π -1 . Lemma. 1 relates the iterates for µF L and µF P using the Parikh image mapping.

Lemma 1. Let (ν i ) i∈N and (κ i ) i∈N be Newton's iteration sequences associated with F L and F P , respectively. For every i ∈ N, we have Π(ν i ) = κ i .

In [START_REF] Esparza | On fixed point equations over commutative semirings[END_REF], the authors show that Newton's iterates converges after a finite number of steps when defined over a commutative ω-continuous semiring. This shows, in our setting, that (κ i ) i∈N stabilizes after a finite number of steps.

Lemma 2. Let (κ i ) i∈N be Newton's iteration sequence associated to F P and let n be the number of variables in X . For every k ≥ n, we have

κ k = Π(µF L ). Hence, for every k ≥ n, Π(ν k ) = Π(µF L ).
We know Newton's iteration sequence (ν i ) i∈N , whose limit is µF L , may not converge after a finite number of iterations. However, using Lem. 2, we know that the Parikh image of the iterates stabilizes after a finite number of steps. Precisely, if n is the number of variables in X , then the language given by ν n is such that Π(ν n ) = Π(L(G)). Moreover because (ν i ) i∈N is an ascending chain, for each variable X ∈ X , we have that ν n (X) is a sublanguage of L X (G) such that Π(ν n (X)) = Π(L X (G)).

Representation of Iterates

We now show that Newton's iterates can be effectively represented as a combination of linear grammars and homomorphisms.

A substitution σ from alphabet Σ 1 to alphabet Σ 2 is a function which maps every word over Σ 1 to a set of words of Σ * 2 such that σ(ε) = {ε} and σ(u

• v) = σ(u) • σ(v).
A homomorphism h is a substitution such that for each word u, h(u) is a singleton. We define the substitution σ [a/b] : Σ 1 ∪ {a} → Σ 1 ∪ {b} which maps a to b and leaves all other symbols unchanged. We show below that the iterates (ν k ) k≤n have a "nice" representation. k-fold composition. We effectively compute and represent each iterate as the valuation which maps each variable X to the language generated by a k-fold composition of a substitution. Since the substitution maps each symbol onto a language which is linear, it is effectively represented and manipulated as a linear grammar. To formally define the representation we need to introduce the following definitions.

Let G = (X , Σ ∪ {v X | X ∈ X }, δ) be a linear grammar and let

k ∈ N, define v k X to be the set of symbols v k X | X ∈ X . Given a language L on alphabet Σ ∪ {v X | X ∈ X }, we define L[v k X ] to be σ [v X /v k X ] X∈X (L) that is the language where each occurence of v X is replaced by v k X . For k ∈ {1, . . . , n}, we define σ k : Σ ∪ v k X → Σ ∪ v k-1 X as the substitution which maps each v k X onto L X ( G)[v k-1
X ] and leaves Σ unchanged. For k = 0 the substitution σ 0 maps each v 0 X on F ( 0)(X) and leaves Σ unchanged. σ 0 basically applies the terminal rules of the grammar. Let k, be such that 0

≤ k ≤ ≤ n we define σ k to be σ k • • • • • σ . Hence, σ k 0 is such that: (Σ ∪ v k X ) * σ k -→ (Σ ∪ v k-1 X ) * • • • (Σ ∪ v 1 X ) * σ1 -→ (Σ ∪ v 0 X ) * σ0
-→ Σ * . Finally, the k-fold composition of a linear grammar G and initial variable X is given by σ k 0 (v k X ). Lemma 3 relates k-fold compositions with (ν k ) k∈N . Moreover we characterize the complexity of computing G given a polynomial transformation F the size of which is defined to be the number of bits needed to write the set {F X } X∈X where each F X is a string of symbols. Lemma 3. Given a polynomial transformation F , there is a polynomial time algorithm to compute a linear grammar G such that for every k ≥ 0, every X ∈ X we have ν k (X) = σ k 0 (v k X ). We refer the reader to our technical report [START_REF] Ganty | Bounded Underapproximations[END_REF] for the polynomial time construction of G given F . However, let us give a sample output of the construction.

Example 2. Let F be a polynomial transformation on L X where F X0 = aX 1 ∪ a and F X1 = X 0 b ∪ aX 1 bX 0 . The construction outputs G = ({X 0 , X 1 }, {a, b, v X0 , v X1 }, δ) where δ is given by:

X 0 → aX 1 | av X1 | a X 1 → X 0 b | aX 1 bv X0 | av X1 bX 0 | v X0 b | av X1 bv X0 . We have that ν 1 (X 0 ) = σ 0 • σ 1 (v 1 X0 ) and ν 1 (X 1 ) = σ 0 • σ 1 (v 1 X1 ).
Lem. 3 completes our goal to define a procedure to effectively compute and represent the iterates (ν k ) k∈N . This sequence is of interest since, given a CFL L and ν n the n-th iterate (where n equals the number of variables in the grammar of L so that Π(ν n ) = Π(L)), if B is a solution to Pb. 1 for the instance ν n , B is also a solution to Pb. 1 for L. Notice that k-fold compositions relate to indexed grammars used to represent Newton iterates in [START_REF] Esparza | Newton's Method for ω-Continuous Semirings[END_REF].

Constructing a Parikh Equivalent Bounded Subset

We now show how, given a k-fold composition L , to compute an elementary bounded language B such that Π(L ∩ B) = Π(B), that is we give an effective procedure to solve Pb. 1 for the instance L . This will complete the solution to Pb. 1, hence the proof of Th. 1. In this section, we give an effective construction of elementary bounded languages that solve Pb. 1 first for regular languages, then for linear languages, and finally for a linear substitution. First we need to introduce the notion of semilinear sets. A set A ⊆ N n is a linear set if there exist c ∈ N n and p 1 , . . . , p k ∈ N n such that A = c + k i=1 λ j p j | λ j ∈ N : c is called the constant of A and p 1 , . . . , p k the periods of A. A semilinear set S is a finite union of linear sets: S = i=1 A i where each A i is a linear set. Parikh's theorem (cf. [START_REF] Ginsburg | The Mathematical Theory of Context-Free Languages[END_REF]) shows that the Parikh image of every CFL is a semilinear set that is effectively computable. Lemma 4. Let L and B be respectively a CFL and an elementary bounded language over Σ such that Π(L ∩ B) = Π(L). There is an effectively computable elementary bounded language B such that Π(L t ∩ B ) = Π(L t ) for all t ∈ N.

Proof. By Parikh's theorem, we know that Π Σ (L) is a computable semilinear set. Let us consider u 1 , . . . , u ∈ L such that Π Σ (u i ) = c i for i ∈ {1, . . . , }.

Let B = u * 1 • • • u * B , we see that B is an elementary bounded language. Let t > 0 be a natural integer. We have to prove that Π(L t ) ⊆ Π(L t ∩ B ). case t ≤ . By property of Π and Π(L) = Π(L ∩ B) we find that:

Π(L t ) = Π((L ∩ B) t ) ⊆ Π(L t ∩ B t ) monotonicity of Π ⊆ Π(L t ∩ B ) B t ⊆ B since ε ∈ B ⊆ Π(L t ∩ B ) def. of B case t > . Let us consider w ∈ L t .
For every i ∈ {1, . . . , } and j ∈ {1, . . . , k i }, there exist some positive integers λ ij and µ i , with i=1 µ i = t such that

Π(w) = i=1 µ i c i + i=1 ki j=1 λ ij p ij .
We define a new variable for each i ∈ {1, . . . , }:

α i = µ i -1 if µ i > 0 0 otherwise. .
For each i ∈ {1, . . . , }, we also consider z i a word of L ∪ {ε} such that

z i = ε if µ i = 0 and Π(z i ) = c i + ki j=1 λ ij p ij else. Let w = u α1 1 . . . u α z 1 . . . z . Clearly, Π(w ) = Π(w) and w ∈ u * 1 • • • u * (L ∪ {ε}) . For each i ∈ {1, . . . , }, Π(L ∩ B) = Π(L) shows that there is z i ∈ (L ∩ B) ∪ {ε} such that Π(z i ) = Π(z i ). Let w = u α1
1 . . . u α z 1 . . . z . We find that Π(w ) = Π(w), w ∈ B and we can easily verify that w ∈ L t .

Regular Languages. The construction of an elementary bounded language that solves Pb. 1 for a regular language L is known from [START_REF] Latteux | Une propriété de la famille GRE[END_REF] (see also [START_REF] Leroux | On flatness for 2-dimensional vector addition systems with states[END_REF], Lem. 4.1). The construction is carried out by induction on the structure of a regular expression for L. Assuming L = ∅, the base case (i.e. a symbol or ε) is trivially solved. Note that if L = ∅ then every elementary bounded language B is such that Π(L ∩ B) = Π(L) = ∅.

The inductive case decomposes into three constructs. Let R 1 and R 2 be regular languages, and B 1 and B 2 the inductively constructed elementary bounded languages such that Π(R 1 ∩ B 1 ) = Π(R 1 ) and Π(R 2 ∩ B 2 ) = Π(R 2 ).

concatenation For the instance R 1 • R 2 , the elementary bounded language

B 1 • B 2 is such that Π((R 1 • R 2 ) ∩ (B 1 • B 2 )) = Π(R 1 • R 2 ); union For R 1 ∪ R 2 ,
the elementary bounded language B 1 • B 2 suffices; Kleene star Let us consider R 1 and B 1 , Lem. 4 shows how to effectively compute an elementary bounded language B such that for every t ∈ N, Π(R t 1 ∩ B ) = Π(R t 1 ). Let us prove that B solves Pb. 1 for the instance R * 1 . In fact, if w is a word of R * 1 , there exists a t ∈ N such that w ∈ R t 1 . Then, we can find a word w in R t 1 ∩ B with the same Parikh image as w. This proves that Π(R * 1 ) ⊆ Π(R * 1 ∩ B ). The other inclusion holds trivially.

Proposition 2. For every regular language R, there is an effective procedure to compute an elementary bounded language B such that Π(R ∩ B) = Π(R).

Linear Languages. We now extend the previous construction to the case of linear languages. Recall that linear languages are used to represent the iterates (ν k ) k∈N . Lemma 5 gives a characterization of linear languages based on regular languages, homomorphism, and some additional structures.

Lemma 5. (from [START_REF] Hopcroft | Introduction to Automata Theory, Languages, and Computation[END_REF]) For every linear language L over Σ, there exist an alphabet A and its distinct copy A, an homomorphism h : (A ∪ A) * → Σ * and a regular language R over A such that L = h(R A * ∩ S) where S = {w w r | w ∈ A * } and w r denotes the reverse image of the word w. Moreover there is an effective procedure to construct h, A, and R.

The next result shows that an elementary bounded language that solves Pb. 1 can be effectively constructed for every linear language L that is given by h and R such that L = h(R A * ∩ S).

  e. a (b ⊕ c) = (a b) ⊕ (a c), and (a ⊕ b) c = (a c) ⊕ (b c). We call ⊕ the combine operation and the extend operation. The natural order relation on a semiring S is defined by a b ⇔ ∃d ∈ S : a ⊕ d = b. The semiring S is naturally ordered if is a partial order on S. The semiring S is commutative if a b = b a for all a, b ∈ S, idempotent if a ⊕ a = a for all a ∈ S, complete if it is naturally ordered and is such that ω-chains a 0 a 1 • • • a n • • • have least upper bounds. Finally, the semiring S is ω-continuous if it is naturally ordered, complete and for all sequences (a i ) i∈N with a i ∈ S, sup { n i=0 a i | n ∈ N} = i∈N a i . We define two semirings we shall use subsequently. Language Semiring. Let L = 2 Σ * , ∪, •, ∅, {ε} denote the idempotent ωcontinuous semiring of languages. The natural order on L is given by set inclusion (viz. ⊆).

A Parikh-Equivalent RepresentationOur proof to compute the above L relies on a fixpoint characterization of CFLs and their Parikh image. Accordingly, we introduce the necessary mathematical notions to define and study properties of those fixpoints.

Acknowledgment. We thank Ahmed Bouajjani for pointing that the bounded languages approach subsumes the context-bounded switches one.

This research was sponsored in part by the NSF grants CCF-0546170 and CCF-0702743, DARPA grant HR0011-09-1-0037, EU People/COFUND program 229599 AMAROUT, EU IST FET Project 231620 HATS, and Madrid Regional Government project S2009TIC-1465 PROMETIDOS.

Proposition 3. For every linear language L = h(R A * ∩ S) where h and R are given, there is an effective procedure which solves Pb. 1 for the instance L, that is a procedure returning an elementary bounded B such that Π(L ∩ B) = Π(L).

Linear languages with Substitutions. Our goal is to solve Pb. 1 for k-fold compositions, i.e. for languages of the form σ k j (v k X ). Prop. 3 gives an effective procedure for the case j = k since σ k k (v k X ) is a linear language. Prop. 4 generalizes to the case j < k: given a solution to Pb. 1 for the instance σ k j+1 (v k X ), there is an effective procedure for Pb. 1 for the instance

Proposition 4. Let 1. L be a CFL over Σ; 2. B an elementary bounded language such that Π(L ∩ B) = Π(L); 3. σ and τ be two substitutions over Σ such that for each a ∈ Σ, (i) σ(a) and τ (a) are respectively a CFL and an elementary bounded and (ii) Π(σ(a) ∩ τ (a)) = Π(σ(a)).

Then, there is an effective procedure that solves Pb. 1 for the instance σ(L), by returning an elementary bounded language B such that Π(σ(L)∩B ) = Π(σ(L)).

We use the above result inductively to solve Pb. 1 for k-fold composition as follows: fix L to be σ k j+1 (v k X ), B to be the solution of Pb. 1 for the instance L, σ to be σ j and τ a substitution which maps every v j X to the solution of Pb. 1 for the instance σ j (v j X ). Then B is the solution of Pb. 1 for the instance σ k j (v k X ). Due to lack of space we refer to reader to [START_REF] Ganty | Bounded Underapproximations[END_REF] for details. We thus have an effective construction of an elementary bounded language that solves Pb. 1 for k-fold composition, hence a constructive proof for Th. 1.

Iterative Algorithm. We conclude this section by showing a result related to the notion of progress if the result of Th. 1 is applied repeatedly. Lemma 6. Given a CFL L, define two sequences

For every w ∈ L, there exists i ∈ N such that w / ∈ L i . Moreover, given L 0 , there is an effective procedure to compute L i for every i > 0.

Proof. Let w ∈ L and let v = Π(w) be its Parikh image. We conclude from Π(L 0 ∩B 0 ) = Π(L 0 ) that there exists a word w ∈ B 0 such that Π(w ) = v. Two cases arise: either w = w and we are done; or w = w. In that case

Intuitively, at least one word with the same Parikh image as w has been selected by B 0 and then removed from L 0 by definition of L 1 . Repeatedly applying the above reasoning shows that at each iteration there exists a word w such that Π(w ) = v, w ∈ B i and w / ∈ L i+1 since L i+1 = L i ∩ B i . Because there are only finitely many words with Parikh image v we conclude that there exists j ∈ N, such that w / ∈ L j . The effectiveness result follows from the following arguments: (1) as we have shown above (our solution to Pb. 1), given a CFL L there is an effective procedure that computes an elementary bounded language B such that Π(L ∩ B) = Π(L); (2) the complement of B is a regular language effectively computable; and (3) the intersection of a CFL with a regular language is again a CFL that can be effectively constructed (see [START_REF] Hopcroft | Introduction to Automata Theory, Languages, and Computation[END_REF]).

Intuitively this result shows that given a context-free language L, if we repeatedly compute and remove a Parikh-equivalent bounded subset of L (L∩B is effectively computable since B is a regular language), then each word w of L is eventually removed from it.

Application to Multithreaded Procedural Programs

We now give an application of our construction that gives a semi-algorithm for checking reachability of multithreaded procedural programs [START_REF] Ramalingam | Context-sensitive synchronization-sensitive analysis is undecidable[END_REF][START_REF] Kahlon | Tractable analysis for concurrent programs via bounded languages[END_REF][START_REF] Bouajjani | A generic approach to the static analysis of concurrent programs with procedures[END_REF]. A common programming model consists of multiple recursive threads communicating via shared memory. Formally, we model such systems as pushdown networks [START_REF] Suwimonteerabuth | Symbolic Context-Bounded Analysis of Multithreaded Java Programs[END_REF]. Let k be a positive integer, a pushdown network is a triple

where G is a finite non-empty set of globals, Γ is the stack alphabet, and for each

, where g ∈ G and α 1 , . . . , α k ∈ Γ * are individual stack content for each thread. Intuitively, the system consists of k threads, each of which with its own stack, and the threads can communicate by reading and manipulating the global storage represented by g.

We define the local transition relation of the i-th thread, written → i , as follows: (g, γβ) → i (g , αβ) iff g, γ → g , α in ∆ i and β ∈ Γ * . The transition relation of N , denoted →, is defined as follows: (g, α 1 , . . . , α i , . . . , α k ) → (g , α 1 , . . . , α i , . . . , α k ) iff (g, α i ) → i (g , α i ) for some i ∈ {1, . . . , k}. By → * i , → * , we denote the reflexive and transitive closure of these relations. Let C 0 and C be two global configurations, the reachability problem asks whether C 0 → * C holds. An instance of the reachability problem is denoted by a triple (N , C 0 , C).

A pushdown system is a pushdown network where k = 1, namely (G, Γ, ∆). A pushdown acceptor is a pushdown system extended with an initial configuration c 0 ∈ G × Γ * , labeled transition rules of the form g, γ λ → g α for g, g , γ, α defined as above and λ ∈ Σ ∪ {ε}. A pushdown acceptor is given by a tuple (G, Γ, Σ, ∆, c 0 ). The language of a pushdown acceptor is defined as expected where the acceptance condition is given by the empty stack.

In what follows, we reduce the reachability problem for a pushdown network of k threads to a language problem for k pushdown acceptors. The pushdown acceptors obtained by reduction from the pushdown network settings have a special global ⊥ that intuitively models an inactive state. The reduction also turns the globals into input symbols which label transitions. The firing of a transition labeled with a global models a context switch. When such transition fires, every pushdown acceptor synchronizes on the label. The effect of such a synchronization is that exactly one acceptor will change its state from inactive to active by updating the value of its global (i.e. from ⊥ to some g ∈ G) and exactly one acceptor will change from active to inactive by updating its global from some g to ⊥. All the others acceptors will synchronize and stay inactive.

Given an instance of the reachability problem, that is a pushdown network (G, Γ, (∆ i ) 1≤i≤k ) with k threads, two global configurations C 0 and C (assume wlog that C is of the form (g, ε, . . . , ε)), we define a family of pushdown acceptors (G , Γ, Σ, ∆ i , c i 0 ) 1≤i≤k , where:

-G = G ∪ {⊥}, Γ is given as above, and Σ = G × {1, . . . , k}, -∆ i is the smallest set such that:

→ ⊥, γ for j ∈ {1, . . . , k} \ {i}, g ∈ G, γ ∈ Γ ;

→ ⊥, γ for j ∈ {1, . . . , k} \ {i}, g ∈ G, γ ∈ Γ ;

Proposition 5. Let k be a positive integer, and (N , C 0 , C) be an instance of the reachability problem with k threads, one can effectively construct CFLs (L 1 , . . . , L k ) (as pushdown acceptors) such that

The converse of the proposition is also true, and since the emptiness problem for intersection of CFLs is undecidable [START_REF] Hopcroft | Introduction to Automata Theory, Languages, and Computation[END_REF], so is the reachability problem. We will now compare two underapproximation techniques for the reachability problem: context-bounded switches [START_REF] Qadeer | Context-bounded model checking of concurrent software[END_REF] and bounded languages, which we first detail below.

Let L 1 , . . . , L k be context-free languages, and consider the problem to decide if 1≤i≤k L i = ∅. We give a decidable sufficient condition: given an elementary bounded language B, we define the intersection modulo B of the languages {L i } i as

Proof. Define the alphabet A = {a 1 , . . . , a n } disjoint from Σ. Let h be the homomorphism that maps the symbols a 1 , . . . , a n to the words w 1 , . . . , w n , respectively. We show that 1≤i≤k

1≤i≤k L i that w ∈ B and w ∈ L i for every 1 ≤ i ≤ k, hence there exist t 1 , . . . , t n ∈ N such that w = w t1 1 . . . w tn n by definition of B. Then, we find that (t 1 , . . . ,

For the other implication, consider (t 1 , . . . , t n ) a vector of

1 . . . a tn n and finally that,

The class of CFLs is effectively closed under inverse homomorphism and intersection with a regular language [START_REF] Hopcroft | Introduction to Automata Theory, Languages, and Computation[END_REF]. Moreover, given a CFL, we can compute its Parikh image which is a semilinear set. Finally, we can compute the semilinear sets

n and the emptiness of the intersection of semilinear sets is decidable [START_REF] Ginsburg | The Mathematical Theory of Context-Free Languages[END_REF].

While Lem. 7 shows decidability for every elementary bounded language, in practice, we want to select B "as large as possible". We select B using Th. 1. We first compute for each language L i the elementary bounded language B i = w

By repeatedly selecting and removing a bounded language B from each L i where 1 ≤ i ≤ k we obtain a sequence {L j i } j≥0 of languages such that

. . The result of Lem. 6 shows that for each word w ∈ L i , there is some j such that w / ∈ L j i , hence that the above sequence is strictly decreasing, that is

. . , and finally that if 1≤i≤k L i = ∅ then the iteration is guaranteed to terminate. Comparison with Context-Bounded Reachability. A well-studied underapproximation for multithreaded reachability is given by context-bounded reachability [START_REF] Qadeer | Context-bounded model checking of concurrent software[END_REF]. We need a few preliminary definitions. We define the global reachability relation ; as a reachability relation where all the moves are made by a single thread: (g, α 1 , . . . , α i , . . . , α n ) ; (g , α 1 , . . . , α i , . . . , α n ) iff (g, α i ) → * i (g , α i ) for some 1 ≤ i ≤ n. The relation ; holds between global configurations reachable from each other in a single context. Furthermore we denote by ; j , where j ≥ 0, the reachability relation within j contexts: ; 0 is the identity relation on global configurations, and ; i+1 = ; i • ;.

Given a pushdown network, global configurations C 0 and C, and a number k ≥ 1, the context-bounded reachability problem asks whether C 0 ; k C holds, i.e. if C can be reached from C 0 in k context switches. This problem is decidable [START_REF] Qadeer | Context-bounded model checking of concurrent software[END_REF]. Context-bounded reachability has been successfully used in practice for bug finding. We show that underapproximations using bounded languages (Lem. 7) subsumes the technique of context-bounded reachability in the following sense. Proposition 6. Let N be a pushdown network, C 0 , C global configurations of N , and

By the CFL encoding (Prop. 5) each of these sequences corresponds to a word in Σ k . If C 0 ; k C, then there is a word w ∈ i L i and w ∈ Σ k . Define B k to be w * 1 • • • w * m where w 1 , . . . , w m is an enumeration of all strings in Σ k . We conclude from w ∈ Σ k and the definition of B k that w ∈ B k , hence that

For the other direction we conclude from

However, underapproximation using bounded languages can be more powerful than context-bounded reachability in the following sense. There is a family {(N k , C 0k , C k )} k∈N of pushdown network reachability problems such that C 0k ; k C k but C 0k ; k-1 C k for each k, but there is a single elementary bounded B such that (B) i L ik = ∅ for each k, where again (L 1k , . . . , L nk ) are CFLs such that C 0k ; C k iff ∩ i L ik = ∅ (as in Prop. 5).

For clarity, we describe the family of pushdown networks as a family of twothreaded programs whose code is shown in Fig. 1. The programs in the family differs from each other by the value to which k is instantiated: k = 0, 1, . . . Each program has two threads. Thread one maintains a local counter c starting at 0. Before each increment to c, thread one sets a global bit. Thread two resets bit. The target configuration C k is given by the exit point of p1. We conclude from the program code that hitting the exit point of p1 requires c ≥ k to hold. For every instance, C k is reachable, but it requires at least k context switches. Thus, there is no fixed context bound that is sufficient to check reachability for every instance in the family. In contrast, the elementary bounded language given by (bit == true, 2) • (bit == false, 1)

* is sufficient to show reachability of the target for every instance in the family.


Karim Dahman
email: @loria.fr

Bridging the Gap between the Business Processes and the Service Oriented Architecture

Bridging the gap between the (ever) evolving Business and its supporting IT capabilities is of high relevance in today's enterprise information system roadmap [START_REF] Chen | From software architecture analysis to service engineering: An empirical study of methodology development for enterprise soa implementation[END_REF]. Without an agile development method and stable IT architectural principles there is no chance to foreshadow a successful route to valuable computerized software solutions. The Service Oriented Architecture (SOA [START_REF] Papazoglou | Service-oriented computing: State of the art and research challenges[END_REF]) has emerged as a new paradigm for modeling, building and managing software architectures to support the Business Processes (BP [START_REF] Dumas | Service-enabled process management[END_REF]) in loosely-coupled, distributed and continuously changing environments. In many cases, the experience shows that with a Model Driven Engineering (MDE [START_REF] Lopes | Generating transformation definition from mapping specification: Application to web service platform[END_REF]), where the BP models drive the software applications, less effort is gone into their alignment during the initial development, and IT developers can rapidly proceed with the instantiation of the technology-neutral SOA implementations [START_REF] Brahe | Bpm on top of soa: experiences from the financial industry[END_REF]. However, in order to enable BP evolutions without loosing the control on the BP/SOA alignment many challenges still need to be addressed. In particular, how to ensure the automated propagation of the BP model evolutions to the SOA model adaptations while keeping them synchronized remains an open question. Therefore, the BP-to-SOA incremental transformation is a major use case for the SOA engineering.

Several frameworks have emerged to help organizations to charter successful route to the SOA implementation. The Model Driven Architecture provides a mean for using UML-based model transformations to direct the course of the system development stages [START_REF] Lopes | Generating transformation definition from mapping specification: Application to web service platform[END_REF]. However, as UML is neither fully service-oriented, nor business process-centered, it needs to address the gap between the emerging process notations and the lower-level standards. In [START_REF] Huemer | The 2nd IEEE Conference on Digital Ecosystems and Technologies[END_REF], the authors advocate the integration of the business values perspective to the SOA engineering. They define a conceptual framework for the design space, but unfortunately fail to provide a practical development scenario. In [START_REF] Dahman | Generation of Component Based Architecture from Business Processes: Model Driven Engineering for SOA[END_REF], we have presented a MDE scenario that starts off with a (source) BP model specification, and that leads to a canonical (target) SOA model. The scenario is enough mature to accomplish the automatic model conceptual mappings, however, it does not provide a support for an incremental transformation. First, it requires manual target model adaptations to reflect the source model evolutions. Of course, adapting the generated SOA model is potentially error-prone, leads necessarily to their misalignment with the BP layer, and implies design decision losses. Second, the effort to compute the modifications on the target is proportional to the size of the source model as we have to enforce again a model transformation [START_REF] Antkiewicz | Design space of heterogeneous synchronization[END_REF]. What sounds so straightforward and easy in theory with the model evolutions in the MDE, turns out to a very challenging endeavor in practice. The existing general model synchronization frameworks [START_REF] Antkiewicz | Design space of heterogeneous synchronization[END_REF] cannot work well here. First, they require users to explicitly write synchronization code to deal with each update kind and on each of the assorted models. Second, the mapping complexity of each combinatorial change is inherently compounded with the decisions regarding the potential information loss or gain related to different levels of the model's expressiveness.

Compared to these frameworks, our approach that we have introduced in [START_REF] Dahman | Towards consistency management in the business-driven development of the soa[END_REF] extracts informations automatically from the previous transformations and does not require users to write a synchronization code. Given a structural update on the (source) BP model and a transformation that has previously generated a corresponding (target) SOA model, we developed a change forward transformation approach to consistently propagate the BP updates into the related SOA. We consider that a structural model update corresponds to the execution of a compound sequence of primitive change operations such as model element additions, removals, and relocations on a graph structures that represent the BP and the SOA models. One way for obtaining a sequence of model update operations is by recording editing operations performed by the BP modelers. For example, the addition of a process fragment can be seen as a composite production of several primitive graph productions on the BP model. The conditional graph rewritings [START_REF] Giese | From model transformation to incremental bidirectional model synchronization[END_REF] allows us to detect the structural update conflicts between pairs of primitive operations. Our transformation trace-aware model synchronizer is implemented in a BP model editor. First, it locates the corresponding constructs in the previous transformation execution context that are affected by the source update. Then, with the identified correspondence and when it is possible over a consistency relation established between the BP and the SCA models, it translates the change operations that consistently update the target with the values from the source. In order, to make the model synchronization effectively incremental, we use the so called update translation operator [START_REF] Antkiewicz | Design space of heterogeneous synchronization[END_REF]. Thus, the synchronization computations result in a reasonable decoupling from the source model size [START_REF] Giese | From model transformation to incremental bidirectional model synchronization[END_REF].

The claimed benefits of our MDE include enhanced development principles of the SOA engineering, a better reuse of legacy applications through service wrappings in software components and an easier adaptation to changes in the business environments through model update propagations. As a major contribution, our design-time approach makes the BP model transformation more tractable to reconfigure the SOA implementation without disrupting its structural consistency. Thus, the system architects can rapidly assess the necessity to propagate the change from the BP models to the SOA implementations. Rather than executing the entire transformation afresh and if the SOA update seems to be appropriate, then they can synchronize the SOA platform-specific implementations with the IT developers. The experimental results are encouraging, but still needs to be validated in a real-scale case study and tool. The integration of our update translation operator in a previously developed ATLAS Transformation Language chain for the Eclipse SOA Tools Platform is in development [START_REF] Dahman | From business process to component architecture: Engineering business to it alignment[END_REF]. Furthermore, the BP/SOA round-tripping is essential to rapidly realign BP with the evolving SOA. Likewise, we have to consider update to both the business and IT architectures via pattern-based transformation techniques. Finally, making the MDE more tractable to reconfigure the BP and the SOA implementations without disrupting the non-functional capabilities remain as a future work.


Markus Schwarzlander

David C Logan

Mark D Fricker

Lee Sweetlove

J Lee

Sweetlove

The circularly permuted yellow fluorescent protein cpYFP that has been used as a superoxide probe is highly responsive to pH but not superoxide in mitochondria: implications for the existence of superoxide 'flashes'

Keywords: cpYFP, mitochondria, superoxide, pH, ROSreactive oxygen species, RNSreactive nitrogen species, ETCelectron transport chain, CLSMconfocal laser scanning microscopy, roGFPredox sensitive GFP, pmfprotonmotive force, SODsuperoxide dismutase, CCCP -carbonylcyanide-3-chlorophenylhydrazone, MnTMPyP -manganese

published or not. The documents may come

The circularly permuted yellow fluorescent protein cpYFP that has been used as a superoxide probe is highly responsive to pH but not superoxide in mitochondria: implications for the existence of superoxide 'flashes'

Introduction

The development of genetically-encoded probes that allow quantification of reactive oxygen species (ROS) at a cell-specific and subcellular resolution in living tissues and in real time have facilitated a more sophisticated understanding of the role of ROS in signalling and development [START_REF] Niethammer | A tissue-scale gradient of hydrogen peroxide mediates rapid wound detection in zebrafish[END_REF][START_REF] Meyer | Fluorescent protein-based redox probes[END_REF]. Measuring superoxide dynamics in living, intact cells, i.e. in vivo is of particular interest: in most systems superoxide is the precursor for most other ROS and RNS such as hydrogen peroxide, the hydroxyl radical or peroxynitrite. In mitochondria, where superoxide is generated by the electron transport chain, superoxide links bioenergetic function and radical dynamics [START_REF] Murphy | How mitochondria produce reactive oxygen species[END_REF]. Superoxide production rate is strongly determined by the functional state of the ETC and its formation can rise dramatically under stress [START_REF] Moller | PLANT MITOCHONDRIA AND OXIDATIVE STRESS: Electron Transport, NADPH Turnover, and Metabolism of Reactive Oxygen Species[END_REF]. Mitochondrial superoxide dynamics are therefore key for the understanding of the interplay between cellular energetic state, redox signalling and stress responses. However, most of our understanding about mitochondrial superoxide has been gathered under in vitro conditions, i.e. from isolated organelles. A genetically encoded superoxide sensor has therefore the potential to provide physiologically meaningful insights into mitochondrial superoxide dynamics in a cellular context. Recently a superoxide sensor based on a circularly-permuted YFP (cpYFP) was reported and provided evidence for 'flashes' of superoxide production in single mitochondria of cardiomyocytes [START_REF] Wang | Superoxide flashes in single mitochondria[END_REF]. This raised important questions about the dynamic nature of mitochondrial free radical processes in vivo.

However, doubts have been raised about the specificity of cpYFP as a reporter of superoxide in the mitochondrial matrix [START_REF] Muller | A critical evaluation of cpYFP as a probe for superoxide[END_REF]. In this study we characterized the dynamic fluorescence properties of cpYFP targeted to the matrix of plant mitochondria. Properties of the probe were validated in living plant cells and in isolated mitochondria and the sensitivity of the probe to mitochondrial bioenergetics, superoxide production and pH were established.

Methods

Plant lines and culture conditions

The mitochondrial-targeted cpYFP construct was engineered by combining the cpYFP coding region in-frame and downstream of the mitochondrial targeting sequence from Nicotiana plumbaginifolia ß-ATPase [START_REF] Logan | Mitochondria-targeted GFP highlights the heterogeneity of mitochondrial shape, size and movement within living plant cells[END_REF] under control of the CaMV 35S promoter in the binary vector pH2GW7 [START_REF] Karimi | GATEWAY vectors for Agrobacteriummediated plant transformation[END_REF], using Gateway technology (Invitrogen Ltd, Paisley, Renfrewshire, UK). Hairpin RNAi constructs were composed of specific and unique fragments of the MnSOD (At3g10920) sequence, in sense and antisense orientation, in the pOpOff2 vector providing dexamethasone inducible transcript knock down [START_REF] Craft | New pOp/LhG4 vectors for stringent glucocorticoid-dependent transgene expression in Arabidopsis[END_REF]. Agrobacterium mediated transformation of Arabidopsis thaliana (accession Columbia, Col-0) was performed by 'floral dip' [10]. Transformants were selected by hygromycin (pH2GW7) or kanamycin (pOpOff2) resistance. Knock down efficiency of MnSOD transcript was assessed by semi-quantitative RT-PCR. Homozygous T 3 lines were selected by segregation of antibiotic resistance. For in vivo microscopy, seedlings were cultivated for 7-10 days on vertical half-strength Murashige and Skoog medium agar plates under long day conditions. For mitochondrial isolation, seedlings were cultured in a hydroponic pot system for 14 d as described before [11]. For induction of RNAi, 10 μM of dexamethasone were added to the medium. Immunoblotting of total seedling extract was performed using a polyclonal MnSOD specific antiserum as described before [START_REF] Morgan | Decrease in manganese superoxide dismutase leads to reduced root growth and affects tricarboxylic acid cycle flux and mitochondrial redox homeostasis[END_REF]13].

Mitochondrial isolation and assays

Mitochondria were isolated from 14 day old Arabidopsis seedling cultures as described before [11], except pH of wash buffers was adjusted with Tris instead of KOH. Coupling was measured in a Clark-type oxygen electrode 'Oxygraph' (Hansatech Instruments, Pentney, Norfolk, UK) as described before [14] in 'basic incubation medium' (0.3 M sucrose, 5 mM KH 2 PO 4 , 10 mM TES, 10 mM NaCl, 2 mM MgSO 4 , 0.1 % (w/v) fatty acid free BSA, pH 7.2 -KOH).

Microscopy

Living roots were imaged in half-strength Murashige and Skoog medium. Staining with 200 nM MitoTracker Orange CMTMRos (Invitrogen Ltd, Paisley, UK) was performed as described before [START_REF] Schwarzlander | Confocal imaging of glutathione redox potential in living plant cells[END_REF]. Isolated mitochondria were immobilized onto round glass cover slides by centrifugation (2000 g, 5 min, 4°C) in 0.3 M sucrose, 10 mM TES, pH 7.2 (Tris). Immediately before imaging mitochondria were energized by addition of medium containing the required respiratory substrate. Microscopy was performed using a Zeiss LSM510 META confocal microscope (Carl Zeiss MicroImaging GmbH, Goettingen, Germany) equipped with laser lines for 488, 405 and 543 nm excitation. Imaging was carried out with a 63 lens (Zeiss Plan-Apochromat 63x, N.A.=1.4, Oil) in multi-track mode with line switching. cpYFP was excited at 488 and 405 nm and MitoTracker Orange at 543 nm. cpYFP or MitoTracker fluorescence were measured at 505-530 nm and 565-615 nm respectively. Laser output was kept under 2% of maximal power equalling <2.5 μW for any wavelength as measured in the defocused beam at the backplane of the objective. Pixel size A c c e p t e d M a n u s c r i p t was 70 nm and pixel dwell time 1.3 μs. Time-series were collected with time intervals between 2 and 5 s. Microscopy data was background subtracted and analysed using custom software as described before [15].

Fluorimetry

Mitochondria were suspended in 'basic incubation medium' in 96-well plates. Total assay volume was 200 μL. Fluorescence was measured at 25°C in a Beckman Coulter DTX 880 Multimode Detector (Beckman Coulter, Inc., Fullerton, CA, USA) equipped with 485 and 405 nm emission filters and a 500-530 nm BP excitation filter. Data were background subtracted and processed in MS Excel.

Results

cpYFP flashes in active plant mitochondria

To study the dynamic behaviour of cpYFP in plant mitochondria we created stable Arabidopsis transformants expressing cpYFP in the mitochondrial matrix. Mitochondrial localisation of cpYFP signal with excitation at either 488 nm or 405 nm was confirmed by colocalisation with MitoTracker Orange (Suppl. Fig. 1) and by fluorescence of isolated, purified mitochondria (Fig. 1B). Probe behaviour was monitored in living root epidermal cells by confocal laser scanning microscopy (CLSM). cpYFP signal was relatively homogeneous between all mitochondria of a single cell, while intensity between cells was somewhat variable. At the level of individual mitochondria infrequent, spontaneous, and transient increases in cpYFP fluorescence were observed with 488 nm excitation (Fig. 1A). The cpYFP signal in a single mitochondrion increased transiently in intensity before returning to baseline fluorescence within seconds (Fig. 1A,C; Suppl. Movie 1). The duration of each event was typically 10 to 20 seconds and the degree of signal increase was 1.3 -2.5 times baseline. Hence this phenomenon showed similar characteristics in time and amplitude as cpYFP 'flashes' in mitochondria of mammalian cells described by [START_REF] Wang | Superoxide flashes in single mitochondria[END_REF]. We therefore adopt the term 'flashes' for the events we describe here in plant mitochondria.

Another similarity between our findings and those of [START_REF] Wang | Superoxide flashes in single mitochondria[END_REF] was the infrequent occurrence of flashes. On average about one flash could be observed when monitoring the top cytoplasmic layer of a whole root epidermal cell for 10 min. Low flash frequency, coupled with the motility of mitochondria in plant cells (moving into and out of the field of observation in three dimensions) prevented continuous observation of single mitochondria and quantification of flash frequency. We therefore optimized a cell-free system using isolated mitochondria that allowed a more systematic assessment of flashes. Isolated mitochondria were immobilized onto a coverslip and monitored by confocal microscopy. Respiratory control ratios were > 2.5 for succinate as substrate in all experiments. Isolated respiring mitochondria also displayed cpYFP flashes (Fig. 1B,D; Suppl. Movie 2). Spontaneous changes in cpYFP signal intensity were more frequent in this system, making flashes the norm rather than the exception at around 0.8 flashes per mitochondrion per minute. Fluorescence with 405 nm excitation remained unchanged during the events (Suppl. Fig. 2). Similar behaviour was observed with other respiratory substrates (malate/pyruvate, NADH). No flashes occurred in non-respiring mitochondria (state 1) or upon uncoupling (data not shown), suggesting that the presence of a proton motive force (pmf) was a prerequisite for flashes to occur. Isolated mitochondria therefore provided an appropriate model system to evaluate further the reason for dynamic cpYFP behaviour in the mitochondrial matrix.

cpYFP responds dynamically to changes in mitochondrial respiratory state cpYFP flashes in the mitochondrial matrix have been linked to respiratory activity and functional ETC [START_REF] Wang | Superoxide flashes in single mitochondria[END_REF]. To understand the average probe behaviour in different bioenergetic states we measured the population response of mitochondrial suspensions in a 96-well plate A c c e p t e d M a n u s c r i p t reader. Different respiratory states were established by substrate or inhibitor feeding. cpYFP signal responded to those changes in a highly sensitive manner with 485 nm excitation (Fig. 2). Supply of respiratory substrate led to a strong increase in probe signal. Substrates with different ETC entry points (succinate: complex II, pyruvate/malate: complexes I and II, ferrocyanide: complex IV) triggered similar cpYFP responses, although ferrocyanide triggered a less pronounced signal increase. For consistency, succinate was used as a substrate in all subsequent measurements. The absolute signal varied between 3-and 6-fold depending on mitochondrial preparation and storage time of mitochondrial suspensions before use (likely correlating with degree of coupling), but relative probe response was consistent between individual experiments. The switch from state 2 to state 3 caused by addition of ADP resulted in a decrease of cpYFP fluorescence, followed by recovery when entering state 4 upon ADP depletion (Fig. 2). Uncoupling by CCCP led to a decrease in signal close to the value of state 1. In contrast, fluorescence at 405 nm excitation remained largely stable over the course of the measurements (Suppl. Fig. 3). Expressing the data as ratio of 485/405 signal was used in a ratiometric approach but was not required in the plate reader system. The overall pattern of cpYFP signal in different respiratory states appeared to correlate with the magnitude of pmf and therefore suggests that cpYFP is responsive to a parameter linked to, or downstream of, pmf in plant mitochondria.

Manipulation of matrix superoxide levels does not impact on cpYFP dynamics

cpYFP has been used previously as a superoxide sensor based on a 4-fold increase in fluorescence in response to artificially generated superoxide in vitro [START_REF] Wang | Superoxide flashes in single mitochondria[END_REF]. The correlation of cpYFP signal and pmf in isolated plant mitochondria is consistent with expected changes in superoxide, as mitochondrial superoxide production increases as a function of pmf [START_REF] Murphy | How mitochondria produce reactive oxygen species[END_REF]. However, other parameters linked to pmf could also be responsible for the altered cpYFP fluorescence intensity. To further evaluate superoxide sensitivity of cpYFP in plant mitochondria, the effect of different complex III inhibitors on cpYFP signal was measured. Antimycin A inhibits complex III by binding to the 'N' site, strongly stimulating superoxide release, while myxothiazol binds to the 'P' site and does not increase superoxide production [START_REF] Moller | PLANT MITOCHONDRIA AND OXIDATIVE STRESS: Electron Transport, NADPH Turnover, and Metabolism of Reactive Oxygen Species[END_REF]. We found that both inhibitors caused a decrease in cpYFP signal (Fig 3A). This suggests that an inhibition of electron transport at complex III per se, rather than changes in superoxide levels, causes changes in cpYFP intensity. In addition, menadione, a redox active quinone that mediates superoxide release in mitochondria [START_REF] Baxter | The metabolic response of heterotrophic Arabidopsis cells to oxidative stress[END_REF], had no effect on cpYFP signal (Suppl. Fig. 4).

The superoxide sensitivity of cpYFP in plant mitochondria was further assessed by treatment of mitochondria under state 2 respiration with three different membrane-permeable superoxide scavengers. Treatments with tiron within the concentration range used by Wang et al. had no effect on cpYFP signal (Fig. 3B). Also tempol, a SOD mimetic, that has been shown to alleviate ROS induced mitochondrial abnormality in plants, when applied at similar concentrations [17], did not cause any effect. By contrast, MnTMPyP, another SOD mimetic, led to a significant decrease in fluorescence. However a proportional decrease was also observed at 405 nm excitation upon MnTMPyP treatment (Suppl. Fig. 5A,B) and MnTMPyP also decreased baseline cpYFP fluorescence, decreasing the signal beyond its state 1 value (Suppl. Fig. 5C). These observations suggest quenching of cpYFP fluorescence by MnTMPyP, which may be a result of the intense brown colour of the compound, rather than an effect due to superoxide removal.

Finally, the response of cpYFP in isolated mitochondria lacking matrix superoxide dismutase (MnSOD) was tested. For that purpose cpYFP was expressed in the mitochondrial matrix of a line containing an inducible RNAi construct for suppression of mitochondrial superoxide dismutase expression. RNAi-mediated suppression of MnSOD was confirmed by immunoblot analysis (Fig. 3C). MnSOD protein was undetectable from day 4 after induction (Fig. 3C,inset). Respiring mitochondria isolated 5 days after induction showed no significant increase in cpYFP signal compared to control (Fig. 3C).

In conclusion, there was no significant experimental correlation between mitochondrial ROS and cpYFP fluorescence in isolated Arabidopsis mitochondria.

A high pK a makes cpYFP highly pH sensitive in the mitochondrial matrix

As no direct evidence for any significant sensitivity of cpYFP to superoxide in plant mitochondria could be found, other parameters linked to pmf were assessed for their ability to modulate cpYFP fluorescence. Strong pH dependence of cpYFP was reported previously by [START_REF] Wang | Superoxide flashes in single mitochondria[END_REF] and cpYFP fluorescence intensity in isolated Arabidopsis mitochondria was observed to increase with increasing medium pH (Suppl. Fig. 6). Re-evaluation of the pH properties of cpYFP in mitochondrial lysates revealed a pK a of around 8.6 with 485 nm excitation (Fig. 4A). In addition the dynamic range of the probe was broad between pH 7 and 10. A >50-fold increase in fluorescence was observed upon alkalisation. Addition of 5 μM CCCP did not lead to any changes in lysates (data not shown), confirming that cpYFP was well equilibrated with the medium. In contrast to excitation with 485 nm, the probe showed only minor pH sensitivity with 405 nm excitation (Fig. 4B). This allows ratiometric expression of pH sensitivity independently of probe concentration and without significant impact on pK a or dynamic range (Fig. 4C). The strong pH dependence of cpYFP raise the possibility that pH changes rather than superoxide may account for the observed probe dynamics in mitochondria.

cpYFP dynamics in respiring plant mitochondria represent pH changes

To assess if pH changes are sufficient to account for the observed probe dynamics in respiring mitochondria, ΔpH was separated from pmf (and thereby superoxide production) using nigericin. pH was clamped by nigericin-mediated K + /H + antiport, while the voltage component of pmf was maintained. Addition of nigericin in the presence of K + ions not only decreased cpYFP signal to the same degree as the uncoupler CCCP (Fig. 5A), it also abolished the increase in cpYFP signal upon energization from state 1 to state 2 (Suppl. Fig. 5C). Clamping matrix pH was therefore sufficient to stop mitochondrial cpYFP dynamics in mitochondrial suspensions independently of the presence of a pmf and associated superoxide release. Nigericin also completely abolished cpYFP flashes in single isolated mitochondria monitored by CLSM (Fig. 5B,C; Suppl. Movies 3,[START_REF] Moller | PLANT MITOCHONDRIA AND OXIDATIVE STRESS: Electron Transport, NADPH Turnover, and Metabolism of Reactive Oxygen Species[END_REF]. Flashes were retained when the identical treatments were applied in K + -free medium (data not shown), demonstrating specificity of pH clamping in this system. Overall, changes in matrix pH provided a sufficient explanation for the observed cpYFP signal dynamics in mitochondrial suspensions as well as in single mitochondria.

Discussion

Based on the observation of cpYFP flashes in single plant mitochondria we aimed to elucidate the basis of the probe response. Similar flashing events have been observed in single mitochondria of cardiomyocytes using cpYFP and interpreted as response superoxide bursts in the matrix based on superoxide sensitivity of the sensor in an in vitro assay [START_REF] Wang | Superoxide flashes in single mitochondria[END_REF]. Using isolated mitochondria as a minimal model system allowed us to validate cpYFP properties in situ, using a reductionist approach. Isolated plant mitochondria lack most respiratory metabolites and co-factors allowing tight control of potential probe interactors [18]. Our results confirm previous observations that mitochondrial cpYFP signal is linked to mitochondrial electron transport and metabolic status [START_REF] Wang | Superoxide flashes in single mitochondria[END_REF]. Wang et al. showed that flash frequency was strongly inhibited when electron transport was dysfunctional or inhibited in cardiomyocytes. In our hands absolute signal intensity strongly depended on respiratory state, decreased upon ETC inhibition at complex III and flashes were only observed in energized mitochondria. However, we were unable to demonstrate a significant response to matrix superoxide; instead the dynamic behaviour of cpYFP was fully accounted for by its pronounced pH sensitivity. pH sensitivity of cpYFP was reported by [START_REF] Wang | Superoxide flashes in single mitochondria[END_REF] without any determination of pK a and dynamic range. pH sensitivity is common in GFP-derived probes, however it can often be ignored when the pK a of the probe is sufficiently distant from the assay pH. Wang et al. ruled out transient changes in matrix pH being responsible for cpYFP flashes, based on the absence of flashes using a mitochondrial targeted EYFP as a pH sensor. However, the pK a of EYFP is around 7. 1 [19] meaning that it will not be particularly responsive to increases of pH from the physiological value of 7.8-7.9 that has been determined in respiring animal and plant mitochondria in vivo [19,20]. Comparably high matrix pH is expected in isolated mitochondria under state 2 and 4 respiration and a medium pH of 7.2. Based on cpYFP signal, switch from state 1 to 2 increases matrix pH by about 1 unit, i.e. to about 8.2, under the conditions used here (see Suppl. Fig. 6). The high pK a of cpYFP ~pH 8.6 means that cpYFP will be much more sensitive than EYFP to pH change in the mitochondrial matrix. For example, given a resting pH of 7.9, a pH increase of 0.4 units results in a ~2-fold increase of cpYFP fluorescence. This is in contrast with EYFP that would only show a very subtle fluorescence change (~1.1-fold) upon the same pH increase [19]. Moreover, the observed probe responses to changes in respiratory states of isolated mitochondria at buffer pH 7.2 appears, at least qualitatively, in line with the expected pH changes occurring in the matrix. cpYFP is therefore a highly responsive pH sensor in the physiological context of the mitochondrial matrix.

Wang et al. provided good evidence that cpYFP is sensitive to superoxide in vitro. It therefore remains possible that cpYFP can report mitochondrial superoxide in vivo. However, for reasons stated above, our view is that changes in cpYFP fluorescence in the mitochondrial matrix in plants are more likely to be related to changes in matrix pH in vivo. A mechanism for the proposed superoxide sensitivity of cpYFP would help to clarify the situation, indeed Wang et al. have suggested involvement of two cysteines. However the reactivity of thiols with superoxide is low, which makes such a mechanism unlikely [21]. In contrast, pH-dependence of cpYFP fluorescence provides a straightforward explanation for the observed probe responses: the chromophore can be protonated, inducing a reversible fluorescence increase [22].

The superoxide sensitivity of cpYFP has been scrutinized in a review by [START_REF] Muller | A critical evaluation of cpYFP as a probe for superoxide[END_REF]. A major criticism included the decreased flash rate upon antimycin A treatment, which generally induces superoxide release into the matrix. Our treatments of isolated plant mitochondria by antimycin A also gave a decrease in cpYFP intensity rather than inverse as expected from elevated superoxide production. cpYFP fluorescence was low when respiration was not active, either due to lack of substrate or due to inhibition of complex III, and no cpYFP flashes occurred in the absence of pmf. Although plant and mammalian mitochondria differ in many aspects, changes in pH could in principle resolve the apparent contradictions that have been pointed out by Muller. Recently Pouvreau [23] also detected flashes in mitochondria of mouse skeletal muscle cells using a ratiometric pericam sensor that contains the cpYFP sequence. MitoSOX, a superoxide sensitive chemical dye, was then used as an in vivo control for superoxide sensitivity of the sensor. Increase in MitoSOX intensity for a mitochondrion undergoing a flash was suggested. Therefore it is possible that cpYFP flashes in different systems represent different physiological phenomena. However, as the mitoSOX signal only increases slightly during a flash, even though mitoSOX acts as an irreversible and cumulative superoxide stain (with its specificity in vivo having been questioned [24]), the possibility of photo-oxidative ROS production during a transient increase in cpYFP fluorescence should be considered as an alternative explanation.

We suggest that cpYFP is a promiscuous sensor that can in principle respond to different parameters via changes in signal intensity. Its responsiveness to superoxide and thiol agents in vitro has been documented along with its pH sensitivity and additional effectors cannot be A c c e p t e d M a n u s c r i p t ruled out. However its pH response is substantial particularly at mitochondrial pH values and cpYFP dynamics in mitochondria can be abolished when pH is clamped. These findings cast doubt on the existence of superoxide flashes in mitochondria suggesting and suggest that the flashes may in fact be related to transient changes in matrix pH. Moreover this work emphasises the need to understand how ROS and redox probes work mechanistically [25,[START_REF] Meyer | Redox-sensitive GFP in Arabidopsis thaliana is a quantitative biosensor for the redox potential of the cellular glutathione redox buffer[END_REF]. Without this understanding the relative contributions of individual parameters to the response of cpYFP under physiological conditions have to be considered carefully in order to draw accurate conclusions. A c c e p t e d M a n u s c r i p t

Licenced copy. Copying is not permitted, except with prior permission and as allowed by law.

Biochemical

  Journal Immediate Publication. Published on 01 Jun 2011 as manuscript BJ20110883 THIS IS NOT THE VERSION OF RECORD -see doi:10.1042/BJ20110883

Biochemical

  Journal Immediate Publication. Published on 01 Jun 2011 as manuscript BJ20110883 THIS IS NOT THE VERSION OF RECORD -see doi:10.1042/BJ20110883

Biochemical

  Journal Immediate Publication. Published on 01 Jun 2011 as manuscript BJ20110883 THIS IS NOT THE VERSION OF RECORD -see doi:10.1042/BJ20110883

FiguresFig. 1 :

 1 Figures

Fig. 2 :

 2 Fig. 2: The response of cpYFP fluorescence to different respiratory substrates and states in isolated mitochondria. Freshly isolated Arabidopsis mitochondria (~20 μg protein) expressing cpYFP in their matrix were suspended in 'basic incubation medium' and energized by respiratory substrates (RS). Suc (circles): 10 mM succinate, 0.25 mM ATP, 20 μM rotenone; Pyr/Mal (diamonds): 10 mM pyruvate, 10 mM malate, 0.3 mM NAD, 0.1 mM thiamine pyrophosphate; Fer (triangles): 20 mM K 4 [Fe(CN) 6 ]. ADP (250 μM) was added as indicated. For uncoupling CCCP (5 μM) was added. n = 5; error bars = SD. The experiment was repeated independently 5 times with similar results.

Fig. 3 :

 3 Fig. 3: CpYFP response to antimycin A, superoxide scavengers and lack of MnSOD in active isolated mitochondria. Mitochondria (20 μg) were suspended in 'basic incubation medium' and energized (10 mM succinate, 0.25 mM ATP, 20 μM rotenone). (A) Treatment with the complex III inhibitors antimycin A (1 μM, white circles), myxothiazol (1 μM, grey circles) and solvent control (EtOH, black circles). (B) Treatment with superoxide scavengers tiron (500 μM, white diamonds), tempol (100 μM, white squares), MnTMPyP (20 μM, white triangles) and solvent control (water, black circles). (C) Response of cpYFP in isolated mitochondria lacking MnSOD (white circles) to different respiratory states (see Fig. 2) compared to control (black circles). Seedlings of a dexamethasone-inducible MnSOD knock down line were induced with 10 μM dexamethasone and solvent control (DMSO). Immunoblotting of seedling extract showed absence of MnSOD protein compared to control from day 4 after induction on (inset). Mitochondria were isolated after 5 days . n = 4; error bars = SD. The experiments were repeated 3 times with similar results.

Fig. 4 :

 4 Fig. 4: pH dependence of mt-cpYFP fluorescence. Fluorescence of lysed mitochondria expressing cpYFP in response to excitation at (A) 485 nm, (B) 405 nm and (C) the ratio of 485 nm to 405 nm fluorescence. Mitochondria were lysed by a freeze and thaw cycle. 10 μg mitochondrial protein lysate was suspended in 0.3 M sucrose, 10 mM TES/Tris. pH was adjusted by titration of TES with Tris base. pK a is indicated by dotted lines. n = 3; error bars = SD.

Fig. 5 :

 5 Fig. 5: The impact of nigericin on cpYFP fluorescence dynamics in isolated mitochondria. (A) Mitochondria (20 μg) were suspended in a medium of 0.2 M sucrose, 0.1 M KCl and 10 mM TES, pH 7.2 (Tris), energized (10 mM succhinate, 20 μM rotenone) and treated with nigericin (5 μM, white circles), CCCP (5 μM, grey circles) and solvent control (EtOH, black circles). n = 3; error bars = SD. The experiment was repeated independently 3 times with similar results. (B,C) The dynamics of cpYFP signal intensity (488 nm excitation) was measured by CLSM in individual respiring mitochondria under the same conditions as in (A). Solvent control (EtOH, B) and5 μM nigericin (C). Normalized intensity traces for four representative individual mitochondria are shown. The experiment was repeated 3 independent times with similar results.

Licenced copy. Copying is not permitted, except with prior permission and as allowed by law.© 2011 The Authors Journal compilation © 2011 Portland Press Limited

© 2011 The Authors Journal compilation © 2011 Portland Press Limited

Acknowledgements

We gratefully thank Dr Wang Wang (University of Washington, Seattle, WA, USA) and Prof Heping Cheng (Peking University, Bejing, China) for kindly providing the cpYFP construct, Dr Karl Morten (University of Oxford, UK) for the generous gift of some myxothiazol, Dr Daniel Kliebenstein (University of California, Davis, CA, USA) for the MnSOD antiserum and Dr Ian Moore (University of Oxford, UK) for the pOpOff2 vector. Stimulating discussions with Prof George Ratcliffe (University of Oxford, UK), Prof Andreas Meyer (University of Bonn, Germany) and Prof Andrew Halestrap (University of Bristol, UK) have strengthened this work. MS was funded by New College Oxford through a Weston Junior Research Fellowship.