Roza Szweda

Michel Tschopp

Olivier Felix

Gero Decher

Jean-François Lutz

Sequences of Sequences: Spatial Organization of Coded Matter through Layer-by-layer Assembly of Digital Polymers

Keywords: data storage, digital materials, information-containing macromolecules, layer-bylayer, sequence-controlled polymers

A library of 16 digitally encoded polyanions was used in a layer-by-layer (LbL) polyelectrolyte assembly to nanofabricate thin films containing digitally coded strata. The polyanions were digital polyphosphodiesters (d-PPDE) prepared via an automated phosphoramidite process. Each component of the library contained 10 bytes of ASCII-encoded text (i.e. 80 coded monomers); thus the entire library allows the writing of a full sentence, which can be stored in a multilayer film as a sequence of sequences. To prepare fully segregated digital domains, non-coded layers composed of poly(allylamine hydrochloride) (PAH)/poly(sodium 4styrenesulfonate) (PSS) were included between the d-PPDE coded layers as an intermediate barrier. Detailed analysis of the film homogeneity indicated formation of 70 nm-thick films in which digital layers are kept apart from another by non-coded interlayers. As a result, the sequence-coded polymer library could be piled-up in a defined sequence of layers.

It was shown in recent years that the monomer sequence of copolymers can be used to store information. [1] Polymers having such a property are called information-containing macromolecules,[1b] or more specifically digital polymers when they store digital information. In DNA, for example, the four nucleotides of the genetic alphabet can be used to write binary messages, as shown in several recent reports.[2] Alternatively, molecular information can be encrypted in the comonomer sequence of non-biological polymers.[3] The information stored inside the polymer chains can be recovered using a sequencing technique, such as highthroughput Illumina sequencing, nanopore sequencing, or tandem mass spectrometry.[4] Some strategies for erasing or rewriting coded monomer sequences have also been reported. [3c, 5] Thus, it is now clearly demonstrated that information sequences can be stored, manipulated, and retrieved at the single-polymer-chain level. Yet, beyond these interesting discoveries, there is currently very little research about the spatial organization of man-made coded matter. In the bulk, digital polymers contain a very large amount of uniform chains having all the same sequence-encoded message. However, potential applications of these polymers, for example, data storage, will probably require the development of organized polymer libraries in which a piece of information can be stored in a defined region of space. For nucleic acids memories, commercial DNA microchips are usually purchased and used as such, [2a,c] which is easy but probably not an optimal solution. Indeed, modern materials science offers many other opportunities to organize soft matter at the nanoscale. For instance, the 2D or 3D organization of digital polymer libraries could be attained via surface patterning, directed self-assembly, co-crystallization, layer-by-layer (LbL) deposition, or by a combination of some of these approaches.

In this context, we report herein the LbL preparation of multilayered thin films containing segregated digital domains. During the last two decades, the LbL process has been shown to be an extremely simple and versatile platform for preparing structured nanomaterials. [6] In the original version of it, oppositely charged polyelectrolytes (that is, polyanions and polycations) are repeatedly deposited on a charged substrate with a nanometer precision to form a thin film containing alternating polyanion/polycation layers. However, the LbL concept has been afterwards extended to many other types of associating polymers and materials, [START_REF] Seyrek | Polymer Science: A Comprehensive Reference[END_REF] thus enabling preparation of a broad variety of nanostructured materials including colloids, organic/inorganic composites and bio-hybrid structures.[8] Furthermore, the deposition process can be facilitated through the use of automated dipping, spin-or spray-assisted assembly.

[9] Yet, although it was already realized in the early days of LbL-assembly that a given sequence of different dipping solutions leads to a unique layer sequence,[6a,10] many people in the field continued to prepare LbL-films containing only two components in strictly alternating fashion. In the present work, a library of digitally encoded polyelectrolytes was used to our knowledge for the first time for the fabrication of LbL films in which each digital layer contains a different piece of coded information (Figure 1). In other words, the information stored in these materials is determined by the monomer sequence of a given digital polymer in a given layer but also by the sequential arrangement of the coded layers in the entire film. The formation of such a "sequence of sequences" was studied herein using ellipsometry, atomic force microscopy (AFM), and X-ray photoelectron spectroscopy (XPS). Digital polyphosphodiesters (d-PPDE) were selected in the present work as coded polyanions. As recently described,[3b] these polymers are obtained via a solid-phase phosphoramidite chemistry approach in which two different phosphoramidite monomers are used as a binary alphabet (Figure 1a). Following previously established conventions, monomers containing a propyl and a 2,2-dimethylpropyl spacer are defined as 0-and 1-bit, respectively. [11] Thus, the synthesis and sequencing of long digital polyphosphodiesters has been previously demonstrated.

[12] Herein, a library of 16 different d-PPDEs was synthesized. This library encodes a citation from the French chemist Marcellin Berthelot: "La chimie crée son objet. Cette faculté créatrice, semblable à celle de l'art lui-même, la distingue essentiellement des sciences naturelles et historiques." (Supporting Information, Figure S1). [START_REF] Berthelot | La Synthèse Chimique[END_REF] This sentence contains 160 characters, including spaces and quotation marks. Thus, using extended ASCIIencoding, it was decomposed into 16 different polymers P1-P16 containing each 10 bytes of information (Supporting Information, Table S1; Figure 1a).[14] Each polymer contained therefore 81 monomers, that is, 80 binary monomers (one byte of information corresponds to 8 monomers) and one thymidine nucleoside (T) coming from the porous glass solid support. All these polymers were synthesized on an automated synthesizer and their structural uniformity was assessed by HPLC (Supporting Information, Figure S2a) and NMR (Supporting Information, Figure S3). Furthermore, two homopolymers H0 and H1 with the same chainlength as the copolymers of the library but containing only 0 or 1 units were synthesized and characterized (Supporting Information, Figures S2b andS3). The LbL assembly process was first studied with the model homopolyanions H0 and H1, using poly(allylamine hydrochloride) (PAH) as a counter-polycation (Figure 1b). These first experiments were performed to assess the influence of the nature of the coded monomer on film formation. Another important aspect of the present work was to avoid non-linear LbL growth, which has already been observed with some polyphosphates. [START_REF] Cini | [END_REF] Indeed, superlinear growth leads to an enhanced diffusion process and therefore to the migration of polyelectrolyte between layers. [16] Such a behavior would not be ideal for the present study in which coded digital layers should be completely segregated from another. Thus, H0 and H1 were first studied to identify experimental conditions, in which the films grow homogenously and linearly. The polyelectrolyte films were constructed on a modified silicon wafers by a manual dipping method and their growth was followed by ellipsometry (Supporting Information, Figure S4). First, a simple alternating process (Route 1 in Figure 1c) was investigated in which a PAH cationic layer was added in between each d-PPDE layer. These experiments showed that the molecular structure of the homopolymers has an influence on LbL growth and on the properties of the resulting films. When using H0 as a polyanion (Supporting Information, Figure S4a), LbL growth followed a linear regime for all investigated concentrations. For instance, after depositing 10 PAH/H0 layers at a polyelectrolyte concentration of 0.04%, thin films with an overall thickness of 5 nm and a root-mean-square (RMS) roughness of 1.1 nm were obtained. In contrast, a superlinear growth was observed for films prepared with H1 (Supporting Information, Figure S4b). [START_REF] Porcel | For detailed information about linear and superlinear growth in LbL assembly[END_REF] After 10 PAH/H1 depositions at a concentration of 0.04%, ellipsometry evidenced formation of films with an overall thickness of 38 nm, thus suggesting extended and well-hydrated structures, in which chain migration between layers might occur. [16,[START_REF] Porcel | For detailed information about linear and superlinear growth in LbL assembly[END_REF] Film inhomogeneity was confirmed by AFM measurements, which indicated an RMS roughness of about 5.7 nm. These results underline that, despite the small structural differences between monomers 0 and 1 (that is, two protons instead of two CH3 groups), the composition extremes found in H0 and H1 lead to different LbL behaviors. Furthermore, when H0 and H1 were both mixed in the same film (Supporting Information, Figure S5), non-linear growth was still observed, thus confirming the dominating role of H1.

To minimize these discrepancies, a second deposition strategy (Route 2 in Figure 1c) was investigated with H0 and H1. In this approach, a complementary polyanion, poly(sodium 4styrenesulfonate) (PSS) was also used (Figure 1b), thus enabling to include non-coded PSS/PAH interlayers between coded d-PPDE layers. PSS was chosen as a copolyanion because PSS/PAH is a widely investigated and well understood polyelectrolyte pair in the LbL field.[6a, 9c] XPS measurements that were performed on model surfaces, on which PSS, PAH, and a d-PPDE homopolymer were successively deposited are shown in the Supporting Information, Figure S6. These results show that H0 and H1 can be deposited on PSS/PAH interlayers. Furthermore, when inserting one PSS interlayer between two d-PPDE layers (that is, using a four-step deposition cycle as shown on Figure 1b), a linear growth was observed with both homopolymers H0 and H1 (Supporting Information, Figure S7). For instance, after performing 10 cycles, both homopolymers led to comparable film having a thickness of 45 nm and a RMS roughness of 2 nm. Hence, Route 2 prevents non-linear LbL growth and was therefore selected for the preparation of digital multilayers. The digital multilayers were first prepared by a conventional dipping LbL process as shown on Figure 2a.[6a] Following Route 2, a four-step PSS/PAH/d-PPDE/PAH deposition cycle was used. Consequently, 63 consecutive layers were deposited to include the 16 coded polyanions P1-P16 of the d-PPDE library (Supporting Information, Table S1). The sequence of coded layers was arbitrarily arranged from the top to the bottom of the film. In other words, d-PPDE deposition started with P16 and finished with P1 (that is, following the reverse order of Table S1). The LbL dipping approach was first performed manually to carefully study film formation. Yet, an important aim of the present work was to demonstrate that the preparation of digital films can also be automated. Thus robotic LbL dipping was also studied and compared to the manual approach. In both cases, similar polyelectrolyte deposition protocols were used. Figure 2a shows the evolution of film thickness determined by ellipsometry as a function of the number of deposited d-PPDE layers for both manual and robotic dipping approaches. As previously observed with homopolymers H0 and H1, a linear growth was observed in all cases. It shall be specified that the molar fraction F0 of comonomer 0 in copolymers P1-P16, is in a range 0.46-0.63 (Supporting Information, Table S1), which is intermediate as compared to the previously studied extremes H0 and H1. It is therefore expected that copolymers follow a similar LbL trend as homopolymers, even though a defined sequence of layers was created using P1-P16. Furthermore, the film thicknesses measured by ellipsometry at all stages of the LbL growth were similar for manual and robotic approaches, thus confirming that automated deposition can be safely employed to prepare digital films. Altogether, the ellipsometry results of Figure 2a suggest that there is limited polyelectrolyte diffusion between layers and that d-PPDE are physically segregated from another. This assumption was further supported by the AFM analysis of film morphology (Figure 2b,c; Supporting Information, Figure S8a). The manual and robotic LbL protocols led to final films (that is, films containing 63 polyelectrolyte layers including 16 d-PPDE coded layers) of similar morphology with comparable RMS roughness values of 2 and 1.8 nm, respectively. The slightly lower RMS value obtained for the robotic protocol may be explained by its more precise sample treatment, eliminating unnecessary manipulations and reducing the probability of scratches or other film damage. For both manual and robotic approaches, the film morphologies appeared homogenous for the whole area studied by AFM, which is in agreement with the small thickness error values estimated by ellipsometry. Furthermore, AFM "scratching" (Figure 2c; Supporting Information, Figure S8a) was used to measure final film thickness. For instance, for the digital films prepared via the robotic approach (Figure 2c), an overall thickness of 70 nm was measured, which is in good accordance with the ellipsometry estimations (75 nm). Hence, the AFM data suggest a controlled inter-distance of about 3 nm between each d-PPDE layer. If needed, this distance can be, of course, enlarged by increasing the number of PSS/PAH non-coded interlayers. The fabrication of digital multilayers was also investigated using spin-assisted deposition, which is an efficient method for facilitating deposition and reducing preparation times.[9b] The films were formed by sequentially dropping polyelectrolyte and rinsing solutions on a modified silicon wafer placed on a spinning unit (Figure 2d,top). Route 2 (Figure 1c) was used to form the multilayers and a short spinning time of 30 s was used for each polyelectrolyte deposition. The LbL deposition was studied at different rotational speeds (1000, 3000, and 5000 rpm). As evidenced by ellipsometry monitoring (Figure 2d, bottom), all resulting films showed linear growth. However, the spinning speed influenced the thickness, homogeneity and roughness of the resulting materials. First of all, overall film thickness increased with decreasing rotational speed, which is due to a longer contact time between polyelectrolyte solution and substrate at slow rotation rates. Regarding film homogeneity, a fast spinning rate (5000 rpm) led to a marked decrease of film thickness at the central point of the sample due to the limited contact time of the polyelectrolyte solution at the midpoint of the substrate. On the other extreme, the use of a slow spinning rate (1000 rpm) results in a poor spreading of polyelectrolyte solutions on the substrate and therefore in the formation of nonhomogeneous films (see errors bars in Figure 2d). Optimal results were obtained with an intermediate spinning speed of 3000 rpm, at which rotation was fast enough to homogenously distribute the polyelectrolyte solutions while maintaining comparable solution-surface contact time over the entire surface area. At this rate, homogenous films with a RMS roughness of only 1.4 nm were obtained (Supporting Information, Figure S8). Thus, spinassisted LbL assembly is a suitable approach for the preparation of digital multilayers. Furthermore, this method is overall much faster than dipping approaches. Indeed, the fabrication of thin films containing 16 coded d-PPDE layers required about 1 h by spin-assisted deposition, whereas it takes about one day by dipping. Yet, the formed films are thinner (40 nm at 3000 rpm) than those prepared by the dipping approach and therefore the interdistance between two coded layers is only of about 2 nm. Of course, as pointed out above, this distance could likely be increased by the use of additional PSS/PAH layers. In summary, thin films containing segregated layers of digitally encoded polymers were prepared by LbL and characterized. An ASCII-encoded sentence of 160 bytes was stored in these films using a library of 16 different digital polyanions. The storage multilayers were prepared using various LbL methods such as manual dipping, robotic dipping, and spinassisted deposition. All three approaches allowed synthesis of thin films with controlled thickness, roughness, and morphology. However, it was found in this work that the use of noncoded PSS/PAH intermediate layers is mandatory to isolate efficiently coded digital layers from another. Overall, this work opens up very interesting new avenues in fundamental and applied polymer science. From a fundamental point of view, the present results highlight for the first time that abiotic coded matter can be organized in precise nanoscale morphologies. Moreover, the formation of a "sequence of sequences" increases coding possibilities in synthetic materials. For instance, out of the 16 16 possible multilayers that could have been created using a set of 16 digital polymers in 16 coded layers, only the sequence reported here gives access to Berthelot's quote (assuming film directionality). Regarding potential applications, the strategies described here could be relevant for the development of molecular archives and other data storage applications. For instance, the combination of 2D patterning (x-y organization) with LbL growth (z-organization) could lead to storage materials with unprecedented storage densities. Yet, digital polymers have been barely studied in materials science and nanotechnology so far and many scientific aspects still have to be addressed. For instance, the development of sequencing methods allowing spatial decoding of coded libraries is an exciting new challenge in polymer analytics. In the case of digital LbL films, decoding could be achieved using depth profiling mass spectrometry methods such as time-of-flight secondary ion mass spectrometry (TOF-SIMS) or desorption electrospray ionization (DESI). [18] ASSOCIATED CONTENT

Supporting Information

Full experimental part: detailed experimental procedures. Supplementary Figures S1-S7.

Figure 1 .

 1 Figure 1. General strategy studied in this work for the preparation of digital multilayers. a) Synthesis of a library of sequence-coded polyanions by solid-phase phosphoramidite chemistry. Experimental conditions: i) phosphoramidite coupling: RT, acetonitrile, tetrazole; ii) oxidation: RT, I2, pyridine, THF/H2O; iii) capping: RT, acetic anhydride, N-methylimidazole; iv) DMT deprotection: CCl3-COOH; CH2Cl2; v) cleavage: MeNH2, NH4OH, H2O, RT. The blue square on the right side represents a porous glass solid support. The decabyte monomer sequences of the homopolymers (H0 and H1) and copolymers (P1-P16) synthesized in this work are listed on the right. b) Molecular structures of non-coded polyanions and polycations that were used in the layer-by-layer process. c) Preparation of digital multilayers. Route 1: alternating deposition of coded d-PPDE (red) and noncoded PAH (blue). Route 2: four-step PSS/PAH/d-PPDE/PAH deposition cycle.

