AN INVERSE METHOD FOR PARAMETRIC TIMED AUTOMATA

We consider in this paper modeled by timed automata. The timing bounds involved in the action guards and location invariants of our timed automata are not constants, but parameters. Those parametric timed automata allow the modelling of various kinds of timed systems, e.g. communication protocols or asynchronous circuits. We will also assume that we are given an initial tuple pi(0) of values for the parameters which corresponds to values for which the system is known to behave properly. Our goal is to compute a constraint K(0) on the parameters, satisfied by pi(0), guaranteeing that, under any parameter valuation satisfying K(0), the system behaves in the same manner: for any two parameters valuations satisfying K(0), the behaviors of the timed automata are (time-abstract) equivalent, i.e., the traces of execution viewed as alternating sequences of actions and locations are identical. We present an algorithm Inverse Method that terminates in the case of acyclic models, and discuss how to extend it to the cyclic case. We also explain how to combine our method with classical synthesis methods which are based on the avoidance of a given set of bad states. A prototype implementation has been done, and various experiments are described.