AGRO-INDUSTRIE et METHODES STATISTIQUES MINIMISATION OF THE COST OF GMO DETECTION IN KERNELS USING CONTROL BY ATTRIBUTES

Keywords: seed acceptance sampling, GMO, quality control, operating characteristic curve, single sampling by attributes, double sampling by attributes, group analysis

Quality contrai by attribute (2], (7] may be used with grain lots in order to detect GMO. But usually the contrai cannot be made on each grain separately. The presence of GMO is rather tested in groups of grains the size of which is an important parameter which can be used to find a cost optimal testing scheme among those which give acceptable buyer and seller risks. This group contrai has been studied for virus or bacterium detection in grains by the Elisa method (4],[3Jand is advocated by (6] for GMO detection. But no optimisation method to select the cheapest testing scheme has yet been described.

Given a cost function depending on the number of groups to analyse and of the total number of grains, we describe in this paper a practical way to get the less expensive testing scheme keeping both the consumer and the producer risks below a predetermined threshold.

Introduction

GMO control is compulsory in numerous countries including those of the European Union. Since tîe introduction of nove! food and ingredient 258/97/EC regulation, ail foods containing GMO or •o erived compounds should be labelled above a 1 % threshold of fortuitous presence in each ingredient (:-egulation 49/2000/EC).

GMO detection is generally made either through a protein specific of the GMO trait, or by PCR amplification and subsequent detection of the corresponding DNA sequence. ln many cases, the result of this detection is a quantitative response, e.g. the Ct in real time quantitative PCR, which can be used, by comparison to known standards, to get an evaluation of the GMO concentration. But doing that rigorously implies a good knowledge of the distribution of this response and of the factors i:,fiuencing it. For instance since test samples and standards have been extracted separately, it is e ssential to know the variability induced by the extraction to evaluate the induced errors.

An easier and more robust way of dealing with such a response is to use it only to detect the presence of GMO (6]. Once a representative sample from the grain lot inspected has been collected, one or several subsamples of it are ground and analysed. For each analysed subsample, the result is t:"'len "yes, it contains the searched GMO" or "no, it does nof'. This yes or no result is known in quality contrai as an attribute of the subsample. The control is then made from the attributes of the different subsamples.

Following (6], we distinguish between "sampling' and "testing' plans. The sampling plan is the physical procedure used to form a representative sample from a bulk load of grains. Weil established such sampling plans are available from GIPSA, Grain Inspection, Packers, and Stockyards Administration of USDA (1 OJ and we don't consider them here. Once such a sample, thought to be as representative as a completely random sample, has been obtained, subsamples are taken and analysed do detect GMO. The way this is done is the testing plan. Severa! testing plans using the control by attribute of the subsamples are proposed in [6). Similar testing plarrs had been described previously for the detection of viruses or bacteria by [START_REF] Maury | Group analysis using ELISA: determination of the level of transmission of Soybean Mosaic Virus in soybean seed[END_REF], [START_REF] Maury | Seed certification for viruses. ln: Plant virus, disease control[END_REF]. The subsamples are called "pools' in one case (6), "groups' in the other [START_REF] Maury | Group analysis using ELISA: determination of the level of transmission of Soybean Mosaic Virus in soybean seed[END_REF], but the approaches described in these articles are essentially the same. Following (4) we shall refer to this kind of control as group analysis.

Testing schemes using the control by attributes are also recommended by GIPSA and used by numerous seed producers and grain exporters. ln [START_REF] Gipsa | Sampling and Testing Recommendations for the Detection of Cry9C Protein in Hybrid Seed Corn[END_REF], such a control is described and recommended for the detection of Starlink, a maize developed by Aventis CropScience which produces a protein Cry9C with insecticidal properties effective in controlling the European corn borer and which was approved for use as animal feed only. ln that case, the GIPSA proposai to check that the lot does not include Starlink kernels is to ground and test enough grains to give the buyer, if no GMO is found in them, a very low probability of accepting a lot with an unacceptable GMO rate. For instance if a p-.roportion above 0.3% is considered unacceptable, 2300 grains have to be used to get a 0.1 % prob.ability of accepting a lot reaching this 0.3% GMO rate. Since detection is made in that case through the expressed protein Cry9C, it is recommended to perform the analysis on separate subsamples of sf.ze -100 insuring that even 1 GM grain in the subsample is reliably detected. The lot is accepted if n::me of the subsamples contains GMO. Thus the GIPSA procedure also uses subsamples and their a~rib'Jtes, but the size of these subsamples is only dictated by the limit of the analytical method of d-etection and does not take into account the seller risk to see his lot refused when there is a slight fortuitous GMO presence. ln this paper the seller and buyer risks are both taken into account. The testing plans studied are t.ased on the simple or double control by attributes [START_REF] Schilling | Acceptance sampling in quality contrai[END_REF]. They are called single-stage or double stage testing by [6). For each of them, we describe a practical algorithmic way to get the cheapest testing p :an keeping both the buyer and the seller risks below a predetermined level. A similar optimisation is done by a program like (5) for ordinary quality control , but the approach is complicated here by the fact that one can play to optimise on the size of the subsamples as well as on their number. Moreover i, ï double contrai, the size need not be the same in the first and second stage. Modifying this size t ,etween the two stages can bring a lot more flexibility and consequently allow an important economy.

As indicated by its name, double control proceeds in two stages. A few subsamples are first tested. A second more important set of subsamples is then tested only if the first results leave some doubt. Since in many cases the first tests are conclusive, this double control may achieve the same risk c::mtrol with a cost far smaller than the simple control which test ail subsamples simultaneously.

These simple and double controls are described more precisely in section 2, the buyer and seller risk constraints in section 3. Section 4 presents the cost function to minimise. Section 5 then oescribes a minimisation algorithm for simple control first, then for double contrai. The results are it lustrated by some operating characteristic curves (figure 4). Their dependance on the cost of the k ernel nature, cost which is higher if the grains are commercial seeds, and much higher with breeder's seeds, clearly appears.

Simple and double control

ln a simpre control. N groups of n grains are separately ground and analysed to determine if they are GMO positive or not. If there are X out of the N groups including GMO, the GMO proportion is estimated by X/N and the lotis accepted if X SA, refused if X > A, where Ais a predetermined acceptance threshold.

As already mentioned, it may be more economicar to use a double contrai instead. First N1 groups of 11 1 grains are tested. The lot is accepted if X 1 S A 1 where Xi is the number of groups including GMO and .4 1 a predetermined threshold. If X 1 ;::: R 1 , where Ri is a predetermined rejection threshold, the lotis refused. ln between, that is if .4 1 < X 1 < R 1, N2 new groups are tested. The lot is men accepted if X 2 S A 2 (Xi), where X 2 is the number of those N2 new groups which include GMO and .•h(X 1 ) a predetermined threshold. The function A 2 : X1 i--+ A-2{X 1 ) giving for each value of X 1

the acceptance threshold at the second step must be a decreasing function of X 1 because the bigger ès X 1 , the smaller must be X 2 to compensate.

Buyer and seller risks

The aim of a control is to insure the buyer that the lot is refused with high probability whenever the proportion of GM kernels is above a non tolerable threshold Pnt, called Low Quality Level_(LQL) (X" Consumer Quality Level (COL) in quality control. But for the seller sake, there must be also a high probability to accept if the GMO proportion is below a tolerable threshold Pt called Acceptable Ouality Level (AOL) or Producer Qality Level (POL) in quality control. Of course, the tolerable threshold must be smaller than the non tolerable one, that is Pt < Pnt, otherwise there cannot be any agreement between the buyer and the seller.

The buyer requirement can thus be formalised by the inequality Prob (acceptance I Pnt) ~ /3

(1)

which means that the risk for the buyer to accept the lot if the GMO proportion reaches the non tolerable threshold must be smaller than /3. Similarly the seller requirement is expressed by the in equality

Prob (refusai I Pt) ~ a (2)
meaning that his risk to refuse if the GMO proportion is the tolerable one Pt does not exceed a. These maximum tolerated risks /3 and a are called buyer and seller risks respectively.

The choice of Pnt , f3, Pt , a de pends on many considerations: risk for humans, risk for environ ment, oegree of purity that can be obtained, nature of the kernels (commercial seeds, basic seeds, breeder's seeds, grain for human food, for animal feed, etc ... ). Once there is an agreement between contractors on their choice, the problem is to find the testing scheme leading to a minimal cost among tiïose which satisfies the constraints ( 1) and ( 2). This cost mainly depends on the number of tests and kernels. ln the next section, its expression is formalised for the two kinds of control considered, the simple and the double.

Cost function

We let C 9 be the cost of testing one group, that is the cost of the whole sequence of operations t.;.Sed to detect GMO in this group (grinding, protein or DNA extraction, immunological or PCR metiïod). Since in simple control there are N such tests, the global cost of test is NC 9 . Toit must be added the cost of the kernels making up the subsamples which strongly depends on their nature ( ::>rdinary grains, commercial seeds, breeder's seed . .. ). This cost is CkNn if Ck is the cost of one kernel. The whole cost therefore takes the form (3) 1-: is always possible to assume that Cg = l, that is to take the test cost as unit price. The cost Ck is t"1en relative to this test cost. For instance Ck = 0.001 if the price of one kernel is 1/1000 of the test price, or equivalently if the cost of a test is equivalent to the cost of 1000 grains. ln double control, the cost is random since the second step only occurs if A 1 < X 1 < R 1 , hence ' N ith a probability denoted by Prob(step 2lp) which depends on the real GMO proportion p. lt is the expectation of this cost for a given p which has to be optimised. This expectation is

C = C(N1,n1) = C 9 N1 + CkN1n1 + Prob(step 2lp) C(N2,n2) + Prob(step 2 jp) (CgN2 + CkN2n2) (4)
where C is defined as in simple control by [START_REF] Maury | Seed certification for viruses. ln: Plant virus, disease control[END_REF]. ln this form it is assumed that the N 2 n 2 kernels needed for the second step have to be paid only if this second step occurs. ln practice, it may be n ecessary to get and pay the N 2 n 2 kernels of the second stage even if they remain unused, in order b avoid a second sampling in the lot and because it may be difficult to return them . The cost then t:akes the following form [START_REF] Qalstat | Logiciel pour PC[END_REF] Though we consider here only the first form (4) of the cost, it is not difficult to adapt the methodology ro the second form.

The parameter p appearing in (4) and ( 5) is unknown. To get an idea of how the optimal testing scheme depends on it, two values Pt and Po = pt/10 will be given toit in this paper. Similarly, the ratio Ck/C 9 giving the cost of a grain relatively to the cost of analysis of a subsample will also be given two values 0.001 and 0.01. The cost defined by ( 3) and ( 4

Case of the simple control

Let p be the proportion of GM kernels in the lot. The sample used for the test is assumed to be representative of the lot so that each kernel in it has probability p to be GMO, independantly of the other kernels. The probability that no kernel is GMO in a group of n kernels is (1p)n and consequently the probability that a group contains at least one GM kernel is p = l -(l -pt. [START_REF] Schilling | Acceptance sampling in quality contrai[END_REF] Tne number X of groups among the N including GM kernels follows a binomial law B(N,P) so that the acceptance and refusai probabilities are respectively

A Prob(X ~ Alp) = ~ (~)P 20 (l-P)N-z, N Prob(X > Alp) = 1 -Prob(X ~ Alp) = L ( ~) P 20 (1 -P)N-z . z=A+l (8)
The buyer requirement (1) is that the acceptance probability is smaller then f3 when p = Pnt, the s~ller one (2) that the refusai probability is smaller than a: when p = Pt:

Prob(X ~ Alpnt) ~ /3, Prob(X > AIPt) ~ a: . (9)
These probabilities are given by [START_REF] Gipsa | Sampling and Testing Recommendations for the Detection of Cry9C Protein in Hybrid Seed Corn[END_REF] where P takes the corresponding values Pnt and Pt:

Pnt = 1 -(1 -Pntt , Pi = 1 -(1 -v t) n.
The problem is to find N, n and A minimising (3) and satisfying the constraints [START_REF] Gipsa | GIPSA. Grain Inspection Handbook, Book 1, Grain Sampling[END_REF].

Let us first consider fixed values of N and n. lt is easy to determine the acceptance numbers A 1 -sading to a consumer risk smaller than {3, if any. They are the integers A satisfying I'"' there is at least one such integer, we denote by A max the greatest of them, defined by

Prob(X ~ ÂmaxlPnt) ~ f3, Prob(X ~ 1 + AmaxlPnt) > /3.
Similar1y the acceptance numbers A giving a producer risk smaller than a: are defined by 1/\/e denote by Amin the smallest one defined by Prob(X ~ AminlPt) ~ 1 -a:, Prob(X ~ Amin -llPt) < 1 -a:. 10) is satisfied at least for A = 0, then .the A satisfying both the buyer and seller constraints [START_REF] Gipsa | GIPSA. Grain Inspection Handbook, Book 1, Grain Sampling[END_REF] are those lying between these two values: Amin ~A~ Amax• To illustrate the methodology, we adopt in the sequel of this article the following values for the parameters defining the constraints: Pnt = 1%, /3 = 5%, Pt= 0.2%, a:= 5%.

(10) ( 11) (12) (13) If (

(14)

Note that the 1% value for Pnt is the current European threshold for food labelling.

For these values, figure 1 represents the evolution of Amax ( +) and Amin {_) in function of N for n = 300. For a fixed n, the cheapest choice of N compatible with the constraints ( 9) is the smallest iinteger 1 Y such that Amin ~ Amax, that is such that _ is below + or at the same level. Any integer value between Amin and Amax is then valid for A. ln the case of the figure 1 where n = 300 and the constraint parameters are defined by ( 14), the smallest N is 7 and for it Amin = A max = 5 so that n ecessarily A = 5.

Tne figure suggests the following algorithm to find the smallest N associated with a given n. The difference Amax -A min is negative for small values of N (N < 7), then oscillates around O in a small range of values of N (7 ~ N ~ 11) and finally become positive for larger values of N (N > 11). This p rompts to find a value of N such that A min = Amax by a dichotomie process and then to look for the minimum N such that A mi n = A max in the vicinity of the found solution. ln the example of figure 1, the dichotomie process gives as first solution N1 = 11, and the comput ation of A max and A min for the values of N below 11 then gives the solution N = 7. Sorne preliminary c omputations led to the conclusion that this algorithm works quite generally provided about 20 values o f JY are explored below the first minimum found by the dichotomie process.

Such a search for N is very fast and can be easily done for ail feasible values of n. This allows t :::> draw a graph like the one in figure 2 giving for each n the minimum acceptable N and the corresponding value of A . Note that about 20 seconds were necessary on a 366 Mhz microcomputer to get !:i'le table giving for each n between 50 and 1000 the corresponding N , table from which the figure is made.

The minimum acceptable number of groups N is always greater or equal to 7. The smaller value o f n leading to this minimum is 204. The corresponding acceptance threshold is A = 4.

The corresponding testing scheme tests the presence of GMO in 7 groups of 204 kernels and accept the lot if the number X of groups where GMO is detected is below 4: X ~ 4. This scheme guarantees that the buyer risk to accept a lot with more than 1 % GMO and the seller risk to reject a lot with less than 0.2% GMO are both below 5%. Note that this testing scheme does not minimise the number Nn of kernels used and is therefore not always the optimal choice. Consider for instance the two values of Ck introduced in section 4. If

C" = C 9 /

Case of the double control

The double control allows to reach the same risk targets with a much lower cost. Let P1 = 1 -(1 -;,) "' and P 2 = 1 -(1-p)" 2 . The probability to accept the lot at the first step is

Prob(X 1 s A1 IP) = t (~' :)Pt 1 (1-Pi)1"'i -xi . x1=0 (15)
There is a second step only if X 1 takes a value x1 such that A1 < x1 < Ri. ln that case the lotis accepted if X 2 s .4 2 (x1), hence with probability

Prob(X 2 s A 2 (xi) lp) = :t) (~:)pf2(l -A)N2-x2 . ( 16
)
As the probability to get X1 = x 1 and

X 2 s A 2 (xi) is Prob(X1 = xilp) Prob(X2 s A2(x1) lp), the p robability of acceptance when A 1 < X 1 < R 1 is R1 -l L Prob(X1 = x1 IP) Prob(X2 S A2(x1) lp)

Finding an optimal double control scheme

To determine an optimal double contrai scheme in classical quality control, Daudin et al. [START_REF] Daudin | Plans de controle double optimaux[END_REF] first vary the parameters of the testing plan continuously in lR, then select integer values in the vicinity o: the real optimal solution. ln GMO control, the cost is strongly dependant on the number of tested grnups. Therefore only small values of N 1 and N 2 have to be examined and it is possible to work dï rectly on sets of integer parameters. The number of possible values for n 1 , n 2 is however too ir.iportant to examine ail of them. So the optimisation is carried out in two steps. First for each possible s,-at of parameters T = (N 1 ,A 1 ,R 1 ,N 2 ,A 2 ), the optimal couple (n1 ,112) satisfying the constraints, if a.,y, is looked for and the associated cost C(T) computed. Then the optimal set T is obtained by e::::,mparison between these C(T) for ail possible T.

Figure 3 illustrates the constraints on (11 1 ,n 2 ) for two choices of T = (N1 ,A1 ,Ri ,N2,A2), with the c::::,nstraint parameters {14). To satisfy the buyer and seller constraints

-1 e point ( n 1 ,n 2 ) must be above the curve B (Buyer curve) defined by P 0 (pnt) = f3 and below the cJrve S (Seller curve) defined by 1 -P 0 (pt) = a. If the area thus defined is empty as in figure 3.ii, tïere is no couple (n 1 ,n 2 ) satisfying the constraints. When it is not empty as in figure 3.i, the following s:ep is to find the couple giving the minimum cost.

,.. T o satisf)• the buyer constraint, the couple (n1 ,n2) must be above curve B. lt must be below curve S to satisfy :lie seller constraint. Thus B and S are respectively the bottom and top borders of the constraint area. Figure i) illustrates a situation where this admissible area, below S and above B, is not empty while figure ii) illustrates on :.he contrary a situation v.here the buyer and seller constraints cannot be simultaneously satisfied.

The figure 3 suggests the following specific algorithm to determine if the constraint area is empty or not. The minimum of the difference curve D = B -S is looked for. This difference D appears to be first decreasing, then increasing in function of n 1 . lt is easy to find its minimum by a dichotomie process, as the point where its derivative in function of n 1 is zero. If B is below S at this minimum, there is a couple (n 1 ,n 2 ) satisfying the constraints and the constraint area, bordered at its top by S and at its bottom by B, is not empty. ln that case, the value of n1 corresponding to the point at the extreme left of the constraint area can be easily found as the value such that B -S = O.

For n 1 tixed, it appears from (6) that the optimum n2 is the smallest one compatible with the constraints, that is the one associated to n 1 on the B curve. So the following optimisation step is to find the minimum cost along the buyer curve B.

ln most cases, the cost C given by (6) appears to be first decreasing, then increasing when moving from the left to the right on the buyer curve. A dichotomie process can be used again to find the zero o~ its derivative dC / dn 1 with respect to n 1 . The corresponding point on the B curve gives the searched optimum. ln some case however, it gives only a local optimum but it was observed that this occurs o:ily for parameters N 1 , A 1 , R 1 , N 2 , A 2 which are far from the optimum.

When C" = O and p small, the derivative dC /dn 1 is already positive at the leftest point of the ex>nstraint area. This point is then optimal. This is for instance the case in figure 3 For p sufficiently small, this quantity increases with P hence with n 1 and so does C.

lt is crucial in the sequence of operations leading to the optimum choice of (n 1 ,n2) to have an 1=tficient way of determining the n 2 associated to a given n 1 on the Sand B curves. These values are found as the solutions of the equations 1 -Pa(Pt) = a and P 0 (pnt) = /3. lt can be easily proved that f.:lr fixed values of the other parameters, the acceptance probability P 0 (p) is a decreasing function of r. 2 • This result can be used to salve efficiently these equations in n 2.

Example. The algorithm is used with the parameters defined by ( 14). The number of groups N1 is ,,aried between 1 and-! and .4 1 , Ri among all possible compatible sets of values. Then N2 is varied between 1 and 10 and .4 2 among all compatible decreasing acceptance function A 2 .

There are 6017 possible combinations (Ni ,Ai ,R 1 ,N 2 ,A 2 ) to explore. For 3899 of them, D = B -~ is negative at its minimum and so there exists a couple (ni ,n2) satisfying the buyer and seller c onstraints. For each of these 3899 combinations, the couple (n 1 ,n2 ) at the left of the constraint area, i.e. with minimum n i , is first looked for. lt appears that this couple minimises the cost function C(p,O) ;iven by (6) for the two values Pt and Po of p introduced in section 4.

Tuen optimas are searched along the B curve for the cost functions C(p,Ck) where p takes the 1 ,alues Po = 0.02%, p, = 0.2% and Ck the values 1/1000, 1/100 (Ck is expressed as in (6) with the . :.irice of the group test as unit price, i.e. C 9 = 1).

The whole search take approximately 40mn on a 366 Mhz microcomputer, i.e. about 30mn to get tïe 3899 admissible conditions with the couple (n 1 ,n 2 ) at the left of the constraint area, then about :.omn to get the corresponding optimal ni for the four costs with Ck :j; O. ln many cases, it can be i ,imediately checked that these last ones coïncide with the former value ni. Table 2 gives the optimal :esting schemes thus obtained. Note that most of the time is spent on condition N 1 = 4 which appears i :,teresting only to minimise the cost computed with p = Pt, C" = 0.01.

The statistical properties of a testing scheme are well summed up by the operating characteristic curve representing the acceptance probability P 0 (p) in function of p. This probability is given by (17) in the double contrai, by [START_REF] Gipsa | Sampling and Testing Recommendations for the Detection of Cry9C Protein in Hybrid Seed Corn[END_REF] in the simple one. Figure 4 gives this curve for some simple and double :esting schemes. The double control scheme 4 in this figure uses only one test in the first step and goes to step 2 with probability 0.06 if p = p 0 = 0.0002 and 0.49 if p = Pt• lt is far less expensive than :he simple contrai optimal testing scheme 3•with N = 7 which gives a similar operating characteristic curve. The simple contrai 1 would be adopted to limit to 5% the risk of accepting a lot with 1 % GMO content if, like in [START_REF] Gipsa | Sampling and Testing Recommendations for the Detection of Cry9C Protein in Hybrid Seed Corn[END_REF], one does not care about the seller risk.

Thus an appropriate choice of a testing scheme by attribute can lead to a quite economical contrai :aking into account both the buyer and seller requirements. ln some cases, this testing scheme can iead to acceptance even if some tested subsamples are GMO positive. This tact must be explained to users as perfectly coherent with the agreement reached by sellers and buyers on the choice of a non zero tolerable threshold Pnt . These testing schemes have still to be compared to testing schemes using the very sensitive quantitative response provided by quantitative real time PCR, which could be more adequate in some cases but need more work to know which factors are influencing the distribution of the quantitative response. -1 -Sorne testing scheme operating characteristic curves with constraint parameters (14} ~ and 5 are the double contrai testing schemes respectively minimising the costs C(0.02%,0.001) and C(0.2%,0.001) onder the buyer and seller constraints defined by (14) (see table 2). 3 gives the cost optimal simple contrai when C k/C 9 = 1/1000 under the same constraints (see table 1). The simple contrai testing scheme 1 takes only the :iuyer constraint into account, while the testing scheme 2 shows what can be achieved with a simple contrai if no ::::iore than 3 groups are to be tested.

  ) with given p, Ck and Cg =lis denoted by C(p,Ck): (6) 5 Cost minimisation of group analysis contrai by attributes 5.

  x1=A1+l and finally the global probability of acceptance, denoted by P0 (p), is R1 -l P 0 (p) = Prob(X1 :S: A1IP) + L Prob(X1 = X1IP) Prob(X2 :S: A2(x1) lp) z1=A ,+l = J~o (~: )Ft''(l -Pi)N1-z1 + (17) Rf l ( ~:) Pf' (1 -Pi )N1 -z1 z1=A1+l

FIG. 3 -

 3 FIG. 3 -Constraints for n 1 and n 2 with the parameters in {14) B (Buyer curve)

  cost C(p,Ck) Parameters of the testing plan Ni n1 A1 Ri N2 n2

  FIG.-1 -Sorne testing scheme operating characteristic curves with constraint parameters (14}

  1000, this scheme minimises the cost function[START_REF] Maury | Seed certification for viruses. ln: Plant virus, disease control[END_REF] but if Ck = C 9 /100 then the cheapest choice is 1\' = 8, n = 164, A = 4. Table1illustrates this point. = N + 0.00lNn 19.1 15.4 10.3 9.3 10.6 10.8 10.8 8.4 8.5 10.9C(N,11) = N + O.OINn 28.8 28.0 21.6 21.1 25.2 27.0 27.3 21.3 21.6 27.8 L~B . 1 -Minimum N and associated costs for some values of n, constraints parameters (14} E.xample: if each group bas n = 204 grains, the buyer and seller requirements can be simultaneously satisfied only if N ~ 7, and for N = 7, A must be equal to 4. However, if the grain cost is e.g 1% of a one group test cost, h-e. nce proportional to N + O.OlNn, then it is cheaper to use N = 8 groups of 164 grains than N = 7 groups of

	n	60	100	140	164		180	200	203 , 204	208	209
	N	18	14	9	8		9	9	9	7	7	9
	A	4	5	4	4		5	5	5	4	4	5
	Nn	1080 1400 1260 1312 1620 1800 1827 1428 1456 1881
	C(N,n) 2ü4 grains
	C .Ë
	~ 20
	.,j
	~ 18
	]6
	H
	12
	10
	a
	6
	1
	100	200	300	100	SOO	600	100	800	900	1 000
										n
	FIG. 2 -Minim11m .V and corresponding A in f1mction of n, constraint parameters {14)

-:-be graphie gï,•es an information similar to that of table 1. The constraints remain those defined by (14). For ::. fixed n in abscissa, the symbol * gives the minimum acceptable N, the symbol . the corresponding A. The 2.ccumulation of these symbols forms respectively thick (*) and t hin ( . ) lines. The minimum N of 7 is obtained -•hen n = 204 as in table

1

.

  .i. The optimum is obtained for ni = 393, n 2 = 330 when Ck = O and p = p 0 . To explain this, note that when Ck = 0, the C:)St (6) becomes C(p,O) =Ni+ Prob(step 21p)N 2 . lt does not depends on n 2 and its dependance on r. 1 is only through Prob(step 21 p) which can be written

	R 1 -l Prob(step 2 lp) = L ci	1 Pi(1-P)Ni-i, where P = l -(1 -p)n' .	(19)
	j=A1 + l

  Optimal testing parameters for some cost function C(p,Ck) in double contrai E.xample: if the me.an GMO rate is p = 0.02% and the cost of a kernel about 1 % of the cost of one group test, the more economical double contrai tests first 1 group of 314 grains. The lot is accepted if the result is negative, o-:hel"\\;se 9 other groups of 182 grains are tested and the lot accepted only if Jess than 4 of them are GMO p,:isiti\'e.

							A2
		C(0.02%,0)	1 333	0	2	6 339	(4)
		C (0.02%,0.001)	1 333	0	2	6 339	(4)
		C (0.02%,0.01)	1 314	0	2	9 182	(4)
		C(0.2%)	2 392	1	3	5 601	(4)
		C (0.2%,0.001)	2 393	1	3	5 330	(3)
		C(0.2%,0.01)	4 155	1	5	5 147 (2,1,0)
	T.~B. 2 -1 simple contrai
	2	simple contrai
	3	simple control
	4	double contrai
	5	double control
	,::-

"' "-' a. 9


Javier Esparza

Anca Muscholl

Igor Walukiewicz

Static Analysis of Deterministic Negotiations

Negotiation diagrams are a model of concurrent computation akin to workflow Petri nets. Deterministic negotiation diagrams, equivalent to the much studied and used free-choice workflow Petri nets, are surprisingly amenable to verification. Soundness (a property close to deadlock-freedom) can be decided in PTIME. Further, other fundamental questions like computing summaries or the expected cost, can also be solved in PTIME for sound deterministic negotiation diagrams, while they are PSPACE-complete in the general case.

In this paper we generalize and explain these results. We extend the classical "meet-over-all-paths" (MOP) formulation of static analysis problems to our concurrent setting, and introduce Mazurkiewicz-invariant analysis problems, which encompass the questions above and new ones. We show that any Mazurkiewicz-invariant analysis problem can be solved in PTIME for sound deterministic negotiations whenever it is in PTIME for sequential flow-graphs-even though the flow-graph of a deterministic negotiation diagram can be exponentially larger than the diagram itself. This gives a common explanation to the low-complexity of all the analysis questions studied so far. Finally, we show that classical gen/kill analyses are also an instance of our framework, and obtain a PTIME algorithm for detecting anti-patterns in free-choice workflow Petri nets.

Our result is based on a novel decomposition theorem, of independent interest, showing that sound deterministic negotiation diagrams can be hierarchically decomposed into (possibly overlapping) smaller sound diagrams.

Introduction

Concurrent systems are difficult to analyze due to the state explosion problem. Unlike for sequential systems, the flow graph of a concurrent system is often exponential in the size of the system, so that analysis techniques for sequential systems cannot be directly applied. One approach to analyze concurrent systems is to take a general model and design heuristics that work for relevant examples. Another, that we pursue in this paper, is to find a restricted class of concurrent systems and design provably efficient algorithms for particular analysis problems for this class.

In [START_REF] Esparza | On negotiation as concurrency primitive[END_REF] Esparza and Desel introduced negotiation diagrams, a model of concurrency closely related to workflow Petri nets. Workflow nets are a very successful formalism for the description of business processes, and a backend for graphical notations like BPMN (Business Process Modeling Notation), EPC (Event-driven Process Chain), or UML Activity Diagrams (see e.g. [START_REF] Trcka | Data-flow antipatterns: Discovering data-flow errors in workflows[END_REF], [START_REF] Van Der Aalst | Workflow verification: Finding controlflow errors using Petri-net-based techniques[END_REF]). In a nutshell, negotiation diagrams are workflow Petri nets that can be decomposed into communicating sequential Petri nets, a feature that makes them more amenable to theoretical study, while the translation into workflow nets (described in [START_REF] Desel | Negotiations and Petri nets[END_REF]) allows to transfer results and algorithms to business process applications.

A negotiation diagram describes a distributed system with a fixed set of sequential processes. The diagram is composed of "atomic negotiations", each one involving a (possibly different) subset of processes. An atomic negotiation starts when all its participants are ready to engage in it, and concludes with the selection of one out of a fixed set of possible outcomes; for each participant process, the outcome determines which atomic negotiations the process is willing to engage in at the next step. As workflow Petri nets, negotiations can simulate linearly bounded automata, and so all interesting analysis problems are PSPACE-hard for them.

A negotiation is deterministic if for every process the outcome of an atomic negotiation completely determines the next atomic negotiation the process should participate in. As shown in [START_REF] Desel | Negotiations and Petri nets[END_REF], the connection between negotiations diagrams and workflow Petri nets is particularly tight in the deterministic case: Deterministic negotiation diagrams are essentially isomorphic to the class of free-choice workflow nets, a class important in practice 1 and extensively studied, see e.g. [START_REF] Esparza | Reduction rules for colored workflow nets[END_REF], [START_REF] Esparza | Polynomial analysis algorithms for free choice probabilistic workflow nets[END_REF], [START_REF] Esparza | Soundness in negotiations[END_REF], [START_REF] Fahland | Instantaneous soundness checking of industrial business process models[END_REF], [START_REF] Farzan | Causal dataflow analysis for concurrent programs[END_REF], [START_REF] Favre | The relationship between workflow graphs and free-choice workflow nets[END_REF], [START_REF] Van Der Aalst | The application of Petri nets to workflow management[END_REF]). The state space of deterministic negotiations/free-choice workflow nets can grow exponentially in their size, and so they are subject to the state explosion problem. However, theoretical research has shown that, remarkably, several fundamental problems can be solved in polynomial time by means of algorithms that avoid direct exploration of the state space (contrary to other techniques, like partial-order reduction, that only reduce the number of states to be explored, and still have exponential worst-case complexity). First, it can be checked in PTIME if a deterministic negotiation diagram is sound [START_REF] Esparza | On negotiation as concurrency primitive II: Deterministic cyclic negotiations[END_REF], a variant of deadlock-freedom property [START_REF] Favre | The relationship between workflow graphs and free-choice workflow nets[END_REF] 2 . Then, for 1. For example, 70% of the almost 2000 workflow nets from the suite of industrial models studied in [START_REF] Esparza | Reduction rules for colored workflow nets[END_REF], [START_REF] Esparza | Efficient algorithms for pre * and post * on interprocedural parallel flow graphs[END_REF], [START_REF] Van Der Aalst | Workflow management: models, methods, and systems[END_REF] are free-choice.

2. About 50% of the free-choice workflow nets from the suite mentioned above are sound. sound deterministic negotiation diagrams PTIME algorithms have been proposed for: the summarization problem [START_REF] Esparza | Reduction rules for colored workflow nets[END_REF], the problem of computing the expected cost of a probabilistic free-choice workflow net [START_REF] Esparza | Polynomial analysis algorithms for free choice probabilistic workflow nets[END_REF], and the identification of some anti-patterns [START_REF] Esparza | Soundness in negotiations[END_REF].

In this paper we develop a generic approach to the static analysis of sound deterministic negotiation diagrams. It covers all the problems above as particular instances, and new ones, like the computation of the best-case/worstcase execution time. The approach is a generalization to the concurrent setting of the classical lattice-based approach to static analysis of sequential flow-graphs [START_REF] Katoen | GSPNs revisited: Simple semantics and new analysis algorithms[END_REF]. A flowgraph consists of a set of nodes, modeling program points, and a set of edges, modeling program instructions, like assignments or guards 3 . In the lattice-based approach one (i) defines a lattice D of dataflow informations capturing the analysis at hand, (ii) assigns semantic transformers [[a]] : D → D to each action a of the flow-graph, (iii) assigns to a path a 1 • • • a n of the flow graph the functional composition

[[a n ]] • • • • • [[a 1 ]
] of the transformers, and (iv) defines the result of the analysis as the "Merge Over all Paths", i.e, the join of the transformers of all execution paths, usually called the MOP-solution or just the MOP of the dataflow problem. So performing an analysis amounts to computing the MOP of the flow-graph for the corresponding lattice and transformers.

Katoen et al. have recently shown in [START_REF] Hecht | Flow Analysis of Computer Programs[END_REF], [START_REF] Eisentraut | A semantics for every GSPN[END_REF] that in order to adequately deal with quantitative analyses of concurrent systems, like expected costs, one needs a semantics that distinguishes between the inherent nondeterminism of each sequential process, and the nondeterminism introduced by concurrency (the choice of the process that should perform the next step). Following these ideas, we introduce a semantics in which the latter is resolved by an external scheduler, and define the MOP for a given scheduler. The result of a dataflow analysis is then given by the infimum or supremum, depending on the application, of the MOPs for all possible schedulers.

The contributions of the paper are the following:

(1) We present an extension of a static analysis framework to deterministic negotiation diagrams. In particular, we identify the class of Mazurkiewicz-invariant frameworks that respect the concurrency relation in negotiations. We prove a theorem showing a first important property of sound deterministic negotiations, namely that the MOP is independent of the scheduler for Mazurkiewicz invariant frameworks. This allows to compute the result of the analysis by fixing a scheduler, and computing the MOP for it. As an another motivation for Mazurkiewicz-invariant frameworks we observe that there are static analysis frameworks for which analysis is NP-hard, even for sound deterministic negotiation diagrams.

(2) The main contribution of the paper is a method to compute MOP problems for sound deterministic negotiation diagrams. The method does not require the computation of the reachable configurations. We prove a novel decomposition theorem showing that a deterministic negotiation diagram is composed of smaller subnegotiations involving only a subset of the processes, and that these subnegotiations are themselves sound. This allows us to define a generic PTIME algorithm for computing the MOP for Mazurkiewiczinvariant static analysis frameworks.

(3) Finally, we show that the problems studied in [START_REF] Esparza | Reduction rules for colored workflow nets[END_REF], [START_REF] Esparza | Polynomial analysis algorithms for free choice probabilistic workflow nets[END_REF], and others, are Mazurkiewicz-invariant. Further, we show that the MOP of an important class of analysesall four flavors of gen/kill problems, well known in the static analysis community -can be reformulated as invariant frameworks, and computed in PTIME.

Organization of the paper: Section 2 introduces the negotiation model and static analysis frameworks. Section 3 proves the decomposition theorem. Section 4 presents the algorithm to compute the MOP of an arbitrary Mazurkiewiczinvariant analysis framework. Section 5 deals with gen/kill analyses. Omitted proofs can be found in the extended version [?].

Related work.

As we have mentioned, deterministic negotiations are very close to free-choice workflow Petri nets, also called workflow graphs. Algorithms for the analysis of specific properties of these nets have been studied in [START_REF] Esparza | Reduction rules for colored workflow nets[END_REF], [START_REF] Esparza | Polynomial analysis algorithms for free choice probabilistic workflow nets[END_REF], [START_REF] Esparza | Soundness in negotiations[END_REF], [START_REF] Fahland | Instantaneous soundness checking of industrial business process models[END_REF], [START_REF] Farzan | Causal dataflow analysis for concurrent programs[END_REF], [START_REF] Favre | The relationship between workflow graphs and free-choice workflow nets[END_REF], [START_REF] Seidl | Constraint-based inter-procedural analysis of parallel programs[END_REF], [START_REF] Van Der Aalst | The application of Petri nets to workflow management[END_REF]. We have already described above the relation to these works.

We discuss the connection to work on static analysis for (abstract models of) programming languages. The synchronization-sensitive analysis of concurrent programs has been intensively studied (see e.g [START_REF] Bouajjani | Analysis of recursively parallel programs[END_REF], [START_REF] Chugh | Dataflow analysis for concurrent programs using datarace detection[END_REF], [START_REF] Esparza | Static analysis of deterministic negotiations[END_REF], [START_REF] Fahland | Dynamic skipping and blocking and dead path elimination for cyclic workflows[END_REF], [START_REF] Farzan | Compositional bitvector analysis for concurrent programs with nested locks[END_REF], [START_REF] Favre | Diagnostic information for control-flow analysis of workflow graphs (a.k.a. free-choice workflow nets)[END_REF], [START_REF] Karp | Parallel program schemata[END_REF], [START_REF] Lammich | Conflict analysis of programs with procedures, dynamic thread creation, and monitors[END_REF], [START_REF] Ramalingam | Context-sensitive synchronization-sensitive analysis is undecidable[END_REF], [START_REF] Schwarz | Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol[END_REF]). A fundamental fact is that interprocedural synchronization-sensitive analysis is undecidable [START_REF] Lammich | Conflict analysis of programs with procedures, dynamic thread creation, and monitors[END_REF], and intraprocedural synchronization-sensitive analysis has high complexity (ranging from PSPACE-completeness to EXPSPACE-completeness, depending on the communication primitive), see e.g. [?]). This is in sharp contrast to the linear complexity of static analysis in the size of the flow graph for sequential programs, and causes work on the subject to roughly split into two research directions. The first one aims at obtaining decidability or low complexity of analyses by restricting the possible synchronization patterns. Many different restrictions have been considered: parbeginparend constructs [START_REF] Esparza | Static analysis of deterministic negotiations[END_REF], [START_REF] Schwarz | Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol[END_REF], generalizations thereof (see e.g. [START_REF] Karp | Parallel program schemata[END_REF]), synchronization by nested locks (see e.g. [START_REF] Fahland | Dynamic skipping and blocking and dead path elimination for cyclic workflows[END_REF]), and asynchronous programming (see e.g. [START_REF] Favre | Diagnostic information for control-flow analysis of workflow graphs (a.k.a. free-choice workflow nets)[END_REF]). The other direction does not restrict the synchronization patterns, at the price of worst-case exponential analysis algorithms (see e.g. [START_REF] Chugh | Dataflow analysis for concurrent programs using datarace detection[END_REF], [START_REF] Farzan | Compositional bitvector analysis for concurrent programs with nested locks[END_REF], where control-flow of parallel programs is modelled by Petri nets, and a notion similar to Mazurkiewicz invariance is also used).

