View article

Probabilistic timed automata can be used to model systems in which probabilistic and timing behaviour coexist. Verification of probabilistic timed automata models is generally performed with regard to a single reference valuation π ₀ of the timing parameters. Given such a parameter valuation, we present a method for obtaining automatically a constraint K ₀ on timing parameters for which the reachability probabilities (1) remain invariant and (2) are equal to the reachability probabilities for the reference valuation. The method relies on parametric analysis of a non-probabilistic version of the probabilistic timed automata model using the “inverse method”. The method presents the following advantages. First, since K ₀ corresponds to a dense domain around π ₀ on which the system behaves uniformly, it gives us a measure of robustness of the system. Second, it allows us to …