Figure 2 .

 2 Figure 2. Characterization of digital multilayers prepared by dipping and spin-assisted LbL approaches. a) top: representation of the dipping protocol (route 2, Figure 1c); bottom: ellipsometry monitoring of film thickness for multilayers prepared by either manual (•) or robotic (○) LbL dipping. The studied films contained 16 coded d-PPDE layers (Supporting Information, Table S1); that is, 63 layers in total. Ellipsometry measurements were made after each d-PPDE deposition. The error bars represent standard deviation values of three independent measurements performed at different surface points. b) AFM characterization of the surface morphology of the final film prepared by robotic dipping. The size of AFM images is 1.5×1.5 mm and Z scale is 15 nm. c) AFM cross-section measured for the final film obtained by robotic dipping. d) top: representation of the spin-assisted assembly protocol (route 2, Figure 1c); bottom: ellipsometry monitoring of film thickness for films prepared spin-assisted LbL assembly at different rotational speeds. The films contained 16 d-PPDE layers and the ellipsometry measurements were made after each d-PPDE deposition. Errors bars were estimated as in (a).

ACKNOWLEDGMENT

J.F.L. thanks the H2020 program of the European Union (project Euro-Sequences, H2020-MSCA-ITN-2014, grant agreement no. 642083) and the CNRS for financial support. The authors thank Pierre Schaaf (Inserm 1121, Strasbourg) for the access to the AFM.

AUTHOR INFORMATION

Corresponding Author

Jean-François Lutz, E-mail: jflutz@unistra.fr Gero Decher, E-mail: decher@unistra.fr

Digital polyanions (coded matter)

Intermediate layers (non-coded matter)


Aleksandra Jovanovic

Didier Lime

Olivier H Roux

Aleksandra Jovanović

Control of Real-time Systems with Integer Parameters

Keywords: Timed Automata, Control, Game Theory, Parameters, Synthesis

published or not. The documents may come

I. INTRODUCTION

Designing real-time systems is a challenging issue and formal models and reasoning are key elements in attaining this objective. In this context, timed automata (TA) [START_REF] Alur | A Theory of Timed Automata[END_REF] are a powerful and popular modeling formalism. They extend finite automata with timing constraints, in which clocks are compared to integer constants that model timing features of the system. This formalism, however, requires complete knowledge of the system. It is thus difficult to use it in early design stages when the whole system is not fully characterized. Even when all timing constraints are known, if the environment changes or the system is proven wrong, the whole controller synthesis process must be carried out again. Additionally, considering a wide range of values for constants allows for a more flexible and robust design.

Parametric reasoning is, therefore, particularly relevant for timed models, since it allows designers to use parameters instead of concrete timing values.

Parametric timed automata [START_REF] Alur | Parametric real-time reasoning[END_REF] extend timed automata [START_REF] Alur | A Theory of Timed Automata[END_REF] to overcome the limits of checking the correctness of the systems with respect to concrete timing constraints. The central problem for verification purposes, reachability-emptiness, which asks whether there exists a parameter valuation such that the automaton has an accepting run, is undecidable [START_REF] Alur | Parametric real-time reasoning[END_REF]. This naturally led to the search for subclasses of the formalism for which some problems would be decidable. L/U automata [START_REF] Hune | Linear parametric model checking of timed automata[END_REF] use each parameter either as a lower bound or as an upper bound on clocks. The reachability-emptiness problem is decidable for this model, but state-space exploration, which would allow for explicit synthesis of all the suitable parameter valuations, still might not terminate [START_REF] Jovanović | Integer parameter synthesis for real-time systems[END_REF].

Control of timed systems.

The introduction of automata-based formalism into the field of control was motivated by the inadequacy of models based on continuous mathematics (differential equations) to describe certain classes of systems. A decision to open a gate or to turn left or right are discrete and most naturally modeled with a finite automaton.

Instead of verifying the correctness of a system, we have here the problem of synthesizing a model for the controller. It consists in computing a controller which, based on the current state of the system, restricts the choices of the system, ensuring that the desired property is satisfied. This problem is often modeled as the synthesis of a winning strategy for the controller in a two-player game against the environment.

More precisely, two players, the controller and the environment, take actions from their own set and thus make the game progress. In each state, both players choose, at the same time and independently of each other, a move (a delay or an action). The next state of the system is then determined from both those actions, possibly non-deterministically.

A formalism that is commonly used to describe such systems in a timed framework is timed game automata (TGA, [START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF]), that explicitly represents the moves of both players, in terms of controllable and uncontrollable edges. They are extended timed automata that distinguish between the actions of the two players, describing at the same time both the controller and the environment.