Compared with these papers, the original feature of our work is that we obtain polynomial analysis algorithms without restricting the possible synchronization patterns; instead, deterministic negotiation diagrams restrict the interplay between synchronization and choice. This distinction can be best appreciated when we compare these formalisms, but excluding choice. In the programming languages of [START_REF] Esparza | Static analysis of deterministic negotiations[END_REF], [START_REF] Fahland | Dynamic skipping and blocking and dead path elimination for cyclic workflows[END_REF], [START_REF] Favre | Diagnostic information for control-flow analysis of workflow graphs (a.k.a. free-choice workflow nets)[END_REF], [START_REF] Karp | Parallel program schemata[END_REF], [START_REF] Schwarz | Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol[END_REF], excluding choice means excluding ifthen-else or alternative constructs, while for deterministic negotiations it means considering the special case in which every node has exactly one outcome. Sound deterministic negotiation diagrams can model all synchronization patterns given in terms of Mazurkiewicz traces, which is not the case for the formalisms of [START_REF] Esparza | Static analysis of deterministic negotiations[END_REF], [START_REF] Fahland | Dynamic skipping and blocking and dead path elimination for cyclic workflows[END_REF], [START_REF] Favre | Diagnostic information for control-flow analysis of workflow graphs (a.k.a. free-choice workflow nets)[END_REF], [START_REF] Karp | Parallel program schemata[END_REF], [START_REF] Schwarz | Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol[END_REF]. For example, the languages of [START_REF] Esparza | Static analysis of deterministic negotiations[END_REF], [START_REF] Schwarz | Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol[END_REF] cannot model a synchronization pattern with three processes A, B, C in which first A synchronizes with B, then A synchronizes with C, and finally B synchronizes with C. Observe that on the other hand, negotiations are finite state, whereas the other formalisms we have mentioned have non-determinism, recursion, and possibly, thread creation.

