LAUSR

We 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 real-valued 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 nontrivial 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.