The (reachability) control problem for TGA is the problem of determining the strategy for the controller such that, no matter what the environment does, the system ends up in the desired location. This problem is known to be decidable [START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF]. The introduction of this formalism has been followed by the development of efficient algorithms [START_REF] Cassez | Efficient onthe-fly algorithms for the analysis of timed games[END_REF] and tool support [START_REF] Behrmann | Uppaal-tiga: Time for playing games![END_REF], successfully applied to several industrial case studies (e.g. [START_REF] Cassez | Automatic synthesis of robust and optimal controllers -an industrial case study[END_REF], [START_REF] Jessen | Guided controller synthesis for climate controller using uppaal tiga[END_REF]).

Control of Parametric timed systems.

In [START_REF] Jovanović | A Game Approach to the Parametric Control of Real Time Systems[END_REF], we have introduced a formalism for timed games extended with parameters, called parametric timed game automata (PGA). In this setting, the most basic problem is: "does there exist values for the parameters such that there exists a controller, such that some control location is reachable whatever the environment does?", which we will call the parametric control problem. As the PGA formalism extends PTA, this problem is undecidable. We have nonetheless extended the backward fixed-point algorithm for solving timed games with reachability objectives of [START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF] to the parametric setting [START_REF] Jovanović | A Game Approach to the Parametric Control of Real Time Systems[END_REF]. This provides a semi-algorithm, which allows to obtain the set of symbolic constraints on the parameters together with the set of winning states for the controller. The termination, however, is not guaranteed.

Our contribution.

We propose to use a restriction scheme proposed in [START_REF] Jovanović | Integer parameter synthesis for real-time systems[END_REF] for PTA: since in classical timed game automata, real-valued clocks are always compared to integers for all practical purposes, we solve undecidability and termination issues by computing parameters as bounded integers. Due to the finite number of parameters values, parameter synthesis can be trivially carried out by an explicit enumeration, but our main contribution is to symbolically compute the resulting set of parameter valuations, without that enumeration. The result is thus given as a symbolic constraint on parameters. The symbolic algorithm is based on the computation of the integer hull of the parametric symbolic states. It builds on the forward exploration of the state-space and backward propagation of winning states of [START_REF] Jovanović | A Game Approach to the Parametric Control of Real Time Systems[END_REF], and adds the integer hull operator there to restrict the explored state space to integer parameters, and ensure termination when they are bounded. Surprisingly, we do not have to apply an integer hull in the backwards computation, in order to obtain the correct integer solution. This saves a lot of computational efforts since that operation is quite expensive.

A preliminary version of this work was published in [START_REF]Synthesis of bounded integer parameters for parametric timed reachability games[END_REF]. The present article develops this work, unifies it with the backward fixed-point semi-algorithm for solving timed games proposed in [START_REF] Jovanović | A Game Approach to the Parametric Control of Real Time Systems[END_REF] and gives full proofs for all the results.

Organization of the Paper.

The rest of the paper is organized as follows. Section II provides definitions about PGA, the problems we are considering, and recalls some negative decidability results. The semialgorithm for computing the whole state-space of a PTA is recalled in Section III. In Section IV we motivate and present a new restriction scheme for the parameter synthesis, we give the complexity of the parametric control problem in this setting, we give the bounded integer parameter synthesis algorithm and we prove its correctness, completeness and termination. We present the execution of the algorithm on an example in Section V and we discuss in section VI the performance of the proposed approach implemented in our tool ROM ÉO, illustrated on a small but realistic case-study. We conclude with section VII. II. PARAMETRIC TIMED GAME AUTOMATA 1) Preliminaries: R is the set of real numbers and R ≥0 is the set of non-negative real numbers. Q is the set of rational numbers. Z the set of integers. Let V ⊆ R. A V -valuation on some finite set X is a function from X to V . We denote by V X the set of V -valuations on X.

Let X be a finite set of variables modeling clocks and let P be a finite set of parameters.

A parametric clock constraint γ is an expression of the form γ ::= x i p | -x i p | γ∧γ, where x i , x j ∈ X, ∈ {≤, < }, and p is a linear expression of the form k 0 +k 1 p 1 +...+k n p n with k 0 , ...k n ∈ Z and p 1 , ...p n ∈ P .

For V ⊆ R, since set X is finite, and given an arbitrary order on its elements, a V -valuation w c on X = {x 1 , . . . , x n } can be seen as the vector (w c (x 1 ), . . . ,

w c (x n )) of R |X| .
The set of valuations on clocks and parameters that satisfy a parametric clock constraint can then be seen as a convex polyhedron of R |X∪P | . We use this remark extensively in the subsequent definitions to consider (parametric) clock constraints as sets.

Let us consider a parametric clock constraint γ. For any parameter valuation w p , we note w p (γ) the linear constraint on clocks obtained by replacing each parameter p i by its value w p (p i ). Similarly, for any clock valuation w c , we note w c (γ) the linear constraint on parameters obtained by replacing each clock x i by its value w c (x i ).

Note that by valuating both parameters and clocks in γ, we obtain w p (w c (γ)) = w c (w p (γ)) that can be seen as a boolean and takes its value in {true, f alse}.

We denote by G(X, P ) the set of parametric constraints over X, and by G (X, P ) a set of parametric constraints over X of the form γ ::

= x i p | γ ∧ γ .
For a valuation w c on X and t ∈ R ≥0 , we write w c + t for the valuation assigning w c (x) + t to each x ∈ X. For R ⊆ X, w c [R] denotes the valuation assigning 0 to each x ∈ R and w c (x) to each x ∈ X\R. Finally, we define the null valuation 0 X on X by ∀x ∈ X, 0 X (x) = 0.

A. Parametric Timed Games

Definition 1: A Parametric Timed Automaton (PTA) is a tuple A = (L, l 0 , X, Σ, P, E, Inv), where L is a finite set of locations, l 0 ∈ L is the initial location, X is a finite set of clocks, Σ is a finite alphabet of actions, P is a finite set of parameters, E ⊆ L × Σ × G(X, P ) × 2 X × L is a finite set of edges, and Inv : L → G (X, P ) is a function that assigns a (parametric) invariant to each location.

If (l, a, γ, R, l ) ∈ E then there is an edge from l to l with action a, (parametric) guard γ and set of clocks to reset R.

For any Q-valuation w p on P , the structure w p (A) obtained from A by replacing each constraint γ by w p (γ) is a timed automaton with invariants (TA) [START_REF] Alur | A Theory of Timed Automata[END_REF], [START_REF] Henzinger | Symbolic model checking for real-time systems[END_REF]. The behavior of a PTA A is described by the behavior of all timed automata obtained by considering all possible valuations of parameters.

Definition 2 (Semantics of a (P)TA): Given a parameter valuation w p , and a PTA A, the concrete semantics of w p (A), is the labeled transition system (Q, q 0 , →) over Σ ∪ R ≥0 where:

• Q = {(l, w c ) ∈ L × R X ≥0 | w c (w p (Inv(l))) is true } • q 0 = {(l 0 , 0 X ) ∈ Q} • delay: (l, w c ) t - → (l, w c + t) with t ≥ 0, iff ∀t ∈ [0, t], (l, w c + t ) ∈ Q • action: (l, w c ) a -→ (l , w c ) with a ∈ Σ, iff (l, w c ), (l , w c ) ∈ Q, there exists an edge (l, a, γ, R, l ) ∈ E, such that w c = w c [R] and w c (w p (γ)) is true.
A finite run of PTA A, for a given a parameter valuation w p , is a sequence of alternating delay and action transitions in the semantics of w p (A), ρ = q 1 a 1 q 2 ...a n-1 q n , where ∀i ∈ [1..n-1], q i ∈ Q, a i ∈ Σ ∪ R ≥0 , and q i a -→ q i+1 . Infinite runs are defined similarly. We denote by Runs(w p (A)) the set of runs starting in the initial state of w p (A), and by Runs(q, w p (A)) the set of runs starting in q. The last state of a finite run ρ is denoted by last(ρ). A state q is said to be reachable in A if there exists a finite run ρ ∈ Runs(w p (A)), such that last(ρ) = q.

We now go one step further and define Parametric Timed Game Automata to model our control problems.

Definition 3: A Parametric (Timed) Game Automaton (PGA) G is a parametric timed automaton with its set of actions Σ partitioned into controllable (Σ c ) and uncontrollable (Σ u ) actions.

As for PTA, for any PGA G and any rational valuation on parameters w p , the structure w p (G), obtained by replacing each constraint γ by w p (γ), is a timed game automaton [START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF], [START_REF] Cassez | Efficient onthe-fly algorithms for the analysis of timed games[END_REF] (TGA). Note that a TGA can also be seen as a PGA with an empty set of parameters.

We formalize our reachability control problem as a timed game, in which the controller player has to reach some distinguished location in a PGA: Definition 4 (Parametric Timed Game): A (reachability) parametric timed game is a pair (G, l goal ) where G is a PGA and l goal is a location of G.

A timed game (i.e. without parameters) is a parametric timed game (G, l goal ) in which G is a TGA.

In a TGA, two players, the controller and the environment, choose at every instant one of the available actions from their own sets, according to their strategy, and the game progresses. Since the game is symmetric, we give only the definition for the controller playing with actions from Σ c . At each step, a strategy tells the controller to either delay in a location (delay), or to take a particular controllable action.

At a given instant, if one player chooses to take an action and the other to delay, then the action is taken. If both choose an action then the result is the non-deterministic choice between the two actions. Finally, if both choose to delay, then nothing happens and we consider the next (different) instant such that one of the player chooses not to delay.

For reachability timed games, one can consider two semantics for uncontrollable actions: either they can only spoil the game and it is up to the controller to do some controllable action to win, or, if at some state s only an uncontrollable action is enabled but forced by time to happen leading to a winning state then, the state s is winning. The usual semantics [START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF], [START_REF] Cassez | Efficient onthe-fly algorithms for the analysis of timed games[END_REF], [START_REF] Asarin | Controller synthesis for timed automata[END_REF] is the first one where uncontrollable actions cannot help to win and is the one we consider in this paper.

Definition 5 (Strategy): A strategy F over w p (G) is a partial function from Runs(w p (G)) to Σ c ∪{delay} such that for every finite run ρ, if F(ρ) ∈ Σ c then last(ρ)

F (ρ)
---→ q for some state q = (l, w c ), and if F(ρ) = delay, then there exists some d > 0 such that for all 0 ≤ d ≤ d, there exists some state q such that last(ρ) d -→ q and F(ρ d -→ q) = delay. Since we focus on control problems for which the control objective (given a parameter valuation) is to reach a particular location of timed automata, [START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF] proves that to win, the controller needs only strategies that are memoryless and constant on regions (as defined in [START_REF] Alur | A Theory of Timed Automata[END_REF]). The former means that for a strategy F and a run ρ, F(ρ) only depends on last(ρ). The latter means that even if players are allowed to choose their actions at any instant, with such a strategy, they will not change their mind until either an action has happened or a sufficient duration has passed that makes one of the clock go from a non-integer value to an integer value, or from an integer value to a non-integer value. We assume nothing on the strategies of the environment.

