L Simonot

M Hébert

R D Hersch

Assessing the proper color of translucent materials by an extended two-flux model from measurements based on an integrating sphere

The optical and visual characterization of translucent materials according to their shape and thickness is still a challenge for scientific research due to the difficulty to describe and predict in a simple manner the angular and spectral distributions of the reflected and transmitted light. In this paper, the light reflection and transmission properties of slightly scattering polymer sheets stacked with each other are studied. The light that is regularly reflected and transmitted by the material, propagated without scattering, as well as the light which is scattered out of the regular directions, are predicted using only a few measurements from a commercial reflectance/transmittance spectrophotometer and an extended twoflux model of the radiative transfer. The proposed methodology, validated by experiments, can be applied by laboratories equipped with an integrating sphere device which is usually used in the context of strongly diffusing rather than translucent materials. A discussion states the potential and the limitations of the proposed methodology.

Introduction

The color prediction of layered absorbing materials such as those produced by 3D printers is enabled by spectral flux transfer models, among which the widely used two-flux models. However, it is known that the two-flux theory is valid for either nonscattering or strongly scattering media, but not for intermediate levels of scattering. The present contribution aims at extending the classical two-flux model in order to predict the spectral properties, therefore the color, of stacked translucent layers by performing measurements on individual layers with a commercially available integrating sphere reflectance-transmittance spectrophotometer for a better convenience in practical applications.

The optical description of a translucent object is made difficult by the scattering of light occurring in the material itself, and possibly at its interfaces with air. A full characterization requires measuring the angular reflectance and transmittance over the sphere, by distinguishing whenever possible the regularly reflected/transmitted fluxes and the diffuse fluxes. The translucent materials can be classified at the center of the range between non-scattering and strongly scattering materials that are easy to characterize optically.

A) Nonscattering materials with flat interfaces

The propagation of collimated light within a stack of these materials is described by using Beer-Lambert-Bouguer's law for the transmittance within the medium, and Snell laws and Fresnel formulae for the reflectance and transmittance at the interfaces. The material is characterized by its absorption coefficient and its refractive index. A two-flux model, such as the one proposed by Stokes predicting reflectances and transmittances of piles of glass plates. [START_REF] Stokes | On the intensity of the light reflected from or transmitted through a pile of plates[END_REF], models the multiple reflections of light by the interfaces in the regular directions.

B) Strongly scattering materials

The propagation of a diffuse (Lambertian) light within strongly scattering materials, characterized by their absorption and backscattering coefficients, can also be modeled by a two-flux model such as the one proposed by Kubelka and Munk [START_REF] Kubelka | Ein Beitrag zur Optik der Farbanstriche[END_REF], or by Kubelka [START_REF] Kubelka | New contributions to the optics of intensely lightscattering material, part I[END_REF][START_REF] Kubelka | New contributions to the optics of intensely lightscattering material, part II. Non-homogeneous layers[END_REF] in the case of stacked layers.

In the case of translucent materials, the angular distribution of light follows a more complex function and varies as the light propagates through the materials. Light scattering in each point is described by a so-called phase function, incorporated into a multiple scattering model based for example on a resolution of the radiative transfer equation [START_REF] Chandrasekhar | Radiative transfert[END_REF][START_REF] Mudgett | Multiple scattering calculations for technology[END_REF]. The four-flux method [START_REF] Mudgett | Multiple scattering calculations for technology[END_REF][START_REF] Beasley | Scattering and absorption in turbid media[END_REF][START_REF] Ishimaru | Wave Propagation and Scattering in Random Media[END_REF][START_REF] Maheu | Four-flux models to solve the scattering transfer equation in terms of Lorenz-Mie parameters[END_REF][START_REF] Maheu | Four-flux models to solve the scattering transfer equation. Special cases[END_REF][START_REF] Simonot | Multilayer fourflux matrix model accounting for directional-diffuse light transfers[END_REF] is an interesting compromise to solve this equation. It consists in simplifying the light propagation problem by considering four global light components: two components diffused over the upper and lower hemispheres, and two components propagating in the regular reflection and transmission directions in respect to the incidence direction. The proper color of the material is perceived from the diffuse component reflected (respectively transmitted) in the upper (respectively lower) hemisphere. The sensation of gloss (respectively transparency) is perceived from the regularly reflected (respectively transmitted) light component.

In terms of measurement systems, a full optical characterization of a translucent material requires bi-directional measurements over the sphere of the reflectance and transmittance of a slice of material, by using a gonio-spectrophotometer. However, this kind of instrument is expensive and not always available in the industry where one of the main issues is the characterization of the intrinsic color of materials. More classical measurement configurations, recommended by the CIE [START_REF]CIE, Colorimetry[END_REF] for color measurements of diffusing materials in reflectance mode, are the 45°:0° and 0°:45° geometries where the specimen is illuminated at the first angle and viewed at the second. However, these geometries do not allow relevant color measurement for non-scattering or weakly scattering materials. Only geometries using an integrating sphere allow measuring the regular and diffuse, reflected and transmitted light components. Most sphere based instruments provide the corresponding measurement geometries. However, these configurations require more than a single integrated sphere in order to apply the four-flux method. We present in this paper an extended two-flux model (or a degraded four-flux model) which considers the propagation of both diffuse and collimated light fluxes in the material, enables predicting with a rather good accuracy the light components diffused by stacks of translucent layers or sheets, and thereby their intrinsic color. This original method thus overcomes the usual limitations of the two-flux approach by considering intermediate materials between non-scattering and strongly scattering media. The predicted reflectances and transmittances can be directly compared with measurements from an integrating sphere reflectance/transmittance spectrophotometer.

Integrating spheres are spherical cavities coated with a white diffuse coating [START_REF] Ulbricht | Die Bestimmung der mittleren räumlichen Lichtintensität durch nur eine Messung[END_REF], and are used to measure diffuse reflectance or transmittance of materials. They can be used in two configurations: either in order to illuminate the sample with perfectly diffused light, or in order to collect the light emerging from the sample, thus giving an average value over all angles of illumination or observation. In the scope of the Kubelka-Munk theory, an integrating sphere is often used to produce the needed Lambertian irradiance, whereas the exitance of the scattering material, assumed to be Lambertian, is estimated by measuring only the radiance in one direction (assuming that a same radiance would be measured in every other direction). However, these properties are valid for strongly scattering media but not for translucent, slightly scattering media whose exiting flux is not Lambertian. Reflectance or transmittance predictions based on integrating sphere measurements are therefore not well adapted to translucent materials, unless a specific methodology, such as the one that we introduce in this paper, is applied.

We consider an integrating sphere used for illumination. The integrating sphere has often a black trap located in the symmetric direction to the detector in respect to the normal of the sample. When the trap is open, no light can be specularly reflected from the sample toward the detector: it is the specular component excluded mode (SCE). When the trap is closed, the specularly reflected light is included into the measured radiance: it is the specular component included mode (SCI). The specular excluded reflectance measurement requires the use of the gloss trap, for which the CIE [START_REF] Cie | Geometric tolerances for colour measurements[END_REF] recommends selecting at least all rays within 1° of the specular reflection direction. Unfortunately, standardization does not exist to more precisely define the angular width of the specular ports. Their angle may vary somewhat depending on the integrating sphere device. The transmittances can also be measured with a diffuse illumination supplied by an integrating sphere. According to the position of the sample close to either the sphere or the detector, the total, respectively the regular, transmittance is obtained. For the regular transmittance, the CIE recommends that the irradiating and measuring geometry be identical with circular cones having a halfangle of 5° [START_REF] Cie | Geometric tolerances for colour measurements[END_REF].

Using measurements from an integrating sphere, the two-flux model can be successfully applied by considering either the total flux transfers (denoted as SCI) or the Collimated-to-Collimated flux transfers (denoted as CC). In order to characterize only the diffuse color of a material without direct reflection or transmission, specular excluded measurements (denoted as SCE) are preferable. However, in the case of translucent layers, the prediction of SCE reflectances and transmittances is not directly possible by using the two-flux model. We show how the two-flux model should be adapted to allow SCE predictions.

After presenting the experimental device and the notations in Section 2, a solution to simulate SCE transfers derived from the twoflux model is established in Section 3 and discussed in Section 4.

Experimental setup and notations

In our experiments, we used the Color i7 spectrophotometer from X-rite, equipped with a pulse discharge Xenon lamp. Measurements are done from 400 to 750 nm in steps of 10 nm. For a given sample, the instrument equipped with an integrating sphere supports four measurement geometries, shown in Fig. 1: -specular included reflectance (di:8°), denoted as SCI r ; -specular excluded reflectance (de:8°), denoted as SCE r , for which the gloss trap is open; -total transmittance (d:0°), denoted as SCI t , for which the sample is placed on the sphere surface; -collimated-to-collimated regular transmittance (0°:0°), denoted as CC t , for which the sample is placed close to the detector.

From the previous measurements, we can also deduce: -the collimated-to-collimated (specular) reflectance (8°:8°), denoted as CC r :

CC SCI SCE r r r = - ; (1)
-the transmittance with regular transmittance excluded (de:0°), denoted as SCE t :

SCE SCI CC t t t = -. (2)
Although the light capturing sensor is positioned at 8° for reflectance measurements and at 0° for transmittance measurements, we assume hereafter that this small angular shift has no influence. In our experiments, we considered translucent, slightly scattering plastic sheets of red and green color. As shown in Fig. 2, they are placed on top of a white background on which black text is printed in order to put their translucency into evidence.

Figure 2. Presentation of the green and red translucent sheets over a white print paper with "Translucency" printed in black.

The measured spectral reflectances and transmittances SCI r , SCE r , SCI t and CC t are presented in Figure 3a for one green sheet, and in Figure 3b for one red sheet. They are the four input spectra for the prediction model. The aim is to predict the reflection and transmission properties of several stacked sheets. Even though the sheets are in mechanical contact with each other, they are not in optical contact: a thin air layer remains between them, and multiple light reflections occur between the sheets. An optical contact obtained by introducing a liquid between the sheets would considerably modify their reflection and transmission properties, therefore their color, in a similar way as shown in Ref. [START_REF] Hébert | Spectral prediction model for piles of nonscattering sheets[END_REF] for stacks of nonscattering acetate sheets.

Prediction model

A two-flux model considers a parallel planar structure of material and therefore reduces the radiative transfer equation to a problem with one spatial dimension. It can be presented as a special case of the N-flux model [START_REF] Mudgett | Multiple scattering calculations for technology[END_REF] where the radiation field for each position in the stack of sheets is composed of two beams ( )