Negotiations

A negotiation diagram N is a tuple Proc, N, dom, R, δ
, where Proc is a finite set of processes (or agents) and N is a finite set of nodes where the processes can synchronize to choose an outcome. The function dom : N → P(Proc) associates to every node n ∈ N the (non-empty) set dom(n) of processes participating in it. Nodes are denoted as m or n, and processes as p or q; possibly with indices. The set of possible outcomes of nodes is denoted R4 , and we use a, b, . . . to range over its elements. Every node n ∈ N has its set of possible outcomes out(n) ⊆ R.

The control flow in a negotiation diagram is determined by a partial transition function δ : N × R × P • -→ P(N ), telling that after the outcome a of node n, process p ∈ dom(n) is ready to participate in any of the nodes in the set δ(n, a, p). So for every n ∈ δ(n, a, p) we have p ∈ dom(n ) ∩ dom(n), and for every n, a ∈ out(n) and p ∈ dom(n) the result δ(n, a, p) is defined. Observe that nodes may have one single participant process, and/or have one single outcome. A location is a pair (n, a) such that a ∈ out(n), and we define its domain as dom(n). Example: Figure 1 shows a negotiation diagram for (a slight modification of) the insurance claim example of [START_REF] Trcka | Data-flow antipatterns: Discovering data-flow errors in workflows[END_REF] (see also Fig. 2 ---→ C . For example, in Figure 1 we have

C (n0,reg) -----→ C for C(D 1 ) = {n 0 } = C(D 2 ) and C (D 1 ) = {n 1 }, C (D 2 ) = {n 2 }.
A run of a negotiation diagram N from a configuration C 1 is a finite or infinite sequence of locations w = (n 1 , a 1 )(n 2 , a 2 ) . . . such that there are configurations C 2 , C 3 , . . . with

C 1 (n1,a1) ----→ C 2 (n2,a2) ----→ C 3 . . .

We denote this by

C 1 w -→, or C 1 w -→ C k if
the sequence is finite and finishes with C k . In the latter case we say that C k is reachable from C 1 on w. We simply call it reachable if w is irrelevant, and write C 1 * -→ C k . Negotiation diagrams come equipped with two distinguished initial and final nodes n init and n fin , in which all processes in Proc participate. The initial and final configurations C init , C fin are given by C init (p) = {n init } and C fin (p) = {n fin } for all p ∈ Proc. A run is successful if it starts in C init and ends in C fin . We assume that every node (except for n fin ) has at least one outcome. In Figure 1, n init = n 0 and n fin = n 7 .

A negotiation diagram N is sound if every partial run starting at C init can be completed to a successful run. If a negotiation diagram has no infinite runs, then it is sound iff it has no reachable deadlock configuration. The negotiation diagram of Figure 1 is sound.

Process p is deterministic in a negotiation diagram N if for every n ∈ N , and a ∈ R, the set δ(n, a, p) of possible successor nodes is either a singleton or the empty set. A negotiation diagram is deterministic if every process p ∈ Proc is deterministic. The negotiation diagram of Figure 1 is deterministic.

The graph of a negotiation diagram has N as set of vertices, and there is an edge n

p,a --→ n iff n ∈ δ(n, a, p). Observe that p ∈ dom(n) ∩ dom(n ).
A negotiation diagram is acyclic if its graph is acyclic. Acyclic negotiation diagrams cannot have infinite runs, so as mentioned above, soundness is equivalent to deadlockfreedom.

Static analysis frameworks

Let (D, , , , ⊥, ) be a complete lattice. A function

f : D → D is monotonic if d d implies f (d) f (d ), and distributive if f ( D ) = {f (d) | d ∈ D }.
An analysis framework 5 of a negotiation diagram is a lattice together with a mapping [[ ]] that assigns to each outcome a monotonic and distributive function [[ ]] in the lattice. Abusing language, we use [[ ]] to denote a framework.

A negotiation diagram has two kinds of nondeterminism, one that picks a node among the ones enabled at a configuration, and a second kind which picks an outcome. We distinguish the two by letting a scheduler to decide the first kind. This is an important design choice, motivated by modeling issues: In distributed systems, one often has information about how the outcomes are picked, but not about the way nondeterminism due to concurrency is resolved. In particular, one may have probabilistic information about the former, but not about the latter. This point has been discussed in detail by Katoen et al. [START_REF] Hecht | Flow Analysis of Computer Programs[END_REF], [START_REF] Eisentraut | A semantics for every GSPN[END_REF], who also advocate the separation of the two kinds of nondeterminism.

A scheduler of N is a partial function S that assigns to every run

C init w -→ C a node S(w) enabled at C, if it exists. A finite initial run w = 1 • • • k , where i = (n i , a i ), is compatible with S if S( 1 • • • i ) = n i+1 for every 1 ≤ i ≤ k -1.
For example, a scheduler for the negotiation diagram in Figure 1 can give preference to n 1 and n 3 over n 2 . The successful runs compatible with this scheduler are given by the regular expression (omitting the nodes of the locations) reg send (tout|rec) eval (npr |pr (done nOK ) * doneOK ).

The abstract semantics of a finite run

w = 1 • • • k is the function [[w]] := [[ k ]] • [[ k-1 ]] • • • • • [[ 1 ]].
The abstract semantics of N with respect to a scheduler S is the function

[[N , S]] defined by [[N , S]] = [[w]] | w is a successful run of N compatible with S
where the extension of to functions is defined pointwise. The abstract semantics

[[N ]] of N is defined as either [[N , S]] | S is a scheduler of N , or as [[N , S]] | S is
a scheduler of N , depending on the application.

In classical static analysis, analysis frameworks are over flow-graphs, instead of negotiation diagrams [START_REF] Katoen | GSPNs revisited: Simple semantics and new analysis algorithms[END_REF]. Flowgraphs describe sequential programs. Loosely speaking, a flow-graph is a graph whose nodes are labeled with program 5. In [START_REF] Katoen | GSPNs revisited: Simple semantics and new analysis algorithms[END_REF] this is called a monotone and distributive framework.

points, and whose edges are labeled with program instructions (assignments or guards). The mapping [[ ]]

assigns to an edge the relation describing the effect of the assignment or guard on the program variables. We can see a flow-graph as a degenerate negotiation diagram in which all nodes have one single process. In this case every reachable configuration enables at most one node, and so there is a unique scheduler. So, in this case, the abstract semantics of a flow-graph is the standard "Merge Over all Paths" (MOP), defined by

[[N ]] = [[w]] | w is a successful run }.
[ ]](T ) = v∈T [[ ]]({v}). The semantics [[N ]]
is the relation that assigns to every initial valuation the possible final valuations after a successful run.