Outcome defines the restricted behavior of w p (G), when the controller plays some strategy F, with respect to all the possible strategies of the environment.

Definition 6 (Outcome): Let G be a PGA, w p be a parameter valuation, and F be a strategy over w p (G). The outcome Outcome(q, F) of F from state q is the subset of runs in Runs(q, w p (G)) defined inductively as:

• the run with no action q ∈ Outcome(q, F)

• if ρ ∈ Outcome(q, F) then ρ = (ρ δ - -→ q ) ∈ Outcome(q, F) if ρ ∈ Runs(q, w p G))
and one of the following three condition holds:

1) δ ∈ Σ u , 2) δ ∈ Σ c and δ = F(ρ), 3) δ ∈ R ≥0 and ∀0 ≤ δ < δ, ∃q ∈ S s.t. last(ρ) δ - -→ q ∧ F(ρ δ - -→ q ) = delay.
• for an infinite run ρ, ρ ∈ Outcome(q, F), if all the finite prefixes of ρ are in Outcome(q, F).

As we are interested in reachability games, we consider only the runs in the outcome that are "long enough" to have a chance to reach the goal location: a run ρ ∈ Outcome(q, F) is maximal if it is has an infinite number of action transitions or there is no delay d and no state q such that ρ = (ρ d --→ q ) ∈ Outcome(q, F) and F(ρ ) ∈ Σ c (the only possible actions from last(ρ) are uncontrollable actions). MaxOut(q, F) denotes the set of maximal runs for a state q and a strategy F.

Definition 7 (Winning strategy, state, game): Let G = (L, l 0 , X, Σ c ∪ Σ u , P, E, Inv) be a PGA and (G, l goal ) a parametric timed game. Let v be a parameter valuation.

A strategy F in the non-parametric game (w p (G), l goal ) is winning from state q if for all runs ρ ∈ MaxOut(q, F), there is some state (l goal , w c ) in ρ.

A state q is winning if there exists a winning strategy from q.

The timed game (w p (G), l goal ) is winning if its initial state is winning.

The parametric timed game (G, l goal ) is winning if there exists some parameter valuation w p such that (w p (G), l goal ) is winning.

In the non-parametric case, the (reachability) control (resp. synthesis) problem is that of the existence (resp. computation) of a strategy such that, no matter what happens in the environment, the system ends-up in the desired location (for short we say this location is enforceable). The control problem is known to be decidable [START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF] and there exists efficient symbolic algorithms for the computation of winning states and strategies [START_REF] Cassez | Efficient onthe-fly algorithms for the analysis of timed games[END_REF]. We now extend these problems to account for parameters. The emptiness problem for PTA, i.e. the existence, for a PTA A, of a parameter valuation v such that some location is reachable in w p (A) is undecidable [START_REF] Alur | Parametric real-time reasoning[END_REF]. Now remark that in a game in which all transitions are controllable, we trivially have that there exists a winning strategy for the controller to enforce the reachability of some location if and only if that location is reachable. We can therefore check the reachability problem using the control problem, and the following theorem holds:

Theorem 1 ( [START_REF] Jovanović | A Game Approach to the Parametric Control of Real Time Systems[END_REF]): The parametric control problem for PGA is undecidable.

We have proposed in [START_REF] Jovanović | A Game Approach to the Parametric Control of Real Time Systems[END_REF] subclasses of PGA, for which the parametric control problem is decidable. These classes are however severely restricted in their use of parameters. These restrictions are inspired by those defining L/U automata, which to the best of our knowledge are yet the less restrictive subclass of PTA for which the parametric control problem is decidable. Since PGA extend PTA there is little hope that we can do much better than L/U games in terms of syntactic subclasses. Also, even the L/U restriction is not enough in general to ensure the termination of the computation of the whole parametric state-space.

To solve this problem without heavy syntactic restrictions, we have propose (as in [START_REF] Jovanović | Integer parameter synthesis for real-time systems[END_REF]) to restrict the problem of parameter synthesis to the search for bounded integer parameter values. This makes all the problems decidable, since we can enumerate all the possible valuations.

Lifting either one of the two assumptions (boundedness or integer) leads to undecidability [START_REF] Jovanović | Integer parameter synthesis for real-time systems[END_REF].

To avoid an explicit enumeration of all the possible values of parameters we will propose an efficient symbolic method to find the solution. This has the additional advantage of giving the set of parameter valuations as a symbolic constraint between parameters. As a consequence to this negative result we now investigate restrictions to the PGA formalism to make the control problem decidable.

III. A SYMBOLIC STATE SPACE ABSTRACTION OF PARAMETRIC TIMED GAMES

For timed reachability games, a winning strategy for the controller can be synthesized using a well-known backward fixed-point algorithm for solving timed games [START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF]. The algorithm is based on the time and action predecessor operators [START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF], [START_REF] Alfaro | Symbolic algorithms for infinite-state games[END_REF], that compute the set of winning states, starting from the goal location. In [START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF], the authors only use a backwards computation. In order to extend this algorithm to the integer parametric case, we need to compute forward the whole reachable state space, then compute backwards the winning states.

In this section, we present the forward computation of the state space w.r.t. our bounded integer approach.

A. State space of a PGA

In order to represent the infinite state space of PGA, we need an abstraction. We use here an extension of the classical symbolic states abstraction of TA and TGA [START_REF] Larsen | Model-Checking for Real-Time Systems[END_REF].

Definition 8 (Parametric symbolic state): A symbolic state of a parametric timed (game) automaton G, with set of clocks X and set of parameters P , is a pair (l, Z) where l is a location of A and Z is a set of valuations v on X ∪ P .

Given a valuation v on X ∪ P , we define its projection v |P on P as the restriction of v to P such that v |P (x) = v(p) for all p ∈ P . We define similarly the projection v |X on X.

Given a set Z of valuations on X ∪ P and v a valuation on

X ∪ P , we define v |P (Z) = {v |X |v ∈ Z and v |P = v |P }. The definition of v |X (Z) is symmetric.
Given an arbitrary order on clocks and variables, their Rvaluations can be seen as points in the |X ∪ P |-dimensional space R |X∪P | . Valuation sets that be reached by a given sequence of edges can be represented by convex polyhedra [START_REF] Jovanović | Integer parameter synthesis for real-time systems[END_REF].

For the computation of the state space, we define the following parametric extensions of the classical operations on valuation sets [START_REF] Jovanović | Integer parameter synthesis for real-time systems[END_REF]:

• future: Z = {v | ∀p ∈ P, v (p) = v(p) and ∀x ∈ X, v (x) = v(x) + d, d ≥ 0}; • reset of the clock variables in set R ⊆ X: Z[R] = {v[R] | v ∈ Z}.
We also need the following operators on symbolic states.