2 N =
propagating forwards I and backwards J. Each sheet gives rise to flux transfers characterized by a front side reflectance r, a back side reflectance r', a forward transmittance t and a backward transmittance t'.

Fig. 4 represents the flux transfers for a stack of two sheets (labelled 1 and 2) without optical contact between them, in the framework of the two-flux model.

The resulting reflectances and transmittances for the superposition of the two sheets are (cf. Appendix and [START_REF] Kortüm | Reflectance spectroscopy (principles, methods and applications[END_REF]):

2 1 1 1 1 2 1 2 2 2 1 2 1 1 r t t r r r r r t t r r r r ′  = +  ′ -   ′  ′ = +  ′ -  and 1 2 1 2 1 2 1 2 1 1 t t t r r t t t r r  =  ′ -   ′ ′  ′ =  ′ -  . ( 3
)
t CC (λ) r SCI (λ) r SCE (λ) (b) Red Sample J 0 r 1 r 2 t 1 t 2 J 2 J 1 I 0 I 2 I 1 r 1 ′ r 2 ′ t 1 ′ t 2 ′ Sample 1 Front side Back side Sample 2
These relations can be generalized to any multilayer system, e.g. by using a matrix formalism [START_REF] Mazauric | Two-flux transfer matrix model for predicting the reflectance and transmittance of duplex halftone prints[END_REF]. When the sheets are symmetric, i.e. it can be assumed that 1 1 r r ′ = , 1 1 t t ′ = , 2 2 r r ′ = , and 2 2

t t ′ = , relations (3) simplify as:

2 2 1 1 1 2 2 1 2 2 1 2 1 2 1 2 1 1 1 r t r r r r rt r r r r t t t t r r  = +  -    ′ = +  -   ′ = =  -   . ( 4
)
Let us now consider identical symmetric sheets of reflectance 1 r and transmittance 1 t . By increasing the number of stacked sheets, the resulting reflectance increases and reaches a limit value, denoted as r ∞ (cf. Appendix):

2 1 r ∞ = α -α - (5)
with

2 2 1 1 1 1 2 r t r + - α = .
This reflectance expression for an infinitely thick material (homogeneous or stratified) is well known and characteristic of the two-flux model. It is also present in the Kubelka-Munk model [START_REF] Kubelka | Ein Beitrag zur Optik der Farbanstriche[END_REF] where α is usually denoted as a and enables computing the albedo of an infinitely thick layer of the material.

It has been shown in Ref. [START_REF] Hébert | Compositional reflectance and transmittance model for multilayer specimens[END_REF] that the two-flux model, and therefore the compositional relations (3), (4) or [START_REF] Chandrasekhar | Radiative transfert[END_REF], apply in the two specific CC and SCI configurations, for perfectly transparent media and for strongly diffusing media, respectively.

For translucent layers, the spectral predictions are explained hereafter for the CC, SCI and SCE configurations. The plots of Figure 5 present the measured and predicted reflectances and transmittances of stacks of 2 and 3 identical green sheets and 2 and 3 identical red sheets. The predicted reflectances of semi-infinite stacks of these sheets are also compared with the measurements performed on a stack of 36 green sheets, and on a stack of 52 red sheets. These numbers are chosen in order to reach the stack opacity (the red sheets are more transparent than the green one's). The deviations between the measured and predicted spectra are given in Table 1, and assessed by both the root mean square deviation RMSD and the visual metric CIELAB ΔE94, obtained by converting both spectra into CIE-1931 XYZ tristimulus values then into CIELAB color coordinates, using the CIE standard illuminant D65.

CC configuration

In the CC configuration, the incident flux is collimated and only the collimated reflected flux in the specular direction or the collimated transmitted flux in the regular direction is considered. The corresponding reflectances and transmittances are the ones denoted by subscript CC. Relations (4) are written:

 = +  -    ′ = +  -   ′ = =  -   . ( 6
)
Moreover, the relation ( 5) with ( )

2 2 1 1 1 1 / 2 CC CC CC r t r α = +
can be used to compute the CC-reflectance for the infinitely thick stack, CC r ∞ .

The measured and predicted CC-reflectances and CCtransmittances are given in the first column of the Figure 5. The specular reflectances CC r are almost independent of the number of sheets. They are mainly due to the first reflection at the upper interface of the stack. This is the reason why the spectra are quite achromatic with a low value similar to the 4% reflectance at normal incidence of an interface between air and a plastic material with refractive index 1.5 n =

. The very slight coloration in specular reflection is due to multiple reflections within the first sheet and between the sheets. Given the low values of CC r compared with the other measurements, the predictions are correct for the order of magnitude (RMSD) but not satisfactory in terms of color difference (CIELAB ΔE94), see Table 1. This may be explained by the important variability in the surface roughness of the sheets. Moreover, slight measurement errors may be emphasized because the reflectances CC r are not directly measured but deduced from SCI r and SCE r measurements [Eq. ( 1)]. However, a fairly good agreement is observed between measured and predicted spectral CC-transmittances for 2 and 3 sheets. The CC-transmittances are induced by light absorption by the material as well as light scattering by either the material or its interfaces with air. Light scattering has the effect of spreading initially collimated light into a larger solid angle. In the case of two or more sheets, the attenuations due to absorbance and solid angle spreading are multiplicative, especially when the denominator 1 2

1 CC CC r r in Eq. ( 6) is close to 1, i.e. when the single-sheet reflectances are low. This allows understanding why the predictions for CC-transmittances are accurate.

Compared to the specular reflectances, the regular transmittances are more colorful, but decrease rapidly towards zero as the number of sheets increases.¨

SCI configuration

In the SCI configuration, the incident flux is perfectly diffuse and the light capturing sensor is at the sheet normal. This mode provides the SCI-reflectances and -transmittances that we assume to correspond to the total reflected or transmitted fluxes exiting from the sample. The two-flux model also applies. For the specular included transfer factors, denoted by subscript SCI, the relations (4) become: The SCI-reflectance of an infinite stack of sheets, SCI r ∞ , is also given by relation ( 5) with ( )

 = +  -    ′ = +  -   ′ = =  -   . ( 7
)
2 2 1 1 1 1 / 2 SCI SCI SCI r t r α = + - .
The second column of Figure 5 presents the measured and predicted SCI-reflectances and -transmittances of stacks of identical sheets. As the number of sheets in the stack increases, the diffuse reflectance monotonously increases, and the diffuse transmittance monotonously decreases. The prediction accuracy, presented in Table 1 (central columns), is fairly good except in the case of an infinitely thick stack for which we denote a sensible deviation in the spectral domain where the stack is the more reflecting. Remind that the reflectance of the infinitely thick stack of sheets, SCI r ∞ , is predicted from the measured reflectance 1 SCI r and transmittance

1 SCI t of one sheet. A slight error in the spectral measurements may induce a significant deviation in the predicted reflectance SCI r ∞ . We often observe that the prediction accuracy for SCI r ∞ is improved by using the measured reflectance and transmittance of k = 2 or more stacked sheets and the following equation (cf. Eq. ( 14) of the Appendix)

2 1 k k k t r r r r r ∞ ∞ ∞ = + - . ( 7
)
In contrast with the CC-transfer factors, SCI-reflectances are not negligible and SCI-transmittances of two or more samples [Eqs. [START_REF] Beasley | Scattering and absorption in turbid media[END_REF]] cannot be reduced to a multiplicative law. The good predictions given by Table 1 require taking into account the multiple reflections between the sheets.

SCE configuration

In the SCE configuration, we consider only the scattered out from the regular directions. In contrast with the CC configuration where only collimated fluxes are considered, and SCI configuration where total fluxes are considered, we experimentally observed that the two-flux model does not apply with the SCE flux transfers. However, thanks to relations (1) and ( 2), the SCE transfers can be deduced from the CC transfers, given by Eqs. ( 6), and the SCI transfers, given by Eqs. [START_REF] Beasley | Scattering and absorption in turbid media[END_REF]. We have:

SCE SCI CC SCE SCI CC SCE SCE SCI CC r r r r r r t t t t = -   ′ ′ ′ = -   ′ = = -  . ( 8
)
Similarly, the infinitely thick SCE-reflectance SCE r ∞ is deduced as:

SCE SCI CC r r r ∞ ∞ ∞ = - . ( 9
)
It is worth noting that the SCE measurements of the individual sheets are not directly required for the prediction of the SCE reflectances and transmittances of a stack [Eqs. ( 8) and ( 9)]. However, to obtain the CC r reflectances [Eq. ( 1)], the SCE r reflectances of the individual sheets are to be measured.

The right column in Figure 5 shows the measured and predicted SCE-reflectances and -transmittances for stacks of identical sheets. The predictions are obtained by first predicting the CC and SCI transfer factors of multiple sheets and then obtaining the SCE transfer factors according to Eqs. ( 8) and ( 9). The predictions are as good as for the SCI configuration (Table 1).

In contrast with CC and SCI measurements, for a given wavelength, the SCE transfers do not always vary monotonously as the number of sheets increases. It is particularly noticeable for the transmittances SCE t in Figure 5. As the two-flux model is a radiative flux balance, it can only predict monotonous variations of the flux transfer factors according to the number of sheets. Due to the observed non-monotonic property, one cannot directly use the SCE measurements to predict with the two-flux model the SCE reflectances and transmittances. However, by first predicting SCI and CC reflectances and transmittances according to Eqs. (6-7), we obtain with Eq. ( 8) valid SCE reflectance and transmittance predictions.

Therefore, the observed non-monotonic property is an indication that the two-flux model cannot directly apply on SCE measurements with this kind of material.

Figure 6 shows the SCE-reflectance and -transmittance of the red translucent plastic sheet on top of the green translucent plastic sheet, and the ones of the green sheet on top of the red sheet. The measured spectra are compared with the spectra predicted by using equations ( 6), ( 7) and ( 8), from the measurements made on one sheet and plotted in Figure 3. As expected, the transmittances are independent of the stacking order, while the resulting reflectance looks reddish or greenish according to whether the red or respectively the green sheet is closer to the observer. Table 2 presents the spectral RMS deviations and the equivalent color deviations (CIELAB ΔE94) between the measured and predicted spectra. It also shows the totally wrong predictions that would be obtained by applying the two-flux model [Eq. ( 4)] directly with the SCE-reflectance and -transmittance of the individual samples. * predictions performed by using directly Eq. ( 4) with the measured SCE spectral reflectances and transmittances of the individual sheets.

Discussion

In this section, we propose to discuss the applicability of the extended two-flux model, in particular in the extreme cases of almost non-scattering and strongly scattering materials. We then address the limitations of the proposed method, firstly due to the use of single-integrating-sphere measurements, secondly due to the difficulty induced by the progressive spreading of a collimated beam.

Special cases

We can verify that the model presented in the previous sections reduces to the same two-flux model in the special cases of nonscattering or strongly scattering materials. In absence of scattering in the material (transparent layers with flat interfaces), either the incident light is collimated and only CC transfers occur [Eqs. [START_REF] Mudgett | Multiple scattering calculations for technology[END_REF] applies], or the incident light is diffuse and total SCI transfers must be considered [Eqs. [START_REF] Beasley | Scattering and absorption in turbid media[END_REF]]. For strongly scattering samples, the same reflectances and transmittances are measured whether the incident light is collimated or diffuse. Therefore, there are no CC transfers, SCI transfers are equivalent to SCE transfers and given by Eqs. [START_REF] Beasley | Scattering and absorption in turbid media[END_REF]. This is however a simplified view. If for example the scattering sheets have flat interfaces, the SCIand SCE-reflectances differ by a small value, almost the same at all wavelengths, corresponding to the Fresnel reflectance of the front sheet surface. In order to take this phenomenon into account, Equations ( 8) can be modified as follows:

1 2 SCE SCI CC SCE SCI CC SCE SCE SI r r r r r r t t t = -   ′ ′ = -   ′ = =  (10)
where the Fresnel reflectance of the front surface, 1 CC r or 2 CC r , depends on the surface roughness [START_REF] Simonot | Color change due to surface state modification[END_REF]. The values for 1 CC r or 2 CC r decrease as the surface roughness increases, and the difference between the SCI and SCE reflectances thus decreases towards zero, the limit case where the light reflected by a sheet having a rough interface can be considered as Lambertian.

Our experiments were carried out with stacks of identical translucent sheets without optical contact, but similar experiments could be performed by stacking translucent layers in optical contact [START_REF] Hébert | Spectral prediction model for piles of nonscattering sheets[END_REF]. The same model applies but with the material considered without its bordering interfaces with air. The optical effect of the bordering interfaces, called Saunderson's correction in the two-flux approach [START_REF] Saunderson | Calculation of the color pigmented plastics[END_REF], depends on the measurement geometry as expressed in [START_REF] Mazauric | Two-flux transfer matrix model for predicting the reflectance and transmittance of duplex halftone prints[END_REF].

Single-integrating-sphere limitation

According to the known limitations of the two-flux theory, we would expect that Eqs. [START_REF] Beasley | Scattering and absorption in turbid media[END_REF] apply for the diffuse-to-diffuse transfers (DD-reflectances and -transmittances, for which the incident light is diffuse, and the outgoing light is captured over the hemisphere), but strictly not for the SCI transfers. Rigorous measurements of the DD transfers would require a double-integrating-sphere [START_REF] Pickering | Two integrating spheres with an intervening scattering sample[END_REF]. Moreover, a double-integrating-sphere would ideally enable three independent measurements, for both reflectance and transmittance: collimatedto-collimated, diffuse-to-diffuse, as well as collimated-to-diffuse configurations. These six independent measurements would allow calibrating a four-flux model, which consists in adding two collimated fluxes to the two diffuse fluxes [START_REF] Mudgett | Multiple scattering calculations for technology[END_REF][START_REF] Beasley | Scattering and absorption in turbid media[END_REF][START_REF] Ishimaru | Wave Propagation and Scattering in Random Media[END_REF][START_REF] Maheu | Four-flux models to solve the scattering transfer equation in terms of Lorenz-Mie parameters[END_REF][START_REF] Maheu | Four-flux models to solve the scattering transfer equation. Special cases[END_REF]. It can be shown [START_REF] Simonot | Multilayer fourflux matrix model accounting for directional-diffuse light transfers[END_REF] that the four-flux model is equivalent to the two-flux model for both CC and DD transfers but not for the collimated-to-diffuse transfers. Unfortunately, double-integrating-sphere measurements are very rarely proposed by current commercial spectrometric devices. With a much more common single-integrating-sphere allowing four independent measurements (Figure 1), the adapted two-flux method presented in this paper seems to be appropriate for predicting the CC, SCI and SCE transmittances and reflectances of superposed slightly diffusing flat sheets.

Progressive "decollimation"

The samples presented in this paper have almost flat interfaces: their surface scattering can be neglected without loss of accuracy. When crossing a sample with flat interfaces, collimated light is either not scattered and stays collimated, or is scattered within the sheets' bulk. A more detailed analysis, based on the samples BRDF's and BTDF's may help understanding in depth how light is scattered and why the predictions are accurate in CC, SCI and SCE modes. With samples presenting rough interfaces, the surface scattering makes a collimated incident light beam spread over a larger solid angle, which grows as the number of encountered interfaces increases. Neither the two-nor the four-flux model can render this angular spreading of the beam, especially if measurements based on the integrating sphere (or even two) are used. It is hard to predict which part of the initially collimated flux can be considered as outside of the specular port of the sphere, therefore as part of the diffuse flux. This is especially difficult because the gloss trap dimensions are not standardized. However, modeling, as simply as possibly (i.e. without use of a complete bidirectional description of light scattering by the sample), this "decollimation" of initially collimated light while crossing a translucent material is an interesting topic for future research.

Conclusion

The aim of this study was to show that the diffuse color of translucent materials can be characterized by a simple extension of a two-flux model and by measurements made with common affordable instruments whose geometry is conceived for strongly scattering media. The proposed extension of the two-flux model to diffuse specular excluded reflectances and transmittances replaces more complex scattering theories and goniospectrophotometers which require much expertise to be used in practical applications. The proposed method relies on measurements performed by using an integrating sphere in specular included and excluded modes. The prediction of the reflectances and transmittances of stacks of samples knowing those of each individual sample can be done by applying the two-flux model for, on one hand, the specularcomponent-included reflectance and the regular-component-included transmittance (SCI transfers), and on the other hand, for the collimated-to-collimated reflectance and transmittance (CC transfers). The specular-component-excluded reflectance and regular-component-excluded transmittance (SCE transfers) can then be deduced by subtracting the SCI and CC transfers, either measured or predicted by the extended two-flux model. This simple method enables distinguishing the color variations according to the material thickness both in the regular directions (CC transfers) and in the rest of the hemisphere (SCE transfers). From the experiments we carried out with slightly scattering polymer sheets, we observed that the simulations are in good agreement with the spectral measurements and allow good predictions of the specular reflected and regular transmitted colors as well as of the reflected and transmitted diffuse colors (in specular excluded mode). This model could be used for innovative printing systems like some 3D printers, for which the color synthesis is based on translucency. This radiometric study also offers new tools for analyzing the color and the perception of translucent samples. J and 1 I can be related according to the following equations:

APPENDIX: The two-flux model

0 1 0 1 1 1 1 0 1 1 J r I t J I t I rJ ′  = +   ′ = +   . (11)
Similar relations can be written for the sample labelled 2 between the fluxes 1 2 , I J and 1 2 , J I :

′  = = +  ′ -   ′ ′ = = +  ′ -    = =  ′ -  ′ ′  ′ = =  ′ -  . ( 13
)
As an alternative to the radiative flux balance, equations (13) can be obtained by writing the multiple reflections between the two samples as a geometric series [START_REF] Kubelka | New contributions to the optics of intensely lightscattering material, part II. Non-homogeneous layers[END_REF].

Let us now consider a semi-infinite stack of identical symmetric slices, e.g. translucent sheets stacked together. Each slice has a reflectance 1 1 r r′ = and transmittance 1 1 t t′ = , independent of the measured side. When many slices are stacked with each other, the stack reflectance reaches an invariant value, denoted as r ∞ , which satisfies the following relation issued from [START_REF] Ulbricht | Die Bestimmung der mittleren räumlichen Lichtintensität durch nur eine Messung[END_REF] by considering that adding one slice does not modifies this reflectance value:

2 1 1 1 1 t r r r r r ∞ ∞ ∞ = + - . (14)
This relation may also be written: Eq. ( 15) has one solution lower than 1, therefore valid for a reflectance:

2 1 r ∞ = α -α -. ( 16
)

Aknowledgement

This work was supported by the French National Research Agency (ANR) in the framework of project PHOTOFLEX n°ANR-12-NANO-0006.

Figure 1 .

 1 Figure 1. Presentation of the four measurement geometries supported by the integrating sphere spectrophotometer.

Figure 3 .

 3 Figure 3. Spectral measurements SCI r , SCE r , SCI t and CC t for a green (a)or a red (b) translucent plastic sheet.In reflectance mode, the sample to be measured is placed in front of a black trap.

Figure 4 .

 4 Figure 4. Two-flux transfers for the superposition of two sheets. Bold arrows represent fluxes while thin arrows represent the transfer factors.

Figure 6 .

 6 Figure 6. Measured (solid lines) and predicted (dotted lines) spectral SCEreflectances and -transmittances of one green translucent sheet on top of one red translucent sheet.

  Green sample on red sample

Fig. 4

 4 Fig. 4 represents the flux transfers for a stack of two samples in the framework of the two-flux model. Let us consider the sample labelled 1. The fluxes 0 I and 1 J illuminating it, and the outgoing fluxes 0J and 1 I can be related according to the following equations:

Table 1 . RMS deviations between the measured and predicted spectra and equivalent color deviations (∆E 94 ).

 1

	(a) Green samples
	0.1 r CC (λ)				1.0	r SCI (λ)				1.0	r SCE (λ)		1 Measured	Predicted
	0.08				0.8					0.8			2 3	2 3
	0.06				0.6					0.6			36	∞
	0.04				0.4					0.4
	0.02				0.2					0.2
	400	500	600	700	400	500	600	700	400		500	600	700
		wavelength (nm)					wavelength (nm)					wavelength (nm)
	1.0 t CC (λ)				1.0	t SCI (λ)				1.0	t SCE (λ)
	0.8				0.8					0.8
	0.6				0.6					0.6
	0.4				0.4					0.4
	0.2				0.2					0.2
	400	500	600	700	400	500	600	700	400	500	600	700
		wavelength (nm)					wavelength (nm)					wavelength (nm)
	(b) Red samples
													Measured	Predicted
	0.1 r CC (λ)				1.0	r SCI (λ)				1.0	r SCE (λ)		1
													2	2
	0.08				0.8					0.8			3	3
													52	∞
	0.06				0.6					0.6
	0.04				0.4					0.4
	0.02				0.2					0.2
	400	500	600	700	400	500	600	700	400		500	600	700
		wavelength (nm)					wavelength (nm)					wavelength (nm)
	1.0 t CC (λ)				1.0	t SCI (λ)				1.0	t SCE (λ)
	0.8				0.8					0.8
	0.6				0.6					0.6
	0.4				0.4					0.4
	0.2				0.2					0.2
	400	500	600	700	400	500	600	700	400	500	600	700
		wavelength (nm)					wavelength (nm)					wavelength (nm)

Figure 5. Measured and predicted spectral reflectances and transmittances of stacks of green or red sheets in Collimated-to-Collimated (left column), Specular Component Included (middle column) and Specular Component Excluded (right column) configurations. The numbers indicate the number of stacked sheets.

Table 2 . RMS deviations between the measured and predicted spectra and equivalent color deviations (∆E 94 ) for the SCE configuration.

 2

		SCE r		t	SCE
		RMSD	∆E 94	RMSD	∆E 94
	Green sheet on top of	0.0023	0.82	0.0085	0.79
	the red sheet	0.0271*	5.36*	0.229*	33.4*
	Red sheet on top of the	0.0144	3.33	0.0084	1.55
	green sheet	0.0325*	7.91*	0.237*	33.9*

Author Biography

Lionel Simonot completed


Sami Evangelista
email: evangeli@cnam.fr

Jean-François Pradat-Peyre

On the Computation of Stubborn Sets of Colored Petri Nets

Valmari's Stubborn Sets method is a member of the so-called partial order methods. These techniques are usually based on a selective search algorithm: at each state processed during the search, a stubborn set is calculated and only the enabled transitions of this set are used to generate the successors of the state. The computation of stubborn sets requires to detect dependencies between transitions in terms of conflict and causality. In colored Petri nets these dependencies are difficult to detect because of the color mappings present on the arcs: conflicts and causality connections depend on the structure of the net but also on these mappings. Thus, tools that implement this technique usually unfold the net before exploring the state space, an operation that is often untractable in practice. We present in this work an alternative method which avoids the cost of unfolding the net. To allow this, we use a syntactically restricted class of colored nets. Note that this class still enables wide modeling facilities since it is the one used in our model checker Helena which has been designed to support the verification of software specifications. The algorithm presented has been implemented and several experiments which show the benefits of our approach are reported. For several models we obtain a reduction close or even equal to the one obtained after an unfolding of the net. We were also able to efficiently reduce the state spaces of several models obtained by an automatic translation of concurrent software.

Introduction

State space analysis is a powerful formal method for proving that finite systems match their specification. It consists of enumerating all the possible configurations (or states) of the system to track the erroneous ones. A major obstacle to the application of this technique to industrial systems is the famous state explosion problem: the number of reachable states can be far too large to fit in memory or even on disk.

The state explosion has been the subject of many researches in the last two decades and techniques that alleviate this problem have been introduced. This includes the family of partial order methods which tackle one of the main sources of the combinatorial explosion: the concurrent execution of several components. These are based on the following observation: due to the interleaving semantic of concurrent systems, a set of different executions can have exactly the same effect on the system and be only a permutation of the same sequence. Thus, an efficient way to reduce the state explosion would be to explore only a single or some representative executions and ignore all the others permutations that are equivalent to the chosen ones. This is why the term of model checking using representatives [START_REF] Peled | All from one, one for all: on model checking using representatives[END_REF] seems more appropriate than the one of partial order model checking.

Valmari's stubborn sets method [START_REF] Valmari | State Space Generation : Efficiency and Practicality[END_REF][START_REF] Valmari | Error detection by reduced reachability graph generation[END_REF][START_REF] Valmari | Eliminating redundant interleavings during concurrent program verification[END_REF] is a member of this family. It is based on a selective search algorithm: at each state processed, a stubborn set of transitions is computed and only the enabled transitions of this set are used to generate the successors of the state. The elimination of some transitions from the stubborn set can cause some states not to be explored and can thus greatly reduce the number of visited states.

The problem of deciding if a set of transitions is stubborn at a state is at least as hard as the reachability problem [START_REF] Clarke | Model Checking[END_REF]. Thus, selective search algorithms exploit the structure of the modeled system to build sets for which the stubbornness conditions are guaranteed to hold. Construction algorithms are thus tightly linked to the formalism of the model, e.g., Promela [START_REF] Holzmann | An improvement in formal verification[END_REF], Petri nets, but, whatever the formalism, they always rely on the notion of dependency between transitions. When adding a transition to the stubborn set, one has to find the transitions that could disable or enable the considered transition. For ordinary PT-nets, these dependencies can be directly deduced from the structure of the net. For this reason, stubborn sets have been widely studied in the field of ordinary Petri nets and many algorithms were introduced to solve the problem. Examples include the deletion algorithm [START_REF] Valmari | State Space Generation : Efficiency and Practicality[END_REF][START_REF] Varpaaniemi | On the Stubborn Set Method in Reduced State Space Generation[END_REF], and the incremental algorithm [START_REF] Valmari | State Space Generation : Efficiency and Practicality[END_REF][START_REF] Varpaaniemi | On the Stubborn Set Method in Reduced State Space Generation[END_REF][START_REF] Valmari | Error detection by reduced reachability graph generation[END_REF].

The computation of stubborn sets for colored Petri nets is more problematic. Indeed, the detection of dependencies between transitions can not solely rely on the structure of the net but must also consider the color mappings that label arcs between places and transitions. A brute force approach consists then in unfolding the net, i.e., building the equivalent ordinary Petri net, in order to apply traditional stubborn sets algorithm for PT-nets. However, this unfolding step is not always possible because of large color domains. A possible way to avoid this unfolding is to work at the "colored" level, and to detect the dependencies between transitions symbolically. As a counterpart, we can not expect to obtain as good results as if the net was unfolded since the analysis of dependencies can not be as precise.

We investigate in this paper a solution for the computation of stubborn sets of colored Petri nets that does not rely on the unfolding of the net nor works at the transition binding level when constructing a stubborn set. Our algorithm detects dependencies directly on the colored Petri net. A keypoint is to use a slightly restricted class of colored Petri net that enables a symbolic detection of the dependencies. However, this class still allows wide modeling facilities since it is the one used in Helena [START_REF] Evangelista | High level petri nets analysis with Helena[END_REF] an explicit state model checker based on high level Petri nets and aimed at software verification. Related works. Stubborn sets of colored Petri nets were initially introduced by Valmari in [START_REF] Valmari | Stubborn sets for reduced state space generation[END_REF][START_REF] Valmari | Stubborn sets of coloured petri nets[END_REF]. His algorithm performs an implicit unfolding of the net: the net is not explicitly unfolded but the algorithm systematically enumerates transition bindings. The possibility to ignore the colors of the net, i.e., treat each colored transition as if it was an agglomeration of all its unfolded transitions, was also mentioned but not recommended, since it usually leads to unnecessary large stubborn sets.

Brgan and Poitrenaud proposed in [START_REF] Brgan | An efficient algorithm for the computation of stubborn sets of well formed petri nets[END_REF] an optimized version of Valmari's algorithm for well formed Petri nets which exploits the good structuring of the color domains and mappings of this class. The idea of their algorithm is to translate some structural relations into equivalent constraints systems before the search. These systems express dependencies between transition bindings and are thus repeatedly solved during the search to compute stubborn sets. Though their method can efficiently speed up the detection of dependencies, their construction of stubborn sets still works at the transition binding level. Consequently, their approach is not much different from unfolding the net.

To our best knowledge, the only algorithm proposed so far, that does not work at the binding level is [START_REF] Kristensen | Finding stubborn sets of coloured petri nets without unfolding[END_REF]. In this paper, the authors suggest that a possible way to obtain "good" stubborn sets for a colored Petri net without unfolding it is to add some extra informations on top of the structure of the net. The model designer must thus supply to the model checking tool some additional inputs, such as the type of the places (e.g., communication buffer, shared resource), that give crucial hints on the structure and the dynamic of the unfolded net. These informations are then used during the search in the stubborn sets construction. Their method seems to provide good reductions for a very low cost as acknowledged by the experimental results. The author argue that it is reasonable to assume that the type of information needed can be provided by the user. An analogy is made to the fact of typing variables in a program. However, there is no other possibility for the tool for validating these informations than unfolding the net or generating the complete state space, which is, by hypothesis, infeasible. Thus, in case of "typing error", the tool could produce wrong results. Another interesting contribution of [START_REF] Kristensen | Finding stubborn sets of coloured petri nets without unfolding[END_REF] is a theoretical result about the complexity of the problem: the size of the unfolded PT-net is the worst-case time complexity of any algorithm that computes nontrivial stubborn sets. A trivial stubborn set include all the transition bindings of the net.

This paper is organized as follows. The next section recalls some basic definitions and notations on colored Petri nets and stubborn sets. Our algorithm is presented in Section 3. Section 4 presents a set of experimental results. Lastly we conclude in Section 5.

Formal Background

We recall in this section the basic definitions and notions on colored Petri nets [START_REF] Jensen | Coloured petri nets: A high level language for system design and analysis[END_REF] and stubborn sets that are needed for the comprehension of this paper. We assume that the reader is familiar with PT-nets and their dynamic behavior.

N will denote the set of positive integers, N + the set N \ {0} and B = {f alse, true} the set of booleans.

The definition of colored Petri nets is based on multi-sets. A multi-set over a set S is a mapping from S to N. The set of multi-set over a set S is denoted by Bag(S). The addition, substraction, and comparison of multi-sets are defined in the usual way. ∅ denotes the empty multi-set. If m is a multi-set then e ∈ m ⇔ m(e) > 0.

If S is a set, S * is the set of finite words over S and S ∞ is the set of infinite words over S. The "." operator shall be used to denote the concatenation of two sequences. shall denote the empty sequence.

We shall denote by P(S) the powerset of a set S, i.e., the set of its sub-sets.

Colored Petri Nets

p) = m(p) - W -(p, t)(c) + W + (p, t)(c).
The state space of a CPN is the set of all the markings of the net which can be reached from the initial marking by a sequence of firings.

Definition 3 (State space).

Let N be a CPN. The state space (or reachability set

) of N is the minimal set S ⊆ M such that m 0 ∈ S and if ∃m ∈ S, t ∈ T, c ∈ C(t) such that m[(t, c) m then m ∈ S.
In the remainder we will often refer to the unfolded net of a CPN. Such a net is an ordinary PT-net obtained from the colored one by creating a node for each place or transition instance of the net. The flow relation of the unfolded net can then be derived by a direct application of the color mappings which label the arcs of the CPN.

Stubborn Sets

The stubborn sets method can be used to build a reduced state space of the system. The construction of this reduced state space can be done by introducing a little modification into a standard search algorithm: at each state processed, a stubborn set of transitions is computed and only the enabled transitions of this set are used to generate the immediate successors of the processed state. The set is said to be stubborn because the transitions outside it can not affect its behavior: it remains stubborn after the firing of any sequence of non stubborn transitions. Consequently, some transitions may never be executed, reducing the number of explored states. In the best case the reduction is exponential. Such a modified algorithm is usually called a selective search algorithm. The computation of the stubborn set must respect certain rules in order to preserve the desired property in the reduced state space. This has led to the introduction of several versions of the stubborn sets method. However, the notion of dynamic stubbornness is a common basis of many of these versions.

Definition 4 (Dynamic Stubbornness).

Let N be a Petri net, m be a marking of N and S ⊆ T . The set S is dynamically stubborn at m if conditions D1 and D2 hold where:

D1 ∀t ∈ S, σ ∈ (T \ S) * , m[σ.t ⇒ m[t.σ D2 (∃t ∈ T | m[t ) ⇒ ∃t ∈ S | ∀σ ∈ (T \ S) * , m[σ ⇒ m[σ.t
Condition D1 states that the firing of a sequence of transitions that are outside the stubborn set can not enable the firing of a disabled transition of S while D2 ensures that if the marking is not dead, then there is an enabled transition in the stubborn set (called a key transition in the stubborn set terminology) which remains firable after the firing of any sequence of non stubborn transitions. It is well known that a selective search algorithm which computes stubborn sets having the dynamic stubbornness property builds a reduced state space which contains all the dead markings of the initial state space and at least one infinite sequence if such a sequence exists. Because of the ignoring phenomenon [START_REF] Valmari | Stubborn sets for reduced state space generation[END_REF], that's basically all that this definition preserves: a firable transition may be infinitely forgotten in the stubborn set computation. In order to verify more elaborated properties, such as liveness properties, it is crucial to prevent this ignoring phenomenon and to add additional constraints in the computation of the stubborn set, possibly leading to less reductions. For instance it is usually needed that along each cycle of the reduced reachability graph, a transition enabled at a marking of the cycle belongs to at least one of the stubborn sets computed for the markings of the cycle. However, this subject is beyond the scope of this work and we will focus our attention on the dynamic stubbornness from definition 4. Thus in the remainder of the paper, we will call a stubborn set a set of transitions which respect the dynamic stubbornness property.

Symbolic Computation of Stubborn Sets

We present in this section an algorithm to compute stubborn sets of colored Petri nets. The proposed method does not rely on an explicit or implicit unfolding of the net but rather on the two following ideas:

-We treat instances classes instead of explicitly enumerating instances. We thus obtain an algorithm which complexity is independent from the size of the unfolded net. -We define a class of colored Petri nets allowing an efficient detection of the dependencies between the transitions of the net.

Our method is therefore inspired by two works [START_REF] Brgan | An efficient algorithm for the computation of stubborn sets of well formed petri nets[END_REF][START_REF] Kristensen | Finding stubborn sets of coloured petri nets without unfolding[END_REF] on the same subject which have been mentioned in the previous section.

In the remainder of the section we will proceed as follows. Firstly we give a static stubbornness definition for PT-nets on which our algorithm is based. Then we make an informal presentation of our algorithm with the help of an example which illustrates several difficulties that arise when directly handling colored nets instead of unfolding. A syntactically restricted class of CPN is introduced in the third part of the section along with additional definitions needed to handle bindings classes. The last part of the section is more technical and deals with a concrete implementation of the algorithm for our CPN class.

Static Stubbornness for PT-Nets

The dynamic stubbornness definition is based on the semantic of the net, i.e., its reachability graph, and it is thus difficult to obtain an "implementation" of this property. Moreover, it has been proved that the problem of deciding if a set is stubborn is at least as hard as checking reachability for the full reachability graph [START_REF] Clarke | Model Checking[END_REF] which is exactly what we want to avoid. Consequently, rather than checking the dynamic stubbornness property for an arbitrary set of transitions, algorithms usually exploit the structure of the modeled system to produce sets of transitions for which the dynamic stubbornness is guaranteed to hold. Such algorithms have been proposed for various description languages, e.g., Promela [START_REF] Holzmann | An improvement in formal verification[END_REF], Variable/Transition systems [START_REF] Valmari | Stubborn sets for reduced state space generation[END_REF], and Petri nets [START_REF] Valmari | State Space Generation : Efficiency and Practicality[END_REF][START_REF] Valmari | Error detection by reduced reachability graph generation[END_REF][START_REF] Varpaaniemi | On the Stubborn Set Method in Reduced State Space Generation[END_REF].

We now introduce a stubbornness definition for Petri nets. It is far from being optimal and could be refined, e.g., see [START_REF] Varpaaniemi | On the Stubborn Set Method in Reduced State Space Generation[END_REF], but we will use it for its simplicity.

Definition 5 (Stubbornness).

Let N be a Petri net, m be a marking and S ⊆ T . S is stubborn at m if the three following conditions are satisfied:

1. (∃t ∈ T | m[t ) ⇒ ∃t ∈ S | m[t 2. if t ∈ S and m[t then ( • t) • ⊆ S 3. if t ∈ S and ¬m[t then ∃p ∈ • t such that m(p) < W -(p, t) and • p ⊆ S
Item 1 prevents from picking an empty set if there are enabled transitions. Item 2 ensures that a firable transition t remains firable after the firing of a sequence which only includes transitions outside the stubborn set. Indeed, all the transitions which could prevent the firing of t, i.e., the set ( • t) • , are also in the stubborn set. Let us note that all the enabled transitions selected in the stubborn sets are thus key transitions since they remain firable. At last item 3 ensures that a disabled transition t remains disabled after the firing of a sequence of non stubborn transitions since place p prevents the firing of t and transitions that could put tokens in it are also stubborn. The place p of this item is usually called a scapegoat in the stubborn sets terminology.

These three items are thus sufficient to prove the following proposition.

Proposition 1. Let N be a Petri net, m be a marking and S ⊆ T . If S is stubborn at m then it is dynamically stubborn at m.

The previous definition can be used to define a stubborn sets computation algorithm for PT-nets. This algorithm initiates the construction with an enabled transition and successively applies item 2 and 3 until reaching a fix point. If the marking does not enable any transition then it directly returns an empty set.

The goal of our work if to present a "colored" version of this algorithm. We will see that difficulty arise with the introduction of color mappings in the net and how to deal with this additional complexity.

Informal Presentation of the Algorithm

At first we informally present our algorithm with the help of the net of figure 1. This net models the part of a distributed system in which different client and server process interact. Clients compete for acquiring access to a pool of shared objects. To each object of the pool is an associated lock guaranteeing an exclusive access to the object. An idle client C can evolve in two different ways. First he can try to grab the lock of object O (transition takeLock). Alternatively, if a server S has acknowledged his request (transition sendAck) he can choose to receive and treat this acknowledgment (transition receiveAck). We denote {c 1 , . . . , c n } the set of clients, {s 1 , . . . , s m } the set of servers and {o 1 , . . . , o l } the set of shared objects.

We propose to detail a few steps of the construction of the stubborn set S at the marking m depicted.Binding tb 1 = (takeLock, C = c 1 , O = o 1 ) is enabled at m and we choose it to initialize the stubborn set S.

Binding tb 1 = (takeLock, C = c 1 , O = o 1
Since tb 1 is enabled we must apply the second item of definition 5 and identify the instances in conflict with it to

m(locks) = o 1 + o 2 m(serverSend) = ∅ m(serverIdle) = ∅ m(ack) = ∅ + c 2 , o 1 m(clientIdle) = c 1 , o 1 C, O O C, O C,
= (receiveAck, C = c 1 , O = o 1 )
is clearly in conflict with tb 1 . Indeed, they both withdraw the token c 1 , o 1 from place clientIdle. We therefore include tb 2 in S. What seems less clear from a PT-net point of view is that tb 1 is also in conflict with other bindings of transition takeLock. An analysis of the unfolded net would indeed reveal that bindings of set ∪ c∈{c2,...,cn} {(takeLock, C = c, O = o 1 )} also withdraw token o 1 from place locks and must thus be included in S. Algorithms of [START_REF] Valmari | Stubborn sets of coloured petri nets[END_REF] and [START_REF] Brgan | An efficient algorithm for the computation of stubborn sets of well formed petri nets[END_REF] would directly insert these n -1 bindings. The size of the stubborn set would then quickly increase as color domains grow. This may even fail with infinite color domains. Our approach is different since we choose to not explicitely enumerate these n -1 bindings but rather to treat this set as a single unit. For this purpose we introduce the symbol which will be used to denote "any item" of a color. Thus we will say that tb 1 is in conflict with binding tb 3 = (takeLock, C = , O = o 1 ), i.e., all the clients who wishes to acquire the same lock. Since tb 3 is a compact representation of a set of bindings we will rather use the term bindings class or more simply class.

Binding tb 2 = (receiveAck, C = c 1 , O = o 1 )
To be enabled tb 2 needs a token c 1 in place ack. The instance (ack, c 1 ) is therefore chosen as a scapegoat. The set ∪ s∈{s1,...,sm} {(sendAck, S = s, C = c 1 )} includes all the bindings which can produce this token. We thus add class tb 4 = (sendAck, S = , C = c 1 ) to S. In other words, the only event that can cause the reception by c 1 of an acknowledgment is the sending of this acknowledgment whatever the sending server.

Binding tb 3 = (takeLock, C = , O = o 1 )
The introduction of the concept of bindings class raises here a difficulty. Indeed, since we want to treat all the bindings of this class as a unit without differentiating them we have to assign the same status (disabled / enabled) to all these bindings in order to apply the second or third item of definition 5. In practice, the number of enabled bindings of a CPN always remains relatively low even when the color domains are large. We thus choose to proceed as follows. We treat each class as if all the bindings within it were disabled and we extract from it the enabled bindings which are inserted into the stubborn and treated separately. Thus an enabled binding added by this way to the stubborn set will be both considered as disabled and enabled. Though this will produce larger stubborn sets, this does not affect the validity of our algorithm. For instance, the two enabled bindings We mentioned in the introduction of this section that the time complexity of this algorithm is not related to the size of the unfolded net. As a matter of fact, the worst time complexity is indeed related to this size since each enabled binding can be processed and the number of enabled bindings is bounded by the number of transitions in the unfolded net. However, in practice, we observe that, even when the types of places and transitions are very large, the number of enabled bindings remains reasonable. So the worst time complexity of our algorithm is rarely reached.

tb 1 = (takeLock, C = c 1 , O = o 1
This example highlighted the necessity to have CPNs with a well structured syntax. Indeed, each time we processed a binding we exploited the structuring of the arc functions to detect dependencies between transitions. This approach would typically fail with CPNs having arbitrarily complex arc functions or color domains. We introduce in the next sub-section a class of CPNs inspired by Well Formed colored nets [START_REF] Chiola | On well-formed coloured nets and their symbolic reachability graph[END_REF] which, on one hand, allows us a symbolic detection of dependencies and, on the other hand, still enables large modeling facilities.

A Class of Colored Petri Nets

Color domains of our colored nets are Cartesian products of finite and non empty sets called basic types. A color domain item will be noted as a tuple, e.g., 2, true . In addition, for each transition t, we will assume a bijective mapping associating each element of its color domain to a variable which will appear in the tuple, e.g., X = 2, B = true .

Definition 6 (Color domain). The set of basic types Δ is a finite set of finite and non empty sets. A color domain

Color mappings of the net are built with the help of elementary expressions. Two types of elementary expressions are allowed: the projection (or variable) and the functional expression. The first one is used to choose a specific element in an item of a color domain. Functional expressions are provided to enable complex operations on basic types. All the valid expressions from a color domain to a basic type can be put in this family. Projections are thus particular cases of functional expressions.

Definition 7 (Elementary expression). Let C ∈ C and δ ∈ Δ. E C,δ , the set of elementary expressions from

C to δ is the set E C,δ = V C,δ ∪ F C,δ where -V C,δ = {V i | i ∈ [1..s(C)] ∧ C i = δ}
is the set of projections from C to δ. V i is defined by:

∀c = c 1 , . . . , c s(C) ∈ C, V i (c) = c i . -F C,δ = {(f, (e 1 , . . . , e n )) | f ∈ δ 1 × • • • × δ n → δ ∧ ∀i ∈ [1..n], e i ∈ E C,δi }
is the set of functional expressions from C to δ. (f, (e 1 , . . . , e n )) is defined by: ∀c ∈ C, (f, (e 1 , . . . , e n ))(c) = f (e 1 (c), . . . , e n (c))

In our examples, instead of using the formal notation V i we will prefer to use the variable of the transition at position i. For example V 2 will be directly noted B if the second element of the transition domain is associated to this variable. Expressions tuples are basic components of color mappings. They can be guarded by a boolean expression which condition the tokens production. The syntax of guards will appear later in this section. A tuple (γ, α, e 1 , . . . , e n ) will also be noted [γ] α • e 1 , . . . , e n . For instance [X > Y ] 2 • X, 0, f(Y ) is a valid example tuple. Given an instantiation of the variables X and Y of the transition it produces 2 items of type X, 0, f(Y ) if X > Y . Otherwise, it produces the empty multi-set.

At last, color mappings that label the arcs of the net are sums of elementary expressions tuples.

Definition 9 (Color mapping). Let C, C ∈ C. A color mapping

f from C to Bag(C ) is a sum f = k i=1 tup i (with ∀i ∈ [1..k], tup i ∈ T up C,C ) defined naturally. The set of color mappings from C to Bag(C ) is noted M ap C,C .
A color mapping will sometimes be considered as the union of the tuples which constitute it, i.e., tup ∈ map ⇔ map = tup + map .

Expressions tuples and transitions can be guarded by a boolean expression which states under which conditions the tuple produces items or the transition if firable. We do not impose special constraints on these guards. Any boolean expression on the color domain of the transition is a valid guard.

Definition 10 (Guard). Let C ∈ C. G C = E C,B is the set of guards over C.

Dealing with instances classes. We first "extend" basic types by including to them the symbol. The same extension is done for color domains. The definition assumes that this symbol does not belong to any basic type.

Definition 11 (Extended color domain). Let δ ∈ Δ. The extended type δ is the set δ ∪ { }. The set of extended types Δ is the set {δ |δ ∈ Δ}. Let C ∈ C. The extended color domain C is the Cartesian product C 1 × • • • × C s(C) . The set of extended color domains is noted C .

We must also modify the semantics of the elementary expressions to take into account this extension. The value of a projection is unchanged. If a sub-expression of a functional expression e is evaluated to so is e. Otherwise its value does not change.

Definition 12 (Extended elementary expression).

Let C ∈ C, δ ∈ Δ, and e ∈ E C,δ . The extended expression e from C to δ is defined by: ∀c ∈ C such that c = c 1 , . . . , c n :

e (c) = ⎧ ⎨ ⎩ if e = V i then c i if e = (f
-U nf δ (e) = if e = then δ else {e} -nf C ( c 1 , . . . , c n ) = U nf C1 (c 1 ) × • • • × U nf Cn (c n )
Lastly we introduce the inclusion relation C defined for every basic type or color domain C. We have c C c if each item c i of c is either the symbol either c i , the item at the same position in c . For instance, it holds that true, B×B true, f alse , but true, B×B f alse, does not. Trivially, if c c then U nf C (c ) ⊆ U nf C (c). We will then say that c is a subclass of c.

Definition 14 (Inclusion relation). Let C ∈ C. The relation

C over C ×C is defined by: c 1 , . . . , c n C c 1 , . . . , c n ⇔ ∀i ∈ [1..n], c i = ∨ c i = c i .
We will omit in the sequel the subscript and superscript of U nf C , C or e when there will be no ambiguity.

The Algorithm

We now introduce the general algorithm (figure 2) to compute a stubborn set of transitions of a CPN. Its input is a marking m of the CPN and it returns a stubborn set at m. Three main data structures are used. S is the stubborn set computed. U is the set of bindings classes which have not been treated yet. N is the set of binding classes which must be included in the stubborn set.

An enabled binding is randomly chosen to initialize the stubborn set and the set of unprocessed classes (line 1). If there is no enabled binding at m, the empty set is directly returned. At each iteration, a binding class (t, c t ) is removed from U and treated by the algorithm (lines 3-4). If this class is composed of a single binding, i.e. the symbol does not appear in it, enabled at m we apply item 2 of the stubbornness definition and we compute the set of bindings classes in conflict with (t, c t ) (line 6). Otherwise we consider it as a class of disabled bindings. We first check (line 8) if c t is not a subclass of a previously treated class c t , i.e., all the bindings of c t are in c t . In this case the stubborn set is unchanged. Else the algorithm applies item 3 and computes the classes of bindings which produce tokens needed by the disabled bindings of (t, c t ). Additionally, we must include in N all the enabled bindings which belong to the bindings class (t, c t ) (line 11).

stubborn (m) 1 S ← if ∃(t, ct) such that m[(t, ct) then {(t, ct)} else ∅; U ← S 2 while U = ∅ do 3 let (t, ct) ∈ U with ct = ct,1, . . . , ct,n 4 U ← U \ {(t, ct)} 5 if ∀i ∈ [1..n]

Implementing Algorithm's Operations

The algorithm of figure 2 is a generic one in the sense that it is not related to our CPN class and could theoretically be implemented for any colored net. We have seen in our introductory example that an efficient implementation of the mappings enablingClasses and disablingClasses seems to require colored nets well structured enough to enable symbolic computations or alternatively some user supplied informations as it is done in [START_REF] Kristensen | Finding stubborn sets of coloured petri nets without unfolding[END_REF].

We detail now an implementation of these operations for our CPN class.

Reversing color mappings.

A frequently used operation in our algorithm is the reverse operation. This one consists of finding for a given color c and a color mapping f the set of colors c such that f (c )(c) > 0. Different methods have been proposed in the literature to address this problem in an efficient way (e.g., [START_REF] Dutheillet | Structural analysis of coloured nets. application to the detection of confusion[END_REF], [START_REF] Brgan | An efficient algorithm for the computation of stubborn sets of well formed petri nets[END_REF], [START_REF] Capra | A high level language for structural relations in well-formed nets[END_REF], [START_REF] Evangelista | Syntactical colored petri nets reductions[END_REF]) for Well Formed nets or similar classes. Even for this formalism, the problem is quite hard, and the solutions proposed either extend the formalism [START_REF] Capra | A high level language for structural relations in well-formed nets[END_REF] or add some extra restrictions on arc functions [START_REF] Evangelista | Syntactical colored petri nets reductions[END_REF].

For our colored nets, the reverse operation is, in general, impossible to apply without an explicit enumeration of colors. This is due to the possibility to insert in tuples some functional expressions which can obviously not be reversed. However, we can still approximate the result of this operation by exploiting the elementary expressions that are "well formed", i.e., the projections, and which are easily reversible.

We now introduce the mapping reverseM ap t,p defined for every couple (p, t) of P × T . Given a color mapping map from C(t) to Bag(C(p)) and a class c p ∈ C(p) , reverseM ap t,p computes a set of classes of transition t which is such that any binding of t which image by map contains a token of class c p belongs to one of the classes computed. More formally, the following proposition must hold for all c ∈ U nf (c p ) and c ∈ C(t):

map(c )(c) > 0 ⇒ ∃c t ∈ reverseM ap t,p (c p , map) | c ∈ U nf (c t )
Using the fact that a color mapping is a sum of tuples we reduce the problem to the definition of the tuple reversal mapping reverseT up t,p (definition 15).

We can clearly identify two steps in this procedure. In the first one we identify the class of bindings (t, c t ) such that tup(c t )(c) > 0 for some c of class c p . This is done by initializing the resulting class to , . . . , which covers all the bindings of t and by looking for projections in tup. When a projection V j is found at position i in the tuple we replace in r the at position j by the item at position i in c p . For instance reverseT up t,p ( 0, 1, 2 , X, Z, f (Y ) ) = { X = 0, Y = , Z = 1 }. The class computed is clearly an over-approximation of the bindings which are really needed. This is mainly due to the fact that functional expressions may appear in the tuple and that such expressions can not be handled without being "unfolded". Since this is typically what we want to avoid, we have no other choice than ignoring these expressions in this first step. A possible optimization would be to identify expressions which can be reversed, and to exploit this reversibility, e.g., reverseT up t,p ( 1 , X + 1 ) = { X = 0 }.

The second step of the reverse operation consists of checking if the computed class is inconsistent with respect to the tuple or the transition. A first inconsistency may appear if there is an expression e i in the tuple which can be evaluated with binding r, i.e., e i (r) = , and which value is different from c i , the item at the same position in class c p (if c i = ). We can then directly return the empty set since there is obviously no binding of t which can produce by tup a token of class c. For instance, reverseT up t,p ( 2, 2 , X, X + 1 ) = ∅. A second inconsistency is detected if either the guard of the tuple or the guard of the transition can be evaluated and does not hold. For instance, reverseT up( 0, , [X > 0] X, Y ) = ∅. Let us recall that these guards or the expressions in the tuple may not be evaluable since the variables which appear in these can have an undefined value.

Definition 15. Let t ∈ T and p ∈ P . The mappings reverseM ap t,p from C(p) × M ap C(t),C(p) to P(C(t) ) and reverseT up t,p from C(p) × T up C(t),C(p)

to P(C(t) ) are defined by:

reverseM ap t,p (c p , map) = tup∈map reverseT up t,p (c p , tup) reverseT upt,p (cp, tup) 1 let cp = c1, . . . , cn 2 let tup = [γ] α • e1, . . . , en 3 r ← , . . . , 4 for i ∈ [1..n] do if ei = Vj and rj = then rj ← ci 5 (* check inconsistencies *) 6 if ∃i ∈ [1.
.n] such that ei(r) = and ci = and ei(r) = ci then return ∅ 7 if γ(r) = false or φ(t)(r) = false then return ∅ 8 return {r} Computing scapegoats. The treatment of a disabled bindings class c involves to identify the bindings firing of which can enable the elements of c. This detection is based, in our static stubbornness definition, on the ability to compute a scapegoat. A scapegoat of a low-level transition t at a marking m is a place which disables t, i.e. W -(p, t) > m(p). For a high-level transition binding (t, c t ) it is simply a couple (p, c p ) such that p ∈ P, c p ∈ C(p) and W -(p, t)(c t )(c p ) > m(p)(c p ). When directly handling bindings classes instead of explicit bindings a difficulty appears that was not highlighted by our introductory example. Indeed, we must find a scapegoat for all the bindings within the class. Thus, in some cases, we will have to choose several scapegoats. We illustrate this problem with the help of the following net.

t q X, Y p Y, f alse Let us consider the class c t = X = 2, Y =
of transition t for which we have two possible scapegoats: (q, , f alse ) and (p, 2, ). For instance, at the two markings m and m our algorithm will proceed as follows:

for m defined by m(p) = 2, 3 , m(q) = 4, true Class (q, , f alse ) is a valid scapegoat for all the bindings of c t since no token in q has f alse as its second component. -for m defined by m (p) = 2, 3 , m (q) = 4, false Class (q, , f alse ) can not be chosen since m (q) ≥ W -(t, q)(c) for c = X = 2, Y = 4 which belongs to the class c t . For the same reason, (p, 2, ) can not be chosen since m (p) ≥ W -(p, t)( X = 2, Y = 3 ). Consequently, both classes, i.e., (q, , f alse ) and (p, 2, ), must be chosen to ensure that each binding of c t has a scapegoat in one of the two classes. Once again, this example shows that working at the high-level has a cost insofar as we compute a set of scapegoats which, from a PT-net point of view, is clearly unnecessarily large. The purpose of function scapegoat is to find, given a bindings class (t, c t ), and a marking m, a set of scapegoat classes for (t, c t ) at m: each disabled binding of (t, c t ) has a scapegoat in a class of scapegoat(t, c t , m). More formally, the following must hold for all c ∈ U nf (c t ) such that¬m[(t, c) :

∃(p, c p ) ∈ scapegoat(t, c t , m), c ∈ U nf (c p ) | W -(p, t)(c)(c ) > m(p)(c )
The function proceeds in two steps. It first tries to find a unique class which is an acceptable scapegoat for all the bindings of c t . A sufficient condition is that there is a tuple [γ]α • e 1 , . . . , e n appearing in the input arc from p to t such that all the tokens present in p at m fulfill one of these two conditions:

-The multiplicity of the token is strictly less than the factor of the tuple α. -There is an expression at position i in the tuple which produces with c t a value different from and different from the item at the same position in the token.

In addition, the guard of the tuple must evaluate to true with c t . Otherwise, i.e., γ(c t ) = f alse or γ(c t ) = , there could be instances in c t for which the tuple does not produce any item. For these instances, the token consumed by the tuple is obviously not a valid scapegoat. If there exists such a tuple tup, then it is straightforward to see that ∀c ∈ U nf (c t ), tup(c) > m(p). The token produced by the tuple can therefore be chosen as a scapegoat.

If we fail to find such a tuple then we pick all the tokens consumed by the bindings of c t . This set is obviously a correct scapegoat for c t . However, all the couples (p, c ) for which it necessarily holds that m(p)(c ) ≥ W -(p, t)(c)(c ) for any c of c t can be safely withdrawn from this set. A sufficient condition for this to hold is that there exists a tuple tup in W -(p, t) such that (1) c p , the image of c t by tup does not contain the symbol, (2) the multiplicity of c p at m is greater than the maximal multiplicity of any item produced by W -(p, t), i.e., Γ (W -(p, t)). Definition 16. The mapping scapegoat from T ×C ×M to P(P × C ) is defined by: scapegoat where

(t, c t , m) = ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ if ∃p ∈ • t
Γ (map) = k i=1 α i with map = k i=1 (γ i , α i , E i )
The size of the reduced reachability graph depends to a large extent on the stubborn sets computed. Though always choosing the stubborn set with the lowest number of enabled bindings does not necessarily yields the best reduction it seems however to be the best and simplest heuristic. The choice of the scapegoats is a nondeterministic factor which can affect the number of enabled bindings in the resulting stubborn set. For PT-nets different strategies have been proposed in [START_REF] Varpaaniemi | On choosing a scapegoat in the stubborn set method[END_REF]. Our implementation of mapping scapegoat sorts "scapegoat candidates" according to three criteria and chooses the first candidate according to this sorting. These three criteria are (we note C the set of bindings classes which are directly inserted into the stubborn set if the scapegoat if chosen): [START_REF] Brgan | An efficient algorithm for the computation of stubborn sets of well formed petri nets[END_REF] the number of enabled bindings in C, (2) the number of which appear in the classes of C, and (3) the number of classes in C. We thus try to limit the number of enabled bindings and the number of transitions of the unfolded net inserted to the stubborn set right after the choice of the scapegoat. Indeed, the number of low-level transitions covered by a class directly depends on the number of stars which appear in the class.

After intensive experiments we observed that this strategy competes favorably against a pseudo-random strategy.

. Mappings disablingClasses and enablingClasses. Concluding, we define the mappings disablingClasses and enablingClasses.

The definition of mapping disablingClasses is based on this simple observation: a binding (t, c t ) remains firable as long as any binding which could withdraw tokens needed by (t, c t ) are not fired. It is thus sufficient to inspect the tokens consumed by (t, c t ) and to identify the bindings which consume these tokens by an application of the reverse operation. Therefore we closely follow the stubbornness definition for PT-nets (definition 5).

Definition 17. The mapping disablingClasses from T × C to P(T × C

) is defined by: disablingClasses(t, c t ) =

p∈ • t,t ∈p • ,cp∈W -(p,t)(ct) reverseM ap t ,p (c p , W -(p, t ))
To identify the bindings which can enable the instances of a class c t of transition t we enumerate the scapegoats of (t, c t ) and, for each scapegoat (p, c p ), we look at each input transition t of p. An application of the reverse operation gives us the bindings of t which put tokens of class c p in p. Once again this definition respects the static stubbornness definition for PT-nets.

Definition 18. The mapping enablingClasses from T × C × M to P(T × C

) is defined by: enablingClasses(t, c t , m) = (p,cp)∈scapegoat(t,ct,m),t ∈ • p reverseM ap t ,p (c p , W + (p, t ))

Experiments

The algorithm described in this work has been implemented in our model checker Helena [START_REF] Evangelista | High level petri nets analysis with Helena[END_REF]. This section reports the results of two series of experiments that have been carried out. In the first series considered we analyzed some models obtained from concurrent programs by an automatic translation using the Quasar [START_REF] Evangelista | Dynamic tasks verification with Quasar[END_REF] tool. In the second one we considered several academic models included in the Helena distribution (available at http://helena.cnam.fr) of which some are recurrent examples of the CPN literature.

All measures were obtained on a Pentium IV with a 2.4 Ghz processor.

Models extracted from programs (table 1).

Four real concurrent programs were first translated using the tool Quasar: an implementation of Chang and Roberts election protocol, two different implementations of the dining philosophers and a client-server protocol with dynamic creation of servers to handle client requests. Helena could not unfold these CPNs due to the huge color domains of the nodes. Indeed, some places of the net model variables having highlevel data types, e.g., records or arrays. Each program is scalable by a parameter and we considered several values of this parameter (the value is given in the first column) and ran two tests: one without the stubborn method enabled (column . We observe that, despite the complexity of the CPNs obtained from an automatic translation of programs, our algorithm gives a significant reduction for the four programs considered. The reductions factor goes from 7 in the worst case (the leader election program) to almost 400 in the best case (the client / server program) and makes realistic the automatic verification of concurrent software.

To further enhance the reduction we plan to combine our method with [START_REF] Kristensen | Finding stubborn sets of coloured petri nets without unfolding[END_REF]. Concurrent programs can indeed easily be mapped to process-partitioned CP nets of [START_REF] Kristensen | Finding stubborn sets of coloured petri nets without unfolding[END_REF] with a simple static analysis of the program. For instance, places corresponding to variables local to a process can be typed as local and places corresponding to variables accessed by several processes can be typed as shared.

Academic models (table 2).

We then considered several academic models which size allows (except for one) an unfolding. For each model we therefore ran an additional test with Prod and its stubborn set algorithm activated. Let us recall that Prod unfolds the net in order to apply the stubborn set method. We used the deletion algorithm of Prod (option -d) which is, to our best knowledge, the most advanced algorithm for PT-nets. The reduction observed with Prod must be seen as a lower bound which is hard to reach without unfolding the net. Comparing the size of the graph reduced by Helena to the size of the complete graph tells us how good the reduction is while comparing it to the graph reduced by Prod tells us how good the reduction could be.

The examples studied can be classified in four categories. In a first category we can put the models for which the graph is weakly reduced by Helena but efficiently reduced by Prod. The two models which belong to this category are the slotted ring protocol and to a lesser extent Lamport's algorithm. We are currently not able to explain the bad results obtained for these two models but plan to investigate this.

The dining philosophers, Eisenberg and McGuire's algorithm, and the election protocol constitute a second category. Their characteristic is that their graph is weakly reduced both by Helena and Prod. A surface analysis may let us think that our algorithm performs a bad reduction for these models. However the poor results obtained with Prod show that we can not expect much better. Indeed, there are some problems for which partial order methods are inefficient. Models such as the dining philosophers or the Eisenberg and McGuire's algorithm which make heavy use of shared resources such as global variables usually fall into this category. These shared resources are a major source of conflicts which lead to compute large stubborn sets yielding a small reduction.

A third category is made up of the distributed database system and Peterson's algorithm. For these two models Helena builds a very reduced graph but Prod can do even better by unfolding the net. This particularly holds for the database system. Its initial graph is in O N • 3 N . Helena builds a reduced graph in O N 2 • 2 N . Prod produces a reduced graph in O N 2 . An analysis of these nets reveals a certain complexity in arc mappings which makes it hard to efficiently detect dependencies without unfolding the net. Let us note that our reduced graph has exactly the same size as in [START_REF] Kristensen | Finding stubborn sets of coloured petri nets without unfolding[END_REF] where they use a semi-automatic algorithm.

At last, for the four other models Helena performs a reduction close or equal to the reduction performed by Prod but outperforms significantly Prod with respect to time. The best results are observed for Eratosthene's algorithm: Helena builds a reduced reachability graph which size is linear with respect to the parameter of the system despite the high complexity of the arc functions. In addition, we notice that the net could not be unfolded because of the size of the color domains. For the multiprocessor and the resource allocation systems we obtain a reduced graph which is exactly the same as the one obtained by Prod. Lastly, for the load balancing system, the gain obtained by unfolding the net is completely marginal with respect to the brutal increase of the exploration time.

Conclusion

The contribution of this paper is a stubborn sets computation algorithm for colored Petri nets which avoids the unfolding by mixing two approaches. First we do not directly handle explicit bindings but rather bindings classes. We therefore stay at the high-level and never explicitly enumerate the transitions of the unfolded net. Second we define a syntactically restricted class of colored Petri nets for which it is possible to detect dependencies in a symbolic manner while preserving high expressiveness. As a counterpart, the detection of the dependencies between transitions can not be as fine as on the unfolded net and some approximations are done which lead to larger stubborn sets.

A set of experimental results have shown the benefits of our approach. For many academic models we achieved a reduction close or equal to the one obtained after an unfolding of the net. We were also able to significantly reduce the state spaces of several concurrent programs automatically translated to colored nets by the Quasar tool. The unfolding approach fails for these colored nets having huge unfolded nets.

In future works we will combine our algorithm with the method of [START_REF] Kristensen | Finding stubborn sets of coloured petri nets without unfolding[END_REF]. Our algorithm exploits the structuring of our CPN class whereas their method is based on user supplied informations. Both should therefore be fully compatible and lead to better reductions.

  ) and tb 5 = (takeLock, C = c 2 , O = o 1 ) both belong to the class tb 3 and must therefore be included in S. Let us come back to tb 3 . Each disabled binding b = (takeLock, C = c i , O = o 1 ) of this class needs a token o 1 in locks and a token c i , o 1 in clientIdle. Since m(locks)( o 1 ) = 1, the absence of token c i , o 1 is the reason why b is disabled. Once again we avoid an explicit enumeration of these scapegoats by using the symbol: the scapegoat of class tb 3 is (clientIdle, , o 1 ). Such an approximation is valid since any disabled binding of tb 3 has a scapegoat place in this class. Item 3 requires that we insert in S the bindings which put in clientIdle tokens belonging to class , o 1 . The single input of clientIdle is gotoIdle. By looking at the color mapping which labels the arc from gotoIdle to clientIdle we notice that a binding (gotoIdle, C = c, O = o ) can produce a token of class , o 1 if and only if o = o 1 . Consequently, we must add (gotoIdle, C = , O = o 1 ) to S.

  C is a product C 1 ו • •×C s(C) where C i ∈ Δ and s(C) ∈ N is the size of C. The set of color domains is noted C.

Definition 8 (

 8 Elementary expressions tuple). Let C, C ∈ C. The set of elementary expressions tuples (or tuples) from C to Bag(C ), is noted T up C,C and is the set of triplets (γ, α, E) such that: γ ∈ G C is the guard of the tuple; α ∈ N + is the factor of the tuple; E = e 1 , . . . , e s(C ) , with ∀i ∈ [1..s(C )], e i ∈ E C,C i , is the expressions list of the tuple. tup = (γ, α, e 1 , . . . , e n ) is defined by: ∀c ∈ C, tup(c) = if γ(c) then α • e 1 (c), . . . , e n (c) else ∅.

Definition 2 (Firing rule). Let N be

	Given a node n of P ∪ T , C(n) will be called the color domain of n. The set
	of inputs (resp. outputs) of a place p is the set • p (resp. p • ) defined by: • p =
	{t|W + (p, t) = 0} 1 (resp. p • = {t|W -(p, t) = 0}). The same sets can be defined
	for a transition t : • t = {p|W -(p, t) = 0} and t • = {p|W + (p, t) = 0}. These
	notations are extended to set of nodes as usual.
	The firing rule defines the dynamic of the net.
	a CPN and m ∈ M. The instance c
	of transition t is firable (or enabled) at m (denoted by m[(t, c) ) if and only
	if φ(t)(c) ∧ m(p) ≥ W -(p, t)(c). The firing of the instance (t, c) at m leads
	to a marking m (denoted by m[(t, c) m ) defined by: ∀p ∈ P, m (

Definition 1 (Colored Petri net). A colored Petri net (or CPN

) is a tuple P, T, C, W -, W + , φ, m 0 where P is a finite set of places; T is a finite set of transitions such that P ∩T = ∅; C a color function is a mapping from P ∪T to Σ, a set of finite and non empty sets; W -and W + the forward and backward incidence matrixes associate to each pair (p, t) of P × T a mapping from C(t) to Bag(C(p)); φ a guard function associates to each t ∈ T a mapping from C(t) to B; and m 0 an initial marking is an element of M the set of mappings which associate to each p ∈ P an element of Bag(C(p)).

From now on a CPN N will implicitly define the tuple P, T, C, W -, W + , φ, m 0 .

  , e 1 , . . . , e m ) then if ∀i ∈ [1..m], e i (c) = then e(c) elseWe will often use in this section the unfolding mapping defined below which is used to enumerate all the items within a class, e.g., U nf B×B ( , true ) = { f alse, true , true, true }.

Definition 13 (Class unfolding). Let δ ∈ Δ and C ∈ C. The mappings U nf δ from δ to P(δ) and U nf C from C to P(C) are defined by:

  , (γ, α, e 1 , . . . , e n ) ∈ W -(p, t) such that γ(c t ) = true and ∀c p = c p,1 , . . . , c p,n ∈ m(p), m(p)(c p ) < α or ∃i ∈ [1..n] | e i (c t ) / ∈ { , c p,i } then {(p, e 1 (c t ), . . . , e n (c t ) )} else {(p, c p ) | p ∈ • tand ∃(γ, α, e 1 , . . . , e n ) ∈ W -(p, t) such that c p = e 1 (c t ), . . . , e n (c t ) and γ(c t ) = f alse and ¬(∀i ∈ [1..n], e i (c t ) =

	and m(p)(c p ) ≥ Γ (W -(p, t)))}

Table 1 .

 1 Data collected for some models extracted from concurrent software

			Complete Graph		Reduced Graph
			|N |	|A|	T	|N |	|A|	T
				The leader election protocol
		7	198 039	1 041 750	61	45 780	93 361	30
		8	1 037 209	6 175 069	644	201 943	430 120	184
		9	5 961 241	40 179 197	10 035	824 362	2 061 193	1 038
				The dining philosophers (first implementation)
		7	1 398 615	5 050 508	138	29 412	44 166	4
	5	8 9	5 416 243 24 842 432	21 585 453 112 433 417	1 038 13 581	83 670 221 865	127 191 319 833	14 40
				The dining philosophers (second implementation)
		4	26 539	55 245	1	6 322	7 667	1
		5	219 304	505 765	11	37 139	46 911	7
		6	1 789 459	4 582 322	145	214 853	359 901	43
				The client / server program
		2	4 141	14 461	1	108	131	0
		3	130 221	593 583	14	1 131	1 434	0
		4	5 445 681	30 593 745	2 508	13 921	19 232	1

Complete Graph), the second with it (column Reduced Graph). The columns |N |, |A|, and T indicate for each run the number of nodes and arcs of the graph, and the exploration time of the graph in seconds.

Table 2 .

 2 Data collected for some academic models

			Helena					Prod
	Complete Graph		Reduced Graph		Reduced Graph
	|N |	|A|	T	|N |	|A|	T	|N |	|A|	T
			The resource allocation system
	2 550 759 11 435 684 49	72 637	100 925	2	72 637 100 925	7
		The distributed database system (from [11])
	649 540 4 330 282 19	67 585	112 662	1	232	242	0
			The dining philosophers
	1 153 351 10 416 483 34	602 493 2 131 338 18	265 143 616 555 41
		Eisenberg and McGuire's mutual exclusion algorithm
	624 790 2 490 418	9	414 555 1 345 417 129	223 482 428 297 491
			The distributed Sieve of Eratosthenes
	2 028 969 9 947 808 59	273	272	0	Net not unfoldable
		Lamport's fast mutual exclusion algorithm (from [12]
	1 672 728 7 944 684 41	959 494 3 176 750 188	197 554 338 504 58
		Chang and Roberts leader election protocol
	218 931 1 836 299	7	156 254	799 871 26	123 979 212 531 51
			The load balancing system
	9 324 768 54 723 965 295	275 090	499 615 11	252 458 477 487 867
			The multiprocessor system (from [4])
	7 322 076 85 522 635 356	138 239	283 646 76	138 239 283 646 572
			Peterson's mutual exclusion algorithm
	1 242 528 4 970 112 19	186 037	386 272 46	80 193 152 565 38
			The slotted ring protocol (from [15])
	439 296 2 897 664 11	287 508	97 8514 26	20 613 37 806	2

0 denotes here the empty mapping from C(t) to Bag(C(p)), i.e., ∀c ∈ C(t), 0(c) = ∅.