Detection of anti-patterns.

Actions in business processes generate, use, modify, and delete resources (for example, a document can be created by a first department, read and used by a second, and classified as confidential by a third). Anti-patterns are used to describe runs that do not correctly access resources; for example, a resource is used before it is created, or a resource is created and then never used. Examples of anti-patterns can be found in [START_REF] Seidl | Constraint-based inter-procedural analysis of parallel programs[END_REF]. They can be easily formalized as analyses frameworks. Consider for example two locations 1 and 2 that generate a resource, and a set K of locations that delete it. We wish to know if a given deterministic sound negotiation diagram has a successful run that belongs to

L = L * 1 (K) * 2 L *
where K denotes the set of locations not in K. In other words, is there a scenario where a resource is generated twice without deleting it in between.

To encode this problem in our static analysis framework, we take D = {0, 1, 2} with the natural order together with min, max as and , respectively. Intuitively, 0 says that the sequence does not have a suffix of the form 1 (K) * , 1 says that it has such a suffix, and 2 that it has a subword 1 (K) * 2 . The semantics of a location is a monotone and distributive function from D to D reflecting this intuition:

[[ 1 ]](x) = 2 if x = 2 1 otherwise [[ 2 ]](x) = 0 if x = 0 2 otherwise
6. Some classical literature uses instead of and speaks of the "Meet Over all Paths", but other standard texts, e.g. [START_REF] Katoen | GSPNs revisited: Simple semantics and new analysis algorithms[END_REF], use .