• initial symbolic state of PTA A = (L, l 0 , Σ, X, P, E, Inv): Init(A) = (l 0 , {v ∈ R X∪P | v |X = 0 X } ∩ Inv(l 0 ); • successor by some edge e = (l, a, γ, R, l ): Succ((l, Z), e) = (l , (Z ∩ γ)[R] ∩ Inv(l ))
Valuations in the initial symbolic states must be such that all clocks are initially equal to 0 and then we saturate with delay while the invariant is satisfied.

For the symbolic successor, we take valuations that satisfy the guard, then we apply resets, and finally we saturate with delay while the invariant is satisfied.

We extend the Succ operator to arbitrary sets of states by defining, for any set of states S and any location l, the subset S l of S containing the states with location l. S l is therefore a symbolic state (l, Z) for some set of valuations Z. Then we define Succ(S, e) as Succ(S l , e), with l being the source location of edge e.

From [START_REF] Jovanović | A Game Approach to the Parametric Control of Real Time Systems[END_REF], we know that the reachable state-space of the PGA G can then be computed by the following fixed-point (when it exists):

S 0 = ∅ and S n+1 = Init(G) ∪ e∈E Succ(S n , e)
The final fixed-point set is noted S * . The obvious problem with this approach is that the fixedpoint computation of S * might not terminate.

We now restrict the problem of parameter synthesis to the search for bounded integer parameter values. To avoid an explicit enumeration of all the possible values of parameters, and following the approach of [START_REF] Jovanović | Integer parameter synthesis for real-time systems[END_REF], we now modify the symbolic computation of S * so that it still preserves the integer parameter valuations.

B. Integer points and integer hulls

For the sake of the simplicity of the presentation, we henceforth consider that all polyhedra representing valuation sets over X ∪P are topologically closed, i.e., all the constraints describing them are non-strict. We invite the reader to refer to [4, Section IV.C] for the explanation of how to compute the integer hull for non-necessarily closed polyhedra.

Let V be a set such that Z ⊆ V . A V -valuation on some set Y is an integer valuation if ∀x ∈ Y, v(x) ∈ Z. Given a set Z of V -valuations, we denote by IntVects(Z) the set of integer valuations in Z.

The convex hull of a set Z of V -valuations, denoted by Conv(Z), is the intersection of all the convex sets of Vvaluations that contain Z.

The integer hull of a set Z of V -valuations, denoted by IH(Z) is defined as the convex hull of the integer valuations in Z:

IH(Z) = Conv(IntVects(Z)).
If D is not convex, then IH(D) can contain strictly more integer valuations than D. Yet, if D can be expressed as a finite union of convex sets D = i Z i , then we can define an extension of the integer hull, which we call integer shape, by IS(D) = i IH(Z i ). We then have an important property:

IntVects(IS(D)) = IntVects(D).

C. (Bounded) Integer parameter state space

For the computation of S * , as in [START_REF] Jovanović | Integer parameter synthesis for real-time systems[END_REF] for the algorithm for the reachability-synthesis for PTA, we now replace all the occurrences of operator Succ with ISucc((l, Z), e) = IH(Succ((l, Z), e)).

The reachable integer parameter state-space of the PGA G can then be computed by the following fixed-point

S 0 = ∅ and S n+1 = Init(G) ∪ e∈E ISucc(S n , e)
The final fixed point is noted IS * .

It is easy to see, that all the symbolic states computed by Succ (and therefore ISucc) have convex valuations sets that can actually be represented by convex polyhedra. Actually, as shown in [START_REF] Hune | Linear parametric model checking of timed automata[END_REF], these polyhedra have a special form, called parametric zone, that has the important following property: for any integer parameter valuation, the polyhedron obtained by replacing the parameter variables in the parametric zone by their values is a convex polyhedron on clock variables (usually called zone) with integer vertices (see [START_REF] Jovanović | Integer parameter synthesis for real-time systems[END_REF], Property 3). Therefore, by using the ISucc instead of Succ in the computation of the whole state-space S * , we ensure termination and obtain a subset IS * of S * such that IntVects(IS * ) = IntVects(S * ), provided we know a bound on the possible values for the parameters (from which we can derive a bound on the values of the clocks, see [START_REF] Jovanović | Integer parameter synthesis for real-time systems[END_REF]).

IV. INTEGER PARAMETER SYNTHESIS FOR CONTROL

The well-known backward fixed-point algorithm for solving timed games [START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF] is based on the time and action predecessor operators [START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF], [START_REF] Alfaro | Symbolic algorithms for infinite-state games[END_REF], that compute the set of winning states, starting from the goal location.

In this section, we will apply our bounded integer approach to parameter synthesis for parametric timed games, and show that surprisingly we do not have to apply the integer hull computation when back propagating the winning states.

We first recall some results of [START_REF] Jovanović | A Game Approach to the Parametric Control of Real Time Systems[END_REF] on the parametric time and action predecessor operators, and their use in devising a semi-algorithm to solve parametric reachability games.

A. A semi-algorithm to solve parametric reachability games

For the backward computation of winning states, we need the following operators:

• past: Z = {v | ∃v ∈ Z s.t. ∀p ∈ P, v (p) = v(p) and ∀x ∈ X, v (x) = v(x) -d, d ≥ 0} • inverse reset of clocks in set R ⊆ X: Z[R] -1 = {v | ∃v ∈ Z s.t. ∀p ∈ P, v (p) = v(p) and ∀x ∈ X, v(x) = 0 if x ∈ R and v (x) = v(x) if x ∈ R} • predecessor by edge e = (l, a, γ, R, l ): Pred((l , Z), e) = (l, Z[R] -1 ∩ γ ∩ Inv(l)).
The predecessor by an edge operation is extended by union to define controllable and uncontrollable action predecessors (predecessors by edge):

• controllable predecessors: cPred((l , Z)) = c∈Σ c Pred((l , Z), c) • uncontrollable predecessors: uPred((l , Z)) = u∈Σ u Pred((l , Z), u)
We also need to define a safe-timed predecessors (Pred t ) operator. Let S 1 , S 2 ⊆ S, both having the same location, and where S is the set of states in the semantics of a PGA. A state (l, v) ∈ S is in Pred t (S 1 , S 2 ) if from (l, v) we can reach (l, v ) ∈ S 1 by time elapsing and along the path from (l, v) to (l, v ) avoid S 2 , formally:

Pred t (S 1 , S 2 ) = {(l, v) | ∃d ≥ 0 s.t. (l, v) d -→ (l, v ), (l, v ) ∈ S 1 and P ost [0,d] (l, v) ⊆ S\S 2 } where P ost [0,d] (l, v) = {(l, v ) ∈ S | ∃t ∈ [0, d] s.t. (l, v) t - → (l, v ), v (x) = v(x) + t, if x ∈ X; v (x) = v(x) if x ∈ P } is the future operator limited to a maximum time elapsing of d time units.
This corresponds intuitively to the states that can reach S 1 by delay, without going through any state in S 2 along the path. Safe-timed predecessor operator can also be expressed as follows:

Lemma 2 ( [6]): For any two symbolic states S 1 and S 2 , such that S 2 is convex:

Pred t (S 1 , S 2 ) = (S 1 \S 2 ) ∪ ((S 1 ∩ S 2 )\S 2 )
Also, the following distribution law holds: Lemma 3 ( [START_REF] Cassez | Efficient onthe-fly algorithms for the analysis of timed games[END_REF]): For any two symbolic states S 1 = i S 1i and S 2 = j S 2j :

Pred t ( i S 1i , j S 2j ) = i j Pred t (S 1i , S 2j )
Finally, we will, in the sequel use the following lemma: Lemma 4 ( [START_REF] Jovanović | A Game Approach to the Parametric Control of Real Time Systems[END_REF]): For any location l, any set of valuations on both clocks and parameters Z, Z , and any parameter valuation

v |P : 1) v |P (Z ) = v |P (Z) 2) v |P (Z ∩ Z ) = v |P (Z) ∩ v |P (Z) 3) v |P (Z[R] -1 ) = v |P (Z)[R] -1 4) v |P (Z \ Z ) = v |P (Z) \ v |P (Z) 5) for any edge e, v |P (Pred((l, Z), e)) = Pred((l, v |P (Z)), v |P (e)) 6) v |P (Pred t (Z 1 , Z 2 )) = Pred t (v |P (Z 1 ), v |P (Z 2 ))
Now, if we denote by S goal = {l goal } × R X∪P , then a backwards algorithm for solving reachability games is given as the fixed-point computation of: W 0 = ∅ and

W n+1 = S * ∩ (Pred t (cPred(W n ), uPred(S * \W n )) ∪ S goal )
The computation of Pred t (cPred(W n ), uPred(S * \W n )) is illustrated in Figure 1. Of course, this might not terminate. When it exists, however, the final fixed-point set is noted W * and we have the following result:

q qc ∈ cPred(Wn) q ∈ uPred(S * \Wn) q1 ∈ Wn q2 ∈ S * \Wn δ > 0 δ ≥ 0 c u
Lemma 5 ( [START_REF] Jovanović | A Game Approach to the Parametric Control of Real Time Systems[END_REF]): For a PGA G, a location l goal , and a state (l, v), it holds that for all i, (l, v) is reachable and there exists a winning strategy enforcing l goal in at most i controllable steps from

(l, v |X ) in v |P (G) iff (l, v) ∈ W i .

B. Integer backward operators

We can now extend the backward operators. From Lemma 2, the result of applying Pred t to two parametric zones is a finite union of parametric zones, on which we will be able to apply Pred t again with Lemma 3, leading again to finite unions of parametric zones. In the backward computation of winning states, we therefore use IS rather than IH.

We first extend the predecessor by an edge operator (Pred) for the computation of integer parameter valuations, similarly to the extension of Succ operator. For a symbolic state (l, D) and an edge e, the integer predecessor by an edge e of (l, D) is defined as: IPred((l, D), e) = IS(Pred((l, D), e)).

We then have the following result: Lemma 6: For any symbolic state (l, Z), with D a finite union of parametric zones, and any edge e: Let us now consider v ∈ IntVects(Pred((l, Z), e)).

Then there exists v ∈ Z such that v ∈ IntVects(Pred((l, {v }), e)). By definition of Pred we also have

v |P = v |P . So v ∈ v |P (Z).
And since v is an integer vector, so is v |P and v |P (Z) is therefore a zone of a classical TA and thus has integer vertices. Consequently, v |P (Z) = IS(v |P (Z)). Moreover, v |P (Z) ⊆ Z (with a slight abuse of notations: each clock valuation in v |P (Z) needs to be combined with the parameter valuation v |P for the dimensions to match) and IS is nondecreasing, so IS(v |P (Z)) ⊆ IS(Z) and thus v ∈ IS(Z) and v ∈ IntVects(Pred((l, IS(Z)), e)). Finally, Conv being non-decreasing, we obtain IS(Pred(IS((l, Z)), e)) ⊇ IS(Pred((l, Z), e)). Now, suppose that D = i Z i , with all Z i convex. Then by definition of IS and Pred, we have IPred(IS((l, Z), e)) = i IPred(IS((l, Z i ), e)). Similarly, IS(Pred((l, Z), e)) = i IS(Pred((l, Z i ), e)). And using the result above for each convex Z i , we complete the proof.

We define, in a similar way:

• integer controllable action predecessors: cIPred((l, Z)) = IS(cPred((l, Z))), • integer uncontrollable action predecessors: uIPred((l, Z)) = IS(uPred((l, Z))). The same result obviously holds for uPred and we can finally extend this to the safe-timed predecessor operator by

IPred t (D 1 , D 2 ) = IS(Pred t (D 1 , D 2 )).
Lemma 8: For any two finite unions of parametric zones D 1 and D 2 :

IPred t (IS(D 1 ), IS(D 2 )) = IS(Pred t (D 1 , D 2 ))
Proof: Since D 1 and D 2 are finite unions of parametric zones, we can write them as:

D 1 = i D 1i and D 2 = j Z 2j . By Lemma 3 we have Pred t ( i Z 1i , j Z 2j ) = i j Pred t (Z 1i , Z 2j ).
And by Lemma 2, for any i, j, we have:

Pred t (Z 1i , Z 2j ) = (Z 1i \Z 2j ) ∪ ((Z 1i ∩ Z 2j )\Z 2j ) , because Z 2j is convex.
What we need to show then is that, for any two parametric zones Z 1 and Z 2 :

• IS(Z 1 ∩ Z 2 ) = IS(IS(Z 1 ) ∩ IS(Z 2 )) • IS(Z 1 ∪ Z 2 ) = IS(IS(Z 1 ) ∪ IS(Z 2 )) • IS(Z 1 ) = IS(IS(Z 1 ) ) • IS(Z 1 \Z 2 ) = IS(IS(Z 1 )\IS(Z 2 ))
These four results are quite straightforward. Let us just prove the first, the rest being similar.

First remark that Z 1 and Z 2 being convex, integer shapes are actually integer hulls. Second IH(Z) ⊆ Z, for any Z and since IH is non-decreasing,

