Behavioral Cartography of Timed Automata

We aim at finding a set of timing parameters for which a given timed automaton has a “good” behavior. We present here a novel approach based on the decomposition of the parametric space into behavioral tiles, i.e., sets of parameter valuations for which the behavior of the system is uniform. This gives us a behavioral cartography according to the values of the parameters. It is then straightforward to partition the space into a “good” and a “bad” subspace, according to the behavior of the tiles. We extend this method to probabilistic systems, allowing to decompose the parametric space into tiles for which the minimal (resp. maximal) probability of reaching a given location is uniform. An implementation has been made, and experiments successfully conducted.

• Type: Journal
• Year: 2010
• Where: RP
• Authors: Étienne André, Laurent Fribourg
• Keywords: Behavior, Control Systems, Parameters, Parametric Space, RP 2010