[

[ ]](x) =      x if ∈ K 2 if ∈ K and x = 2 0 if ∈ K and x = 0, 1 2.1.3. Minimal/maximal expected cost. We let D = {(p, c) | p ∈ R + 0 , c ∈ R}
, where we interpret p as a probability and c as a cost. We take

(p 1 , c 1 ) (p 2 , c 2 ) = (p 1 + p 2 , c 1 p 1 + c 2 p 2 ) and (p 1 , c 1 ) (p 2 , c 2 ) if p 1 ≤ p 2 and c 1 ≤ c 2 .
We define a function Prob :

N × R → [0, 1] such that Prob(n, a) = 0 if a /
∈ out(n), and a∈R Prob(n, a) = 1 for every n ∈ N . Intuitively, Prob(n, a) is the probability that node n yields the outcome a. We also define a cost function Cost : N × R → R that assigns to each result a cost.

Let

[[ ]]((p, c)) = p • Prob( ), c + Cost( ) . Then [[N , S]](1, 0)
gives the expected cost of N under the scheduler S (which may be infinite) and [[N ]](1, 0) is the minimal/maximal expected cost.

2.1.4. Best/worst-case execution time. Let R + 0 denote the nonnegative reals. A time valuation is a function v : Proc → R + 0 ∪ {∞} that assigns to each process p a time v(p), intuitively corresponding to the time that the process has needed so far. The elements of D are time valuations, with

(v v )(p) = max{v(p), v (p)} for every process p, and v v if v(p) ≤ v (p) for every process p,
We assign to each outcome = (n, a) and to each process p ∈ dom(n) the time t ,p that p needs to execute a.

The semantic function [[ ]] is given by

[[ ]](v) = v , where v (p) = v(p) if p / ∈ dom(n) max p ∈dom(n) v(p ) + t ,p if p ∈ dom(n)
This definition reflects that all processes in dom(n) must wait until all of them are ready, and then we add to them the time they need to execute . Since the initial and final atoms involve all processes, the abstract semantics [[w]] of a successful run has the form [[w]](v) = (max p∈Proc v(p) + t w (p)) p∈Proc , where t w (p) is the time process p needs to execute w. In particular, we have

[[w]](0) = t w . Then [[N , S]](0)
gives the best-case execution time for a scheduler S, and [[N ]](0) the infimum/ supremum over the times for each scheduler.

Maximal fixed point of an analysis framework

It is well-known that for sequential flow-graphs the MOP of an analysis framework coincides with the Maximal Fixed Point of the framework, or MFP. The MOP is the least fixed point of a set of linear equations over the lattice, having one equation for each node of the flow-graph 7 . The least fixed point can be approximated by means of Kleene's theorem, and computed exactly in a number of cases, including the case of lattices satisfying the ascending chain condition, but also others. For example, the lattice for the expected 7. Again, the name "maximal" has historical reasons. cost of a flow-graph does not satisfy the ascending chain condition, but yields a set of linear fixed point equations over the rational numbers, which can be solved using standard techniques.

In the concurrent case, the correspondence between MOP and MFP is more delicate. Given a scheduler S, we can construct the reachability graph of the negotiation diagram, corresponding to the runs compatible with S. If the graph is finite (for instance, this is always the case if the scheduler is memoryless, i.e., the node selected by the scheduler to extend a run depends only on the configuration reached by the run), then [[N , S]] can be computed as the MFP of this graph, seen as a sequential flow-graph. The corresponding set of linear fixed point equations has one equation for each configuration of the graph. However, this approach has two problems: In the remaining of this section we introduce a Mazurkiewicz-invariant analysis framework, and show that for this framework and for the class of sound deterministic negotiation diagrams we can overcome these two obstacles. In Section 2. If we remove any of the three conditions of our setting (Mazurkiewicz-invariance, soundness, determinism), then there exist frameworks with the following property: deciding if the MOP has a given value is polynomial in the sequential case (i.e., for flow graphs of sequential programs), but at least NP-hard for negotiations.

We sketch the NP-hardness proof for deterministic, sound negotiations where the framework is not Mazurkiewicz-invariant. Consider the NP-hard problem 1in-3-SAT, where it is asked if for a CNF formula with k variables and m clauses there is an assignment that sets exactly one literal true in each clause. We have k processes p 1 , . . . , p k , one for each variable x i . We describe the (acyclic) deterministic, sound negotiation N . The initial node of N has a single outcome, that leads process p i to a node with domain {p i }. From there p i branches for the two possible values for x i . The "true" branch is a line with outcomes corresponding to clauses that become "true" when x i is true, and analogously for the "false" branch -in both cases respecting the order of clauses. Let us denote by C j an outcome corresponding to the j-th clause. The lattice D has elements ⊥ < 1, . . . , (m + 1) < ; so there are m + 1 pairwise incomparable elements together with ⊥ and . For every node n and clause