IH(IH(Z 1 ) ∩ IH(Z 2 )) ⊆ IH(Z 1 ∩ Z 2 ). Finally, if v ∈ IntVects(Z 1 ∩ Z 2 ) then clearly v ∈ IntVects(Z 1 ) ∩ IntVects(Z 2 ) and consequently v ∈ IH(Z 1 ) ∩ IH(Z 2 )). Since v is an integer valuation, we further have v ∈ IntVects(IH(Z 1 ) ∩ IH(Z 2 ) and thus IntVects(Z 1 ∩ Z 2 ) ⊆ IntVects(IH(Z 1 ) ∩ IH(Z 2
)) and we conclude by remarking that Conv is non-decreasing and can therefore be applied on both sides while preserving the inclusion.

C. Computing the Winning States with Integer Parameters

Consider now the following fixed-point computation: IW 0 = ∅ and

IW n+1 = IS * ∩(IPred t (cIPred(IW n ), uIPred(IS * \IW n ))∪S goal )
When it terminates, we call IW * the corresponding fixpoint.

Lemma 9: For any integer parameter valuation v, and any finite union of parametric zones D: v(IH(D)) = v(D).

Proof: By definition of IS, we have IS(D) ⊆ D. Then, using Lemma 4, we obtain that v(IS(D)) ⊆ v(D).

Consider for now a single parametric zone Z. Since v is an integer parameter valuation, zone v(Z) has integer vertices so IH(v(Z)) = v(Z). Let w ∈ IntVects(v(Z)). Then clearly the valuation combining w and v belongs to Z and is an integer valuation. So it belongs to IH(Z). So w ∈ v(IH(Z)) and therefore IntVects(v(Z)) ⊆ v(IH(Z)). Since Conv is nondecreasing and v(IH(Z)) is convex, we therefore obtain that IH(v(Z)) ⊆ v(IH(Z)). And then v(Z) ⊆ v(IH(Z)).

To conclude, consider now that D = i Z i , each Z i being a parametric zone. Then i v(Z i ) = i v(IH(Z i )) and then, using the basic properties of valuations, v( i Z i ) = v( i IH(Z i )), which is the expected result.

Lemma 10: For any integer parameter valuation v, any location l, any finite union of parametric zones D, and any edge e: v(IPred((l, D), e)) = Pred((l, v(D)), v(e)).

Proof: Since D is a finite union of parametric zones, so is Pred((l, D), e) and by Lemma 4, we have Pred((l, v(D)), v(e)) = v(Pred((l, D), e)). Furthermore, v is an integer valuation, so by Lemma 9, we have v(Pred((l, D), e)) = v(IS(Pred((l, D), e))) and finally Pred((l, v(D)), v(e)) = v(IS(Pred((l, D), e))).

Lemma 11: For all integer parameter valuation v and all n ≥ 0, v(IW n ) = v(W n ).

Proof: Let v be an integer valuation. We work by induction on n The case for n = 0 is trivial. Now consider some n ≥ 0 and suppose the property holds:

Recall that

IW n+1 = IS * ∩ (IPred t (cIPred(IW n ), uIPred(IS * \IW n )) ∪ S goal )
Then, by Lemma 8,

IW n+1 = IS * ∩ (IS(Pred t (cPred(IW n ), uPred(IS * \IW n ))) ∪ S goal )
Using now Lemma 9, Lemma 4, and Lemma 10,

v(IW n+1 ) = v(IS * ) ∩ (Pred t (cPred(v(IW n )), uPred(v(IS * )\v(IW n ))) ∪v(S goal ))
Using the analogue of Lemma 10 for Succ [4, Lemma 4], since v is an integer valuation, we have v(ISucc((l, D), e)) = Succ((l, v(D)), v(e)). Through a straightforward induction, this implies that since v is an integer valuation, v(IS * ) = v(S * ).

Putting it all together with the induction hypothesis, this means that v(IW n+1 ) = v(W n+1 ).

Lemma 12: For a PGA G, location l goal , and a state (l, v) such that v is an integer valuation, it holds that ∀i, there exists a winning strategy in at most i controllable steps from

(l, v |X ) in v |P (G) iff (l, v) ∈ IW i .
Proof: Direct from Lemma 11. We now prove that the fixed-point computation IW n terminates and that its result IW * is correct and complete.

Theorem 13 (Termination): For any PGA G and any desired location l goal , the algorithm terminates.

Proof: We proved that the forward computation of IS * terminates. When going backwards, each time we apply IPred t we know that we have added to the winning set of states at least one integer point (otherwise the integer hulls are the same and we can terminate). Since there is only a finite number of integer points to add (due to the boundedness of clocks and parameters), the computation terminates.

Theorem 14 (Correctness and completeness):

Let Start(G) = {v ∈ R X∪P | v |X = 0 X }.
Let v be an integer parameter valuation. For any PGA G and any location l goal , upon termination, there exists a winning strategy for the controller in v(G) iff v ∈ (IW * ∩ Start(G)) |P .

Proof: We start by proving the right to left implication. Suppose v ∈ (IW * ∩ Start(G)) |P . Then there exists a state (l 0 , v 0 ) in IW * ∩ Start(G) such that v 0|P = v and v 0|X has all coordinates equal to 0, therefore v 0 is an integer valuation on X ∪ P and since it belongs IW * , it belongs to IW n for some n. We can then apply Lemma 5 to conclude. Now, we prove the left to right implication. If there exists a winning strategy for the controller to win in v(G) then it means that it can win within a finite number of controllable steps. Then, by Lemma 5, it means that the state (l 0 , v 0 ) such that v 0|P = v and v 0|X has all coordinates equal to 0 belongs to IW n for some n, and therefore to IW * , which concludes the proof.

D. Avoiding Integer Hulls in the Backward Computation

We have shown how to symbolically compute the bounded integer parameter valuations that permit the controller to win. We will now prove that, surprisingly, we actually do not have to apply the integer hull in the backwards computation, in order to obtain the correct integer solution and ensure termination.

Consider the fixed-point computation corresponding to this setting: IW 0 = ∅ and

IW n+1 = IS * ∩ (Pred t (cPred(IW n ), uPred(IS * \IW n )) ∪ S goal )
Let us first show that if this procedure terminates, it is sound and complete.

Theorem 15 (Correctness and completeness): For any PGA G, a desired location l goal , and an integer parameter valuation v, upon the termination, there exists a winning strategy for the

controller in v(G) iff v ∈ (IW * ∩ Start(G)) |P .
Proof: First remark that, for all n, we have IW n ⊆ IW n ⊆ W n , because integer hulls and shapes only remove points. Let v be an integer parameter valuation. Then, we have

v(IW n ) ⊆ v(IW n ) ⊆ v(W n ). By Lemma 11, v(IW n ) = v(W n
) so all three sets are actually equal and in particular v(IW n ) = v(W n ). The theorem then follows in the same way as Theorem 14.

Proving the termination is much trickier: we construct new objects, that we call parametric regions, that refines the standard regions for timed automata of [START_REF] Alur | A Theory of Timed Automata[END_REF] with parametric constraints. We therefore further divide the regions with all the guards from the model and all the constraints defining integer hulls (of the symbolic states) obtained in the forward computation. We prove that these parametric regions are in finite number, that the symbolic states are convex unions of such regions and that the backwards computation preserves such unions. From this we can conclude that the backwards fix-point computation eventually terminates.

Before going into the details of this refinement, let us first briefly recall the main ideas between Alur & Dill's region partition for timed automata.

The aim is to define an equivalence relation on clock valuations such that if two valuations are equivalent they go to equivalent valuations, both by taking some edge, or by letting some time elapse. Regions are then the equivalence classes of that relation. Ensuring that there is a finite number of those regions relies on the fact that if the value of some clock x is above the maximal constant m appearing in all the clock constraints of the automaton (guards and invariants), then the actual value does not matter, only the fact that it is above m: a constraint x ≤ c (with by definition c ≤ m) is false and a constraint x ≥ c is true, for any such value.

The dashed part of Fig. 2 outlines the region partition of the clock space in the particular case of two clocks x 1 and x 2 . Each region is either a single point with integer coordinates, an open segment strictly between two such points (vertical, horizontal or diagonal), an open triangle, strictly between these segments or points, or, finally, beyond the maximal constant m appearing in the constraints of the system, open and infinite rectangles. We see that for a given value of m there are a finite number of regions.

For timed automata, when clocks are bounded, or by applying an extrapolation operator (see e.g. [START_REF] Behrmann | Lower and upper bounds in zone-based abstractions of timed automata[END_REF]), the valuation part of symbolic states as computed by (the specialization of) the Succ operator, are convex unions of regions (i.e. zones) for a suitable finite value of m, which ensures that they are in finite number.

In the parametric case, this is more complex because these symbolic states constrain both clocks and parameters. To ensure that they are also in finite number, using the same idea as in [4, Section IV.D.1], we can derive a bound on clocks from the bound on parameters. We could also alternatively use the bound on parameters for an extrapolation operator [START_REF] André | Integer-complete synthesis for bounded parametric timed automata[END_REF]. Thus we again have a finite number of regions. But the polyhedra defining the state-space are not convex unions of those regions: we therefore also need to refine the regions abstraction by partitioning along all the constraints encountered in the guards and invariants of the PGA, and in the integer hulls of the symbolic states computed in the forward exploration.

Furthermore, such a constraint may create a non-integer point when intersecting the lines x = k, for some clock x and k ∈ N. For each such point, we also further partition along all lines that go though that point and are parallel to the diagonal constraints of the region abstraction (added constraints are of therefore of the form x i -x j = k for some clocks x i , x j and k ∈ Q).

Note that if a constraint in the integer hull of some symbolic state intersects a diagonal line defined by x i -x j = k, for some clocks x i , x j and some k ∈ Z, creating a non-integer point, then the partition already accounts for diagonals going through this point, due to the standard region construction. We now give a formal definition of parametric regions.

Definition 9 (Parametric regions): Let m be the maximal value of parametric expressions occurring in the constraints of the PGA (recall that parameters are bounded so it is possible to compute that value). Parametric regions are constructed in the following way:

1) the variable-space R X∪P is partitioned along the constraints x ∼ k and x -y ∼ k for all clocks x, y ∈ X, ∼∈ {<, =, >} and 0 ≤ k ≤ m (this gives standard regions); 2) for any guard or invariant of the automaton and any constraint appearing in the (finite number of) polyhedra defining IS * , γ ∼ 0, we further partition the variablespace, with the constraints γ ∼ 0 for every ∼ ∈ {<, = , >}; 3) for any (non-integer) point that is the intersection of constraints using an = operator and added in the first two steps, we further refine the variable-space by constraints of the form x -y + k ∼ 0, with ∼∈ {<, =, >} for all clocks x = y and k ∈ Q, going through that point. Fig. 2b shows a two-dimensional example of how the variable-space is partitioned into parametric regions. The dimensions related to parameters are not shown to keep the figure readable. The integer hull of some symbolic state obtained during the forward exploration is drawn in red. Its side that does not overlap with the region graph is extended (in green) as long as it cuts the region graph. Additionally, each non-integer point obtained in the intersection of the constraints defining the integer hull and the region graph, has a diagonal constraint that goes through it (in blue). An example of a parametric region is given in gray.

In order to prove the termination when going backwards, we have to show that all the operators preserve the parametric regions.

Lemma 16: If (a i ) i and (b j ) j are finite families of parametric regions then the following sets are a finite union of parametric regions:

1) i a i ∪ j b j ;

2) i a i ∩ j b j ; 3) the complement of i a i ; 4) ( i a i ) ; 5) the valuation part of Pred((l, i a i ), e), for any location l and edge e; 6) Pred t ( i a i , j b j ).

Proof: The first three are straightforward using the fact that parametric regions are taken from a finite set.

Given one parametric region, the "past" operator consists in (i) removing the constraints that impose lower bounds on clocks, (ii) add constraints that ensure that clocks stay nonnegative: ∀i, x i ≥ 0, and (iii) add constraints that ensure that all clocks evolve at the same speed: ∀i, j, x i -x j stays in the same fixed interval as in the regions of which we take the past. These constraints we remove or add are all used to partition the variable-space into parametric regions. So, removing or adding them lead to a union of parametric regions. For several parametric regions, the same results holds by finite union.

The fifth is immediate because the constraints of guards and invariants are used to define the parametric regions.

For Pred t we need to use once again the two results from [START_REF] Cassez | Efficient onthe-fly algorithms for the analysis of timed games[END_REF]:

Pred t ( i a i , j b j ) = i j Pred t (a i , b j ) and Pred t (a i , b j ) = (a i \b j ) ∪ ((a i ∩ b j )\b j ) (if b j is convex,
which is true by definition of the parametric region), which can equivalently be written as: Pred t (a i , b j ) = (a i ∩ b j ) ∪ (a i ∩ b j ∩ b j ) . We can then conclude by using the first four results.

