Control of Real-Time Systems With Integer Parameters

International audienceWe consider the problem of synthesizing controllers for real-time systems where some timing features are not known with precision. We model the plant as a parametric timed automaton (PTA), i.e., a finite automaton equipped with realvalued clocks constraining its behavior, in which the timing constraints on these clocks can make use of parameters. The most general problem we study then consists in synthesizing both a controller and values for the parameters such that some control location of the automaton is reachable. It is however well-known that most non-trivial problems on parametric timed automata are undecidable and the classical techniques for the verification (and a fortiori for the control) of timed systems do not terminate in that setting. We therefore provide a restriction on the use of parameters to ensure the decidability of the control problems. Since in classical timed automata, real-valued clocks are always compared to integers for all practical purposes, we search for parameter values as bounded integers. Hence we solve undecidability and termination issues, we provide terminating symbolic synthesis procedures, and our method retains most of the practical usefulness of PTA for the modeling of real-time systems