C j we set [[(n, C j )]](j) = j + 1, [[(n, C j )]]( ) = and [[(n, C j )]](d) = ⊥ otherwise. More- over [[ ]]
is the identity function for all other locations . This framework is monotonic and distributive. For a run w of N we have

[[w]](1) = m+1 if the subsequence of clauses appearing in w is exactly C 1 . . . C m ; otherwise [[w]](1) = ⊥. Since [[N ]]
is the over all runs, we get that the 1-in-3-SAT instance is positive iff

[[N ]](1) = m + 1.
In the sequential case, the analysis can be done in polynomial time, since the lattice D → D has the height O(m).

The proofs of the other two cases (where determinism or soundness are removed) follow easily from a simple construction shown in Theorem 1 of [START_REF] Esparza | On negotiation as concurrency primitive[END_REF]: Given a deterministic linearly bounded automaton A and a word w, one can construct in polynomial time a negotiation N A having one single run that simulates the execution of A on the input w. This gives PSPACE-hardness for essentially all non-trivial frameworks, Mazurkiewicz invariant or not.

Mazurkiewicz-invariant analysis frameworks

We introduce the notion of Mazurkiewicz equivalence between runs (also called trace equivalence in the literature [START_REF] Diekert | The Book of Traces[END_REF]). Two equivalent runs started in the same configuration will end up in the same configuration. We call an analysis framework Mazurkiewicz-invariant if the values of equivalent runs are the same. We then show that the MOP of a Mazurkiewicz-invariant analysis is independent of the scheduler.

Definition 1. Two nodes n, m of a negotiation diagram are independent if dom(n) ∩ dom(m) = ∅. Two locations are independent if their nodes are independent. Given two finite sequences of locations w 1 , w 2 , we write w 1 ∼ w 2 if w 1 = w 1 2 w and w 2 = w 2 1 w for independent locations 1 , 2 . Mazurkiewicz equivalence, denoted by ≡, is the reflexive-transitive closure of ∼.

The next lemma says that Mazurkiewicz equivalent runs have the same behaviors.

Lemma 1. If C 1 w -→ C 2 and v ≡ w, then C 1 v -→ C 2 . In particular, if w is a (successful) run, then v is.
Interestingly Mazurkiewicz equivalence behaves very well with respect to schedulers. Lemma 2. Let N be a deterministic negotiation diagram and let S be a scheduler of N . For every successful run w there is exactly one successful run v ≡ w that is compatible with S.

We observe that Lemma 2 may not hold for runs that are not successful nor for non-deterministic negotiation diagrams.

We can now define Mazurkiewicz-invariant analysis frameworks, and prove that they are independent of schedulers.

Definition 2. An analysis framework is

Mazurkiewicz- invariant if [[ 1 ]]•[[ 2 ]] = [[ 2 ]]•[[ 1 ]
] for every two independent outcomes 1 , 2 . It turns out that many interesting analysis frameworks are Mazurkiewicz-invariant, or Mazurkiewicz-invariant under natural conditions. Let us look at the examples from Section 2.1.

The input/output framework is Mazurkiewicz-invariant if [[ 1 ]]([[ 2 ]]({v})) = [[ 2 ]]([[ 1 ]]({v}))
holds whenever 1 and 2 are independent. This is not always the case, but holds e.g. when all variables of V are local variables. Formally, the set V of variables is partitioned into sets V p of local variables for each process p. Further, [[ ]] involves only the local variables of the processes involved in : Letting (v , v) denote a valuation of V , split into a valuation v of the variables of the processes of and a valuation v of the rest, we have

[[ ]](v , v) = (v , v), and [[ ]](v , v) = [[ ]](v , v ) for every v , v, v .
The anti-pattern framework is not Mazurkiewiczinvariant. For example if we take some

∈ K independent of 1 then [[ 1 2 ]] = [[ 1 2 ]].
However, in Section 5 we will show that there is a Mazurkiewicz-invariant framework for anti-patterns.

The minimal/maximal expected cost framework is Mazurkiewicz-invariant. Indeed, it satisfies

[[ 1 ]] • [[ 2 ]] = [[ 2 ]] • [[ 1 ]
] for all outcomes 1 , 2 , independent or not. Further, by Theorem 1 the expected cost is the same for every scheduler, and so the result of the analysis is the expected cost of the negotiation diagram.

The best/worse case execution framework is Mazurkiewicz-invariant. Intuitively, the scheduler introduces an artificial linearization of the nodes, which are however being executed in parallel. As in the previous case, the result of the analysis is the best-case/worst-case execution time of the negotiation diagram (if the negotiation diagram is cyclic and the cycle non-zero time, then the worst-case execution time is infinite).

Our next goal is a generic algorithm for computing the MOP of Mazurkiewicz-invariant frameworks for sound deterministic negotiation diagrams. This will be done in Section 4, but before we will need some results on decomposing negotiation diagrams.

Decomposing Sound Negotiation Diagrams

We associate with every node n and every location of a sound deterministic negotiation diagram N a "subnegotiation" N | n and N | , and prove that it is also sound. In Section 4 we use these subnegotiations to define an analysis algorithm for sound deterministic negotiation diagrams. We illustrate the results of this section on the example of Figure 2. Intuitively, N | n contains the nodes n such that dom(n ) ⊆ dom(n), with transitions inherited from N , and n as initial node. The non-trivial part is to define the final node and show that N | n is sound. Given a location = (n, a), the negotiation N | contains the part of N | n reachable by executions that start with and afterwards only use nodes with domains strictly included in dom(n). Figure 3 shows some of the subnegotiations we will obtain for some nodes and locations of Figure 2. The rest of the section first presents a theorem showing the existence and uniqueness of some special configurations (Section 3.1), and then uses it to define N | n and N | , and prove their soundness (Section 3.2).

Unique maximal configurations

Given a node n of a sound and deterministic negotiation, we prove the existence of a unique reachable configuration I(n) enabling n and only n. Then we show the following: if we start from I(n) as initial configuration, "freeze" the processes of Proc \ dom(n), and let the processes of dom(n) execute maximally (i.e., until they cannot execute any node without the help of processes of Proc \ dom(n)), then we always reach the same "final" configuration F (n). Additionally, given a location = (n, a) we show: If from I(n) we execute and let the processes of dom(n) proceed until no enabled node m satisfies dom(m) ⊂ dom(n), then again we always reach the same "final" configuration F ( ).

Let X ⊆ Proc be a set of processes. A sequence of locations 1 , . . . , k is an X-sequence if the domains of all i are included in X; it is a strict X-sequence if moreover the domains of all i , but possibly 1 , are strictly included in X. We write (strict) n-sequence for (strict) dom(n)-sequence.

We write n n if dom(n ) ⊆ dom(n), and n ≺ n if dom(n ) dom(n) (and similarly for , ≺ , n etc). Our goal is to prove: Theorem 2. Let m be a reachable node of a sound deterministic negotiation diagram N .

(i) There is a unique reachable configuration I(m) of N that enables m, and no other node. (ii) There is a unique configuration F (m) such that -F (m) is reachable from I(m) by means of an m-sequence, and for every node n enabled at F (m), dom(n)

is not included in dom(m).

(iii) For every location of m there is a unique configuration F ( ) such that -F ( ) is reachable from I(m) by means of a strict m-sequence starting with , and for every node n enabled at F ( ), dom(n) is not strictly included in dom(m).

E.g., in Figure 2 we have I(n 1 ) = (n 1 , n 8 , n 8 ) (an abbreviation for I(n 1 )(p 1 ) = {n 1 }, I(n 1 )(p 2 ) = {n 8 }, I(n 1 )(p 3 ) = {n 8 }); I(n 2 ) = (n 8 , n 2 , n 2 ); and I(n 3 ) = (n 8 , n 3 , n 7 ). Moreover, F (n 1 ) = F (n 2 ) = (n 8 , n 8 , n 8 ); and F (n 3 ) = (n 8 , n 7 , n 7 ). Further, we get F (n 7 , a) = (n 8 , n 7 , n 7 ) and

F (n 7 , b) = (n 8 , n 2 , n 2 ).
The proof of Theorem 2 is quite involved. The theorem is a consequence of the Unique Configuration lemma (Lemma 4 below), which relies on the Domination lemma (Lemma 3 below), which in turn is based on results of [START_REF] Esparza | On negotiation as concurrency primitive II: Deterministic cyclic negotiations[END_REF], [START_REF] Esparza | Soundness in negotiations[END_REF].

A local path of a negotiation diagram N is a path

n 0 p0,a0 ---→ n 1 p1,a1 ---→ . . . p k-1 ,a k-1 -------→ n k in the graph of N . A local path is a local circuit if k > 0 and n 0 = n k . A local
path is reachable if some node in the path is reachable. The domination lemma says that every local circuit has some node containing all processes of the circuit. The unique configuration lemma says that if two enabled configurations agree on a set of processes X and every enabled action in one of the two configurations needs a process from X, then the two configurations are actually the same. Lemma 4. (Unique Configuration Lemma) Let X ⊆ Proc be a set of processes. Let C 1 , C 2 be reachable configurations such that (1) C 1 (p) = C 2 (p) for every p ∈ X, and (2) every node n enabled at

C 1 or C 2 satisfies dom(n)∩X = ∅. Then C 1 = C 2 .
The above lemma gives Theorem 2 rather directly. For (i), take X = dom(m). Suppose that there are two configurations I 1 and I 2 as in (i). The hypotheses of Lemma 4 are satisfied, and so I 1 = I 2 . The case (ii) is equally easy, while (iii) is only a bit more involved.

Subnegotiations for nodes and locations

We use Theorem 2 to define the subnegotiations N | n and N | for each node n and location of a sound deterministic negotiation diagram N , and prove that they are sound. Definition 3. Let N be a sound deterministic negotiation diagram and let n be a reachable node of N . The negotiation diagram N | n contains all the nodes and locations that appear in the n-sequences u such that

I(n) u -→ F (n), plus a new final node n| fin n with dom(n| fin n ) = dom(n).
The initial node is n, and the transition function δ| n is defined as follows. For given m, a, p, we set:

δ| n (m, a, p) = δ(m, a, p) if δ(m, a, p) = F (n)(p) n| fin n if δ(m, a, p) = F (n)(p)
An example of N | n is given on the left of Figure 3.

Lemma 5. If N is a sound deterministic negotiation dia- gram then so is N | n .
The subnegotiation N | induced by a location = (n, a) is defined analogously to N | n , with two differences. First, in N | the node n has a as the unique outcome. Second, the domain of every node of N | , except the node n itself, is strictly included in dom(n).

Computing the MOP

We use the decomposition of Section 3 to define an algorithm computing the MOP for Mazurkiewicz-invariant frameworks and arbitrary sound deterministic negotiation diagram. The idea is to repeatedly reduce parts of the negotiation diagram without changing the meaning of the whole negotiation. When reduction will be no longer possible, the negotiation diagram will have only one location, whose value will be the value of the negotiation. The goal of this section is to present Algorithm 1 and Theorem 3 that is our main result.