We can now get back to the termination of the IW n fixedpoint computation:

Theorem 17 (Termination): For any PGA G and any desired location l goal the fixed-point computation of IW * terminates.

Proof: Again, we know, from [START_REF] Jovanović | Integer parameter synthesis for real-time systems[END_REF], that the forward computation of IS * , using ISucc and for bounded parameters, terminates. By definition of parametric regions, IS * can be written as a finite union of symbolic states whose associated valuations can be represented as finite unions of parametric region. When going backwards using Pred t , by Lemma 16 we know that parametric regions are preserved. Therefore at each step at least one region is added to the set of winning states (otherwise the fixed-point is reached and we can terminate). Since there is a finite number of parametric regions, the computation must terminate.

E. Complexity

As remarked in [START_REF] Jovanović | Integer parameter synthesis for real-time systems[END_REF], all of the possible valuations of parameters, that are integer and bounded, can be enumerated in exponential time. Therefore, for a problem that is EXPTIME for TGA, the corresponding bounded integer version for PGA is also EXPTIME. The timed control problem is EXPTIMEcomplete for TGA [START_REF] Jurdzinski | Reachability-time games on timed automata[END_REF], and it is a special case of the parametric control problem for PGA. We can thus conclude that the parametric control problem for PGA is EXPTIMEcomplete for bounded integer parameters.

Theorem 18: The parametric control problem for PGA with bounded integer parameters is EXPTIME-complete.

V. ILLUSTRATIVE EXAMPLE

We consider the same example as in [START_REF] Cassez | Efficient onthe-fly algorithms for the analysis of timed games[END_REF], but we extend and parameterize the model in order to obtain the Parametric Game Automata of Figure 3. The model has two clocks x and y, controllable (c i ) and uncontrollable (u i ) actions and two parameters a and b. The reachability game consists in finding a strategy for the controller that will eventually end up in location Goal. We now explain how the algorithm works.

A. Computation of IS *

We note Z a zone computed with the bounded integer parameter assumption and Z otherwise.

Without the bounded integer parameter assumption, the initial symbolic state is:

(l 0 , Z 0 ) with Z 0 = x = y ∧ x ≥ 0 ∧ y ≥ 0 . After n loops u 0 , we have : (l 0 , Z n ) with Z n = x ≥ a ∧ a ≤ b + 1 ∧ 0 ≤ na ≤ y -x ≤ n(b + 1)
. At this step, without the bounded integer parameter assumption, the symbolic state graph (see Figure 4) is not finite and the algorithm does not terminate neither for integer parameters nor for bounded parameters.

We now ensure the termination in the integer and bounded case. For example, assume all parameters and clocks are less

l 0 l 1 y ≥ 2; c 0 ; x := 0, y := 0 a ≤ x ≤ b + 1; u 0 ; x := 0 l 5 l 2 Goal l 3 l 4 x > a; u 1 x < 1 u 2 x := 0, y := 0 x ≤ a; c 1 x ≥ 2; c 2 x < b u 3 c 3 x ≤ a c 4 Fig. 3. A Parametric Timed Game Automaton l 0 Z 0 l 0 Z 1 . . . l 0 Z n . . . l 1 x ≥ 0 l 5 x > a l 2 x ≥ 0 Goal x ≥ 2 l 3 x ≥ 0 l 4 x ≥ 0 u 0 u 0 u 0 u 0 c 0 u 1 u 2 c 1 c 2 u 3 c 3 c 4 l 1 a ≤ b + 1 l 5 x > a a ≤ b + 1 l 2 a ≤ b + 1 Goal x ≥ 2 a ≤ b + 1 l 3 a ≤ b + 1 l 4 a ≤ b + 1 c 0 c 0 c 0 c 0 u 1 u 2 c 1 c 2 u 3 c 3 c 4
Fig. 4. Infinite Symbolic state graph • After one loop:

l 0 Z 0 l 0 Z 1 l 0 Z 2 l 0 Z 3 l 0 Z 4 l 1 x ≥ 0 . . . u 0 u 0 u 0 u 0 u 0 c 0 l 1 a ≤ b + 1 . . .
Z 1 = x ≥ a ∧ a ≤ 3 ∧ a ≤ b + 1 ∧ a ≤ y -x ≤ b + 1 • After two loops: Z 2 = x ≥ a ∧ a ≤ 1 ∧ a ≤ b + 1 ∧ 2a ≤ y -x ≤ 2(b + 1) • After three loops: Z 3 = x ≥ a∧a ≤ 1∧a ≤ b+1∧3a ≤ y -x ≤ 3(b + 1) • After four loops: Z 4 = x ≥ a∧a = 0∧a ≤ b+1∧y-x ≤ 3 • ∀n > 4, after n loops: Z n = Z 4
The symbolic state graph representing IS * is given in Figure 5. Only the top part of the figure changes compared to Figure 4, so we have removed the bottom part to make it more readable. After transition c 0 , the resets of clocks x and y remove the diagonal constraint involving y -x then from location l 1 on, we have x = y since x and y are, from this location on, always reset simultaneously then, for the sake of readability, we omit clock y in the symbolic states associated with locations l 1 and its successors. Moreover, all the symbolic states obtained by transition c 0 from (l 0 , Z 1 ). . . (l 0 , Z 4 ) are included in (l 1 , x ≥ 0 ∧ a ≤ b + 1). We merge them in the symbolic state graph of Figure 5, again for the sake of readability. This is by the way a classical optimisation for timed games, discussed in [6, Section 5.2], and easily extended to the parametric case.

B. Backward algorithm

After the computation of the symbolic states, shown in Figure 5, the backward algorithm starts from the symbolic winning subsets (Goal, x ≥ 2) and (Goal, x ≥ 2 ∧ a ≤ b + 1). To show more precisely from where the constraints come, we actually describe the back-propagation following the different paths instead of computing explicitly the sets IW n (in [START_REF] Cassez | Efficient onthe-fly algorithms for the analysis of timed games[END_REF], it is shown that this leads to the same result). From (Goal, x ≥ 2 ∧ a ≤ b + 1), by the controllable action (c 2 ) predecessor, we obtain (l 2 , x ≥ 2 ∧ a ≤ b + 1). Computing the (timed) past removes the constraint x ≥ 2, and computing the safe-timed predecessor adds x ≥ b in order not to end-up in l 3 by u 3 . The resulting state is (l 2 , x ≥ b∧a ≤ b+1). The controllable action predecessor for c 4 adds the constraint x ≤ a. The constraint on the parameters derived in this state is a ≥ b. This constraint is back-propagated to the predecessor states. The safe-timed predecessors give us the state (l 4 , x ≥ 0 ∧ a ≥ b ∧ a ≤ b + 1).

We obtain successively the following sets of winning states:

• (l 3 , x ≥ 0 ∧ a ≥ b ∧ a ≤ b + 1), • (l 2 , (x ≥ b) ∨ (x ≥ 0 ∧ a ≥ b) ∧ a ≤ b + 1), • (l 1 , (x ≤ a)∧ (x < 1∧a ≥ b)∨x ≥ 1 ∧ (x ≥ b)∨(x ≥ 0 ∧ a ≥ b) ∧ a ≤ b + 1). The last one simplifies to (l 1 , x ≤ a ∧ a ≥ b ∧ a ≤ b + 1).
From the symbolic winning subset (Goal, x ≥ 2), we obtain the same result without the constraint a ≤ b + 1.

The constraints are now back-propagated to the states associated with l 0 . The constraint a > 0 is added in order not to end-up in the symbolic state (l 0 , Z 4 ) by an infinite loop u 0 in null time for symbolic state (l 0 , Z 4 ) which is back-propagated to (l 0 , Z 3 ) . . . (l 0 , Z 0 ). Moreover the back-propagation from (Goal, x ≥ 2) to (l 0 , Z 0 ) leads to the constraint a > b+1. We finally obtain (l 0 , (a ≥ b) ∧ (a > b + 1) ∨ (a ≤ b + 1) ∧ (a > 0) ). Thus, there exists a winning strategy if and only if

(a > b + 1) ∨ (a > 0) ∧ (b ≤ a ≤ b + 1) .

C. Extracting a Winning Strategy

We first recall a classical result (straightforwardly extended to the parametric setting): Theorem 19 ( [START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF]): Let (G, l goal ) be a parametric reachability timed game. For all parameter valuations v, if there exists a winning strategy in v(G) then there exists a memoryless winning strategy in v(G).

With this theorem, and following [START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF], it is easy to extract a memory-less winning strategy from the set of winning states. We proceed as follows: a controllable action predecessor gives us the state from which a corresponding controllable action should be taken, while safe-timed predecessor further gives us the state where we should delay.

Since we work on symbolic states, for all the (concrete) states in a given symbolic state of W * , in particular with the same clock valuations but different parameter valuations, give the same strategies by this procedure. This thus gives "parametric strategies" defined in function of the parameters.

Let us now illustrate how to extract a winning strategy from the winning set of states. The symbolic state (l 2 , x ≥ 2) is the controllable action predecessor of (Goal, x ≥ 2) by action c 2 . Then the winning strategy is: in all states of (l 2 , x ≥ 2) the controllable transition c 2 should be taken immediately, and in (l 2 , x ≥ 0), we should delay until x ≥ 2. The controllable action predecessor from l 2 gives two symbolic states:

• (l 1 , x ≥ 0 ∧ x ≤ a).
From that state action c 1 should be taken immediately. The controllable action predecessor gives (l 0 , y ≥ 2) from which action c 0 should be taken immediately. Timed predecessors give the symbolic state (l 0 , y < 2) in which we should delay until y ≥ 2. • (l 4 , x ≥ b∧x ≤ a), deriving a constraint a ≥ b. From that state action c 2 should be taken immediately, and timed predecessors give the symbolic state (l 4 , x ≥ 0, a ≥ b) in which we should delay until x ≥ b. The controllable action predecessor is (l 3 , x ≥ 0) from which action c 3 should be taken immediately

We can do the same reasoning by starting from (Goal, x ≥ 2, a ≤ b + 1). Notice that there may be several winning strategies. Algorithmically speaking, the order of exploration of the winning states leads to different winning strategies for different values of parameters.

Instantiating the parameters: Recall that for this example, the parameters are bounded by (a ≤ 3) and (b ≤ 3) and there exists a winning strategy if and only if (a > b+1)∨ (a > 0) ∧ (b ≤ a ≤ b + 1) . The possible values for (a, b) are then (2, 0), (3, 0), (3, 1), (1, 1), (2, 1), (2, 2), (3, 2), [START_REF] Hune | Linear parametric model checking of timed automata[END_REF][START_REF] Hune | Linear parametric model checking of timed automata[END_REF]. We choose valuation a = 2 and b = 1 which satisfies the constraints. A winning strategy corresponding to this parameter valuation, and extracted from the winning states set, is:

In all states: Do:

(l 0 , y < 2) delay (l 0 , y ≥ 2) c 0 (l 1 , x ≤ 2) c 1 (l 2 , x < 2) delay (l 2 , x ≥ 2) c 2 (l 3 , x ≥ 0) c 3 (l 4 , x < 1) delay (l 4 , x ≥ 1 ∧ x ≤ 2) c 4
Implementing the strategy: A systematic implementation of real-time models has been studied in [START_REF] Wulf | Systematic implementation of real-time models[END_REF]. Practically speaking, implementing such a strategy can be done on different targets such as field programmable gate arrays (FPGA) [START_REF] Fleming | FPGA based control for real time systems[END_REF] or microcontrollers [START_REF] Bandur | Microcontroller assembly synthesis from timed automaton task specifications[END_REF]. For more complex strategies and in particular for distributed systems, the implementation of distributed timed automata specifications is proposed in [START_REF] Devillers | Implementing timed automata specifications: The "sandwich" approach[END_REF], allowing to guarantee that the specifications are preserved by the implementation.

VI. IMPLEMENTATION AND CASE STUDY

We have implemented the computation of the winning states and the synthesis of the strategy in our tool ROM ÉO1 [START_REF] Lime | Romeo: A parametric model-checker for Petri nets with stopwatches[END_REF]. With its textual input language, ROM ÉO handles a model called Clock Transition Systems (CTS) which encompasses both timed automata and Time Petri Nets. We have extended CTS with controllable and uncontrollable actions in order to model parametric timed games. In this section, we show how the parametric reachability control problem can be used in practice for the synthesis of an offline scheduler.

A. The model

We consider a scheduling problem proposed in [START_REF] Bucci | Time state space analysis of real-time preemptive systems[END_REF] and adapted for a periodic non-preemptive and parametric setting. Consider three real-time tasks τ 1 , τ 2 and τ 3 . Task τ 1 is periodic with period a and has an execution time C 1 ∈ [10, b] where a and b are parameters. Tasks τ 2 and τ 3 are periodic with periods respectively 2a and 3a, and execution time C 2 ∈ [18, 28] and C 3 ∈ [20, 28]. These three tasks are scheduled using a non-preemptive2 policy defined by the controller we want to synthesise.

We model this problem with a network of 4 parametric timed automata given in Figs 6.a, 6.b, 6.c and 6.d. The automaton given in Fig. 6.e will be used later instead of the one from Fig. 6.d. The automata of the network interact with each other by a classical synchronized product à la Arnold Nivat where a transition with label e! (respectively e?) must be executed simultaneously with one and only one other transition with label e? (respectively e!). The synchronization of actions start i (in blue on the figure Fig. 6) is done as soon as possible (this is an urgent channel in the tool UPPAAL [START_REF] Behrmann | Uppaal-tiga: Time for playing games![END_REF]).

We assume invariants make it possible to win by taking an uncontrollable action forced by the urgency of the invariant. These "forced" uncontrollable actions can be easily simulated in our framework by adding, for each uncontrollable action from l to l with a time interval [α, β], a controllable action from l to l with the point time interval [β, β]. The models of the tasks and their activations are given in Figures 6.a, 6.b and 6.c. For example, for task τ 1 in Figure 6.a, as soon as clock x 1 reaches value a, synchronization start 1 can be performed if the automaton of the task is in state task 1 . But if x 1 reaches again value a and exceeds it (meaning that the task τ 1 overruns its deadline) synchronization start 1 will definitively be impossible. After the synchronization, the automaton for the activation is in location clock 1 and the automaton of task τ 1 is in location ready 1 . The non-preemptive scheduler is given in Figure 6.d.

Moreover, we give in Figure 6.e, the model of the nonpreemptive scheduler (to be used instead of the model given in Figure 6.d) with the classical "rate monotonic" priority assignment policy, i.e. static priorities are assigned according to the period of the task, so a shorter period results in a higher task priority. With the scheduler of Figure 6.e, actions notReady i and Activate i are urgent. A fixed priority assignment policy is referred to as optimal if it can schedule all tasks sets that are schedulable using a different priority assignment. Rate monotonic priority assignment is not optimal for fixed priority non-preemptive scheduling.

B. Our results

We first use the scheduler of Figure 6.d. where the controller can choose to execute any ready task. Using ROM ÉO, and given that all parameters should be non-negative integers, we obtain that there exists a winning strategy (and then an offline scheduler) iff a -b ≥ 28 and b ≥ 10. ROM ÉO can extract one strategy among the winning strategies corresponding to infinitely repeating the following sequence of task executions: τ 2 , τ 1 , τ 3 , τ 1 , τ 2 , τ 1 , τ 3 , τ 1 , τ 2 , τ 1 , τ 1

We now change the model of the scheduler with the rate monotonic priority assignment defined by priority(τ 1 ) > priority(τ 2 ) > priority(τ 3 ) and modelled in Figure 6.e . It leads to the same constraints a -b ≥ 28 and b ≥ 10 but the winning strategy is now unique and corresponds to the following repeated sequence: τ 1 , τ 2 , τ 1 , τ 3 , τ 1 , τ 2 , τ 1 , τ 3 , τ 1 , τ 2 , τ 1 .

This result is very interesting in practice since it shows that, for this case study, the non-preemptive priority policy is actually optimal for the task sets that correspond to all the possible integer parameter values.

C. Comparison with an enumeration of the parameter values

To the best of our knowledge, the only other approach from the state-of-the-art able to solve a problem similar to ours, is to explicitly enumerate all the possible parameter valuations (assuming there are only a finite number of them), and to solve all the resulting timed games.

We therefore compare now the overall usefulness of our approach to this explicit enumeration scheme. We use Roméo also to solve the timed game obtained for each parameter valuation.

We consider the schedulability problem of figure 6 and we choose values of parameters leading to both true or false results for the controllability of this schedulability problem. The results are given in table I.

In practice, our approach behaves well with respect to the scaling of the bounds on parameters. For an explicit enumeration, we can easily see in table I this is not the case. We use a machine with an Intel Core i7-6500U at 2.5 GHz and 16 Gb RAM. T O means that the computation did not finish within 60 min. We can see that our approach scales much better than the explicit enumeration. Though we show only the result for 1000, on this model, our approach is actually insensitive to the bound on parameters, when it is above 100.

Note that our implementation is not optimized for instantiated parameters. Hence, given a specialized implementation and a not too big set for the possible parameter values, an explicit enumeration might be more efficient. In the general case however, we believe that our approach is more flexible and efficient.

Moreover, our symbolic computation may terminate even if the parameters are not bounded, while explicit enumeration is impossible in this case. This situation occurs in the present case-study.

Finally, our approach directly gives a symbolic constraint, which is, in our opinion, more useful than the individual values satisfying the property.

VII. CONCLUSION

We have studied control problems for timed automata extended with timing parameters, expressed in terms of parametric timed games. In that setting, the existence of parameter values such that a controller enforcing the reachability of some control location exists is undecidable.

Since in classical timed game automata, real-valued clocks are always compared to integers for all practical purposes, we solved undecidability and termination issues by computing parameters as bounded integers.

We have proposed a further extension of a well-known fixed-point backward algorithm for solving timed games of [START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF], first extended for parametric timed games in [START_REF] Jovanović | A Game Approach to the Parametric Control of Real Time Systems[END_REF].

The method is symbolic and avoids the explicit enumeration of all possible parameter valuations. It is based on the computation of the integer hulls of the parametric symbolic states. Due to the boundedness of integer parameters, termination is ensured, and the resulting set of parameter valuations is given as symbolic constraints between parameters. We have proved the correctness and completeness of the algorithm and we have proved that the integer hull operator can be avoided when propagating the winning states backwards.

The algorithm is implemented in our tool ROMEO and we have demonstrated its use on a small scheduling case-study.

In future work, we plan to extend this work to other timed models, such as PTA with stopwatches, and look for less restrictive domains of values for parameters.

  Parametric control problem: INPUTS: A PGA G and a location l goal of G. PROBLEM: Is the parametric timed game (G, l goal ) winning? Parametric synthesis problem: INPUTS: A PGA G and a location l goal of G. PROBLEM: Compute the set of valuations v of the parameters and the corresponding winning strategies for (w p (G), l goal ) to be winning.

Fig. 1 .

 1 Fig.1. q ∈ Predt(cPred(Wn), uPred(S * \Wn)): q can reach Wn by delay and controllable action, without going in S * \Wn

  IPred(IS((l, D), e)) = IS(Pred((l, D), e))Proof: Let us first assume that Z is convex. Then IS(Z) = IH(Z). We prove both inclusions:1) IPred(IS((l, Z)), e) ⊆ IS(Pred((l, Z), e)). IS((l, Z)) ⊆ (l, Z) and since Pred and IS are nondecreasing, we immediately have IPred(IS((l, Z)), e) ⊆ IS(Pred((l, Z), e)). 2) IPred(IS((l, Z)), e) ⊇ IS(Pred((l, Z), e)).

Lemma 7 :

 7 For any symbolic state (l, D), with D a finite union of parametric zones: cIPred(IS((l, D))) = IS(cPred((l, D))) Proof: Immediate with Lemma 6 from the facts that: cPred((l, D)) = c∈Σ c Pred(IS((l, D), c))) and IS(D 1 , D 2 ) = IS(D 1 ) ∪ IS(D 2 ) when D 1 and D 2 are finite unions of parametric zones.

Fig. 2 .

 2 Fig. 2. Alur & Dill's regions (dashed) and the construction of parametric regions

c 0 c 0 c 0 c 0 Fig. 5 .

 05 Fig. 5. Symbolic state graph with a ≤ 3 ∧ b ≤ 3

Fig 6 .a

 6 Fig 6.a The periodic request and the model of the task τ1

  38, 50] b ∈ [10, 20] a -b ≥ 28 a ∈ [38, 100] b ∈ [10, 72] a -b ≥ 28 a ∈ [38, 1000] b ∈ [10, 972] a -b

  ≥ 28

	Symbolic	Computation time Computed states	0.05 s 38	0.4 s 899	0.13 s 139	4.9 s 2924	10.5 s 5275	10.5 s 5275
	Enumeration	Computation time Computed states	0.05 s 38	0.4 s 899	0.13 s 139	51.6 s 99480	1608 s 3.13 10 6	T O T O
					TABLE I
		COMPARISON WITH AN EXPLICIT ENUMERATION OF PARAMETER VALUES.

Available at http://romeo.rts-software.org

A running task cannot be interrupted.

ACKNOWLEDGMENT

This work is partially supported by the ANR national research program "PACS" (ANR-14-CE28-0002).

This work has been partially funded by ANR project ProMiS number ANR-19-CE25-0015.