Selected publications at LSV

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.

   address = {Brno, Czech Republic},
   author = {Andr{\'e}, {\'E}tienne and Fribourg, Laurent},
   booktitle = {{P}roceedings of the 4th {W}orkshop on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'10)},
   DOI = {10.1007/978-3-642-15349-5_5},
   editor = {Ku{\v c}era, Anton{\'\i}n and Potapov, Igor},
   month = aug,
   pages = {76-90},
   publisher = {Springer},
   series = {Lecture Notes in Computer Science},
   title = {Behavioral Cartography of Timed Automata},
   url = {},
   volume = {6227},
   year = {2010},