As we have seen in the previous section, for every node n, the negotiation diagram N | n is sound and the final configuration F (n) is unique. Thus we can safely replace all the transitions from n by one transition going directly to F (n) and assign to this transition the value of N | n . This requires to be able to compute F (n) as well as the value of N | n . For this we proceed by induction on the domain of n starting from nodes with the smallest domain. As we will see, this will require us to compute MOP only for negotiations of two (very) special forms One-trace negotiations. These are acyclic negotiation diagrams in which every node has one single outcome. In this degenerate case, all the executions of the negotiation diagram are Mazurkiewicz equivalent; moreover, by acyclicity, the trace contains every location at most once. Since the analysis framework is Mazurkiewicz-invariant, we have

[[N ]] = [[w]]
for any successful run w. A successful run can be computed by just executing the negotiation diagram with some arbitrary scheduler. Once a successful run w is computed, we extract from it a flow-graph with |w| nodes, that is actually a sequence, and compute MFP.

Replications. Intuitively, a replication is a negotiation diagram in which all processes are involved in every node, and all processes move uniformly, that is, after they agree on an outcome they all move to the same node. Formally, a negotiation diagram is a replication if for every reachable node n and every outcome (n, a) there is a node m such that δ(n, a, p) = m for every process p. Observe that, in particular, all nodes of a replication have the same domain. It follows that (the reachable part of) a replication is a flowgraph "in disguise". More precisely, we can assign to it a flow-graph having one node for every reachable node, and an edge for every location (n, a), leading from n to δ(n, a, p), where p can be chosen arbitrarily out of dom(n). It follows immediately that the MOP for the negotiation diagram is equal to the MFP of this flow-graph. Definition 5. A node n is reduced if it has one single outcome, and for this single outcome a we have δ(n, a, p) = F (n)(p) for every p ∈ dom(n).

A location = (n, a) is reduced if δ(n, a, p) = F ( )(p) for every p ∈ dom(n). Now we will define an operation of reducing nodes and locations in a negotiation diagram; this is the core operation for every node n such that dom(n) = X do

10: ## N | n is a replication ## 11: [[n, a n ]] = MOP (N | n ) 12:
end for 13:

for every node n such that dom(n) = X do 14: The negotiation diagram Red n (N ) is defined similarly but now:

N := Red n (N )
• out(n) := {a n }; • δ(n, a n , p) := F (n)(p) for every process p ∈ dom(n).
The next lemma states that these reduction operations preserve the meaning of a negotiation diagram. This argument works if indeed we can compute M OP (N | ) and M OP (N | n ) in lines 6 and 11 of the algorithm, respectively. For this it is enough to show that the invariants immediately preceding these lines hold, as this would mean that we deal with special cases we have discussed at the beginning of this section. The following lemma implies that the invariants indeed hold. Assume that all locations have cost 1, and that the probability of a location = (n, a) is 1/|out(n)| (so, for example, the locations (n 3 , a) and (n 3 , b) have probability 1/2, while (n 0 , a) has probability 1). We compute the expected cost of the diagram using Algorithm 1.

The minimal non-reduced nodes w.r.t. are n 3 , n 4 , n 5 , n 6 . All their locations satisfy this we can easily do because N | (n2,a) is a one-trace negotiation; we just pick any successful run, for example (n 2 , a)(n 3 , a n3 )(n 4 , a n4 ), and add the costs. After reducing N | (n2,a) we obtain the negotiation diagram in the middle of Figure 4; the non-reachable nodes n 3 , . . . , n 6 are no longer displayed, and all locations have cost 1 but (n 2 , a (n2,a) ), which has cost 7. Further, all locations of n 2 and n 7 satisfy

[[N | ]] = [[ ]].
We compute N | n2 and N | n7 by a fixed point calculation analogous to the one above (observe that both of them are replications), and after reduction obtain the negotiation diagram at the bottom of the figure, with [[n 7 , a n7 ]] = (1, 9) and [[n 2 , a n2 ]] = (1, 7 + 9) = [START_REF] Bouajjani | Analysis of recursively parallel programs[END_REF][START_REF] Farzan | Causal dataflow analysis for concurrent programs[END_REF]. Now, the minimal non-reduced node is n 0 .We compute MOP (N | (n0,a) ) (N | (n0,a) is a one-trace negotiation), and obtain [[n 0 , a]] = (1, 1 + 1 + 16) = [START_REF] Bouajjani | Analysis of recursively parallel programs[END_REF][START_REF] Favre | Diagnostic information for control-flow analysis of workflow graphs (a.k.a. free-choice workflow nets)[END_REF], which is the final result. Finally, to estimate the complexity of the algorithm, we should also examine how to calculate Red (N ) and Red n (N ) in lines 7 and 14 of the algorithm. In order to calculate Red (N ) we need to know F ( ). The invariant says that N | at that point has one trace. So it is enough to execute this trace in N | to reach F ( ). Similarly, for Red n (N ) we need to know F (n). The invariant says that N n is a replication, so it is just a flow graph with one final node n fin . We can execute in N any path leading to the exit to calculate F (n). To sum up, the calculations of Red (N ) and Red n (N ) in lines 7 and 14 can be done in linear time with respect to the size of N .

We summarize the results of this section:

Anti-Patterns and Gen/Kill Analyses

We saw in Section 2.1 that the problem of detecting an anti-pattern can be naturally captured as an analysis framework, which however is not Mazurkiewicz-invariant. We now show that, while the natural framework is not Mazurkiewicz invariant, an equivalent framework that returns the same result is. Then we sketch how this result generalizes to arbitrary Gen/Kill analysis frameworks, a much studied class [START_REF] Ganty | Algorithmic verification of asynchronous programs[END_REF].

We need some basic notions of Mazurkiewicz trace theory [START_REF] Diekert | The Book of Traces[END_REF]. Given a sequence w = w 1 • • • w n ∈ L , define i j for two positions i, j of w if i ≤ j and w i is not independent from w j (see Definition 1). Further, define is the transitive closure of the relation . It is well-known that if w ≡ v, i.e., if w, v are Mazurkiewicz equivalent, then w and v are isomorphic as labeled partial orders (the labels being the locations). We write btw (i, j) for the set of positions between i and j, i.e., {k : i k j}.

Recall that anti-pattern analysis asked if there is an execution with the property "w ∈ L" for the language L = L * 1 (K) * 2 L * . Instead of this property consider the following property of w:

(*) there are two positions i, j such that w i = 1 , w j = 2 , btw (i, j) ∩ K = ∅, and not j i. The special case of this condition is when btw (i, j) = ∅; then, since not j i, we actually know that the two positions i, j are concurrent, so w is Mazurkiewicz equivalent to u 1 2 v, for some u, v. Lemma 9. A negotiation diagram N has a successful run w ∈ L iff it has a successful run v with property (*).

It remains to set a static analysis framework for tracking property (*). Since this is a property of Mazurkiewicz traces, the framework is Mazurkiewicz-invariant.

We need one more piece of notation. For a word w and a process p we write btw ( 1 , p) for the set btw (i, j) where i is the last occurrence of 1 , and j is the last occurrence of a location using process p.

We define now an auxiliary function α from sequences to P(Proc) 2 ∪ { }. We set α(w) = if w has property (*), otherwise α(w) = (P A , P B ) where

• p ∈ P A if btw ( 1 , p) = ∅ and btw ( 1 , p) ∩ K = ∅, • p ∈ P B if btw ( 1 , p) = ∅ and btw ( 1 , p) ∩ K = ∅.
We describe a PTIME computable function F such that for every sequence w and location :

α(w ) = F (α(w), )
For defining F we first describe the update of btw ( 1 , p) when extending w by . Let us detail the more interesting case where = 1 . Observe that the set of positions btw ( 1 , p) does not change if p / ∈ dom( ). If p ∈ dom( ) then the update of btw ( 1 , p) is the union of btw ( 1 , q) over all q ∈ dom( ), plus . According to these observations, we define the update of F in the case = 1 as follows. If p / ∈ dom( ) then process p remains in its set, P A or P B . If p ∈ dom( ), then: p goes into the set P B if either there was some q ∈ dom( ) in P B , or ∈ K and there is some q ∈ dom( ) in P A ; p goes into the set P A if / ∈ K, no q ∈ dom( ) is in P B and there is at least one q ∈ dom( ) in P A .

The function F can be extended to a monotonic and distributive function F on P(Proc) 3 ∪ { } ordered componentwise, by turning α(w) into a partition of Proc (adding a component P C = Proc \ (P A ∪ P B )) and embedding it into a suitable function over P(Proc) 3 ∪ { }.

With the help of the function F we define now the value of each location:

* : [[w]](∅, ∅, Proc) = iff w ∈ L. Moreover, [[N ]](∅, ∅, Proc) =
iff N has a successful execution in L.

Generalization to Gen/Kill analyses

We consider general Gen/Kill analyses 8 . We are given a set of locations G ⊆ L that generate something, and a set of locations K ⊆ L (not necessarily disjoint with G) that kill this something. The lattice D has just two elements {0, 1}, with ∧ and ∨ as lattice operations, and the transformer of a program instruction is of the form

[[ ]](v) = (v ∧ ( ∈ ∨ ( ∈ G).
Classical examples from the static analysis of programs are the computation of reaching definitions, available expressions, live variables, very busy expressions, where the "something" are values assigned to a variable or an expression [START_REF] Katoen | GSPNs revisited: Simple semantics and new analysis algorithms[END_REF]. The four main classes of Gen/Kill analyses differ only on whether control-flow is interpreted forward or backwards, and on whether we do "merge over all paths" or "meet over all paths". Observe that in backward properties we require that a configuration C is reachable from the initial configuration. For forward properties we do not need to assume that a configuration is co-reachable from the final configuration, as this will be immediately implied by soundness.

The two existential properties above can be expressed in terms of the existence of successful executions of a particular form: executions C init w -→ C fin with w belonging to some language. The same is true for the negation of the universal properties. Consider the languages given by regular expressions: The resource analysis at the beginning of this section corresponds to E 3 . For each one of E 1 , E 2 , E 4 it is easy to produce an analogue of Lemma 9 reformulating the property in trace terms. This allows us to check all properties in polynomial time using our algorithm for Mazurkiewicz invariant analysis frameworks.

1) E 1 = L * G(K) * L * , 2) E 2 = (K ∩ G) * L * ∪ L * (K ∩ G)(K ∩ G) * L * , 3) E 3 = L * (K) * G L * , 4) E 4 = L * (K ∩ G) * ∪ L * (K ∩ G) * (K ∩ G) L * . Lemma 12.

Conclusions

Previous work had identified deterministic negotiations -a model of concurrency essentially isomorphic to freechoice workflow Petri nets -as a class that has both practical relevance for business process modeling, and admits PTIME analysis for several important properties once negotiations are assumed to be sound. Moreover soundness is a natural prerequisite that can be checked in PTIME.

We have proposed a general notion of Mazurkiewiczinvariant analysis frameworks. We have shown that computing the MOP in such frameworks for sound deterministic negotiations is as easy as computing it for sequential flow graphs (while computing the MOP of general frameworks takes exponentially longer, unless PTIME=NP). This result not only subsumes all previous PTIME results on analysis of sound deterministic negotiations, but also yields PTIME algorithms for new problems, like the computation of the best-case/worst-case execution time, the detection of antipatterns, and general gen/kill analysis problems. The result is particularly interesting for gen/kill problems: While their natural formulation is not in terms of Mazurkiewiczinvariant frameworks, we have shown that they can be reformulated as such.

In future work we plan to improve the degree of the polynomial bounding the runtime of our algorithm. Since our decomposition does not partition a negotiation into disjoint parts, when computing MOPs of subnegotiations we are redoing computations. Bounding the size of overlaps looks like a promising way of bringing the complexity on a par with the sequential case. Section 5 on gen/kill analyses raises a further question. In the sequential case, a gen/kill analysis can be simultaneously computed for all program points and all program variables (for example, one can compute for each program point the set of live variables at that point). This is not yet the case in our algorithm. In fact, it is not clear what is a program point in a negotiation: If one takes a configuration as a program point, then, since the number of reachable configurations can grow exponentially in the size of the negotiation diagram, any algorithm that explicitly computes the MOP for each reachable configuration has exponential worst-case complexity.

Figure 1 .

 1 Figure 1. A negotiation diagram with two processes.

6

 6 Several interesting analyses are instances of our framework. 2.1.1. Input/output semantics. Let V be a set of variables and Z the set of values. A valuation is a function V → Z, and Val denotes the set of all valuations. An element of D is a set T ⊆ Val . The join and meet lattice operations are set union and intersection. For each location = (n, a), the function [[ ]] describes for each input valuation v ∈ Val the set of output valuations [[ ]]({v}) that are possible if n ends with result a. For any set T of valuations the function is defined by [

  (a) The number of schedulers is infinite, and nonmemoryless schedulers may generate an infinite reachability graph; so we do not obtain an algorithm for computing [[N ]]. (b) Even for memoryless schedulers, the size of the reachability graph may grow exponentially in the size of the negotiation diagram. So the algorithm for computing [[N , S]] needs exponential time, also for lattices with only two elements.

  3 we solve problem (a): We show that [[N ]] = [[N , S]] for every scheduler S (Theorem 1 below), and so that it suffices to compute [[N , S]] for a scheduler S of our choice. In the rest of the paper we solve problem (b): We give a procedure that computes [[N ]] without ever constructing the reachability graph of the negotiation diagram. The procedure reduces the problem of computing the MOP to computing the MFP of a polynomial number of (sequential) flow-graphs, each of them of size at most linear in the size of the negotiation diagram. This shows that the MOP can be computed in polynomial time for a sound deterministic negotiation diagram iff it can be computed in polynomial time for a sequential flow-graph.

Theorem 1 .

 1 Let N be a negotiation diagram, and let [[ ]] be an analysis framework for N . If N is deterministic and [[ ]] is Mazurkiewicz-invariant, then [[N , S]] = [[N , S ]] for every two schedulers S, S , and so [[N ]] = [[N , S]] for every scheduler S.

Figure 2 .

 2 Figure 2. A negotiation diagram with three processes.

Figure 3 .

 3 Figure 3. Subnegotiations N |n 3 (top left), N | (n 3 ,a) (bottom left), and N | (n 2 ,a) (right) of the negotiation diagram of Figure 2. Nodes unreachable from the initial node are not shown.

Lemma 3 .

 3 (Domination Lemma) Let N be a deterministic sound negotiation diagram. Every reachable local circuit of N contains a dominant node, i.e. a node n such that m n, for every node m of the circuit.

Definition 4 .

 4 Figure 3 shows (on the right) N | for the location = (n 2 , a) of the negotiation diagram of Figure 2. Lemma 6. If N is a sound deterministic negotiation diagram, then so is N | .

Algorithm 1 4 :

 14 Algorithm computing MOP for a sound deterministic negotiation diagram N . 1: while N has non-reduced nodes do 2: m := ≺-minimal, non-reduced node 3: X = dom(m) for every = (n, a) with dom(n) = X do 5: ## N | is a one-trace negotiation ## 6: [[n, a ]] := MOP (N | )

  end while 17: return [[ ]], where is the unique outcome of the initial node of N of Algorithm 1. For a location = (n, a), the operation Red (N ) removes the transition of n on and adds a new transition on (n, a ). Similarly Red n (N ), but this time it removes all transitions from n and adds a single new transition on (n, a n ). Definition 6. Let N = Proc, N, dom, R, δ be a sound deterministic negotiation diagram and let = (n, a) be a non-reduced outcome of N . The negotiation diagram Red (N ) has the same components as N but for out and δ that are subject to the following changes: • out(n) := (out(n) \ {a}) ∪ {a }; • δ(n, a , p) := F ( )(p) for every process p ∈ dom(n).

Lemma 7 .

 7 Let N and = (n, a) be as in Definition 6. Assign to the new location = (n, a ) the mapping[[ ]] := [[N | ]]. Then [[N ]] = [[Red (N )]]. Analogously, [[N ]] = [[Red n (N )]] when we assign [[(n, a n )]] = [[N | n ]].At this point we can examine Algorithm 1. The algorithm repeatedly applies reduction operations to a given negotiation diagram. Thanks to Lemma 7 these reductions preserve the meaning of the negotiation diagram. At every reduction, the number of reachable locations in the negotiation diagram decreases. So the algorithm stops, and when it stops the negotiation diagram has only one reachable location. The abstract semantics of this location is equal to the abstract semantics of the original negotiation diagram.

Lemma 8 .

 8 Let N be a sound deterministic negotiation diagram, and n a node such that all nodes m ≺ n are reduced in N . (1) if a is an outcome of n, then for = (n, a) the negotiation diagram N | is a one-trace negotiation. (2) if all locations n are reduced, then N | n is a replication. Example: Consider the negotiation diagram of Figure 2.

  [[N | ]] = [[ ]]. The algorithm computes MOP (N | ni ) for i = 3, 4, 5, 6. The subnegotiations N | n3 and N | n5 are shown in Figure 3; the other two are similar. MOP (N | n3 ) is the expected cost of reaching n f in from n 3 in N | n3 . Since N | n3 is a replication (in fact, it is even a flow-graph), we can compute it as the least solution of the following fixed point equation, where we abbreviate Prob( ) to P ( ) and Cost( ) to C( ): (p, c) = p • P (n 3 , b) • P (n 5 , a) + P (n 3 , a), P (n 3 , b) • P (n 5 , a) • (C(n 3 , b) + C(n 5 , a) + c)+ P (n 3 , a) • C(n 3 , a) point (1, 3), which of course can be computed by just solving the linear equation. So MOP (N| n3 ) = (1, 3). We obtain [[n 3 , a n3 ]] = [[n 4 , a n4 ]] = 3, [[n 5 , a n5 ]] = [[n 6 , a n6 ]] = 4,and the reduced negotiation diagram at the top of Figure 4. Observe that nodes n 5 and n 6 are no longer reachable. The minimal non-reduced nodes are now n 2 and n 7 . The locations of n 7 satisfy [[N | ]] = [[ ]]. For the location (n 2 , a) we obtain MOP (N | (n2,a) ) = (1, 1 + 3 + 3) = (1, 7);

2 Figure 4 .

 24 Figure 4. Three reduced negotiation diagrams constructed by Algorithm 1 started on the negotiation diagram of Figure 2.

  [[ ]](P A , P B , P C ) = F ((P A , P B , P C ), )Observe that this gives us [[w]] = α(w) for every sequence w. The above discussion yields two lemmas showing that [[ ]] is a Mazurkiewicz invariant analysis framework that can be computed in PTIME, since F can be computed in PTIME.Lemma 10. [[•]] is Mazurkiewicz-invariant.Lemma 11. Consider a negotiation diagram N over set of locations L. For every sequence w ∈ L

•

  may/forward. For some configuration C there is an execution C init w -→ C with w ∈ L * G(K) * . • must/forward. For every configuration C and every execution C init w -→ C, if w ends with then w ∈ L * G(K) * . • may/backward. For some reachable configuration C there is an execution C w -→ C fin with w ∈ (K) * GL * . 8. Although not in bitvector form, which we leave for future work (see the conclusions).

•

  must/backward. For every reachable configuration C and every execution C w -→ C fin , if w starts with then w ∈ (K) * GL * .

  For a sound negotiation diagram we have the following:• may/forward is equivalent to ∃C init w -→ C fin with w ∈ E 1 . • negation of must/forward is equivalent to ∃C init w -→ C fin with w ∈ E 2 . • may/backward is equivalent to ∃C init w -→ C fin with w ∈ E 3 . • negation of must/backward is equivalent to ∃C init w -→ C fin with w ∈ E 4 .

  of[START_REF] Esparza | Reduction rules for colored workflow nets[END_REF] for a workflow Petri net model). The diagram describes a workflow for handling insurance claims by an insurance company with two departments D 1 and D 2 . The processes of the negotiation are D 1 and D 2 . The nodes n 0 , n 4 , n 7 have domain {D 1 , D 2 }; n 1 and n 3 have domain D 1 , and n 2 , n 5 , n 6 have domain D 2 . After the claim is registered, outcome reg involves both processes, D 1 sends a questionnaire to the client, and concurrently D 2 makes a first evaluation of the claim. After the client's answer is received or a time-out occurs (outcome tout), both departments decide together at node n 4 whether to process the claim or not. In both cases D 1 has nothing further to do, and moves to the final node n 7 . If the decision is to process the claim, then D 2 moves to n 5 , and the claim is processed, possibly several times, until a satisfactory result is achieved (outcome OK), after which D 2 also moves to n 7 .A configuration of a negotiation diagram is a function C : Proc → P(N ) mapping each process p to the set of nodes in which p is ready to engage. A node n is enabled in a configuration C if n ∈ C(p) for every p ∈ dom(n), that is, if all processes that participate in n are ready to proceed with it. A configuration is a deadlock if it has no enabled node. If node n is enabled in C, and a is an outcome of n, then we say that location (n, a) can be executed, and its execution produces a new configuration C given by C (p) = δ(n, a, p) for p ∈ dom(n) and C (p) = C(p) for p ∈ dom(n). We denote this by C

	(n,a)

  Theorem 3. Let N be a sound deterministic negotiation diagram, and [[ ]] a Mazurkiewicz invariant analysis framework. Algorithm 1 stops and outputs [[N ]]. The complexity of the algorithm is O(|N |(C + |N |)) where |N | is the size of N , and C is the cost of [[ ]] analysis for flow-graphs of size |N |.

In some papers the roles of nodes and edges are reversed: Nodes are program instructions, and edges are program points. The version with program points as nodes is more convenient for our purposes.

R stands for result; we prefer to avoid the confusing symbol O.

Acknowledgments. We thank the anonymous reviewers for useful remarks, and Jörg Desel, Philipp Hoffmann, and Denis Kuperberg for helpful discussions.

Partially supported by the DFG Project Negotiations: A Model for Tractable Concurrency, and the Institute of Advance Studies of the Technische Universität München.