Selected publications at LSV

Safety properties are crucial when verifying real-time concurrent systems. When reasoning parametrically, i.e., with unknown constants, it is of high interest to infer a set of parameter valuations consistent with such safety properties. We present here algorithms based on the inverse method for parametric timed automata: given a reference parameter valuation, it infers a constraint such that, for any valuation satisfying this constraint, the discrete behavior of the system is the same as under the reference valuation in terms of traces, i.e., alternating sequences of locations and actions. These algorithms do not guarantee the equality of the trace sets, but are significantly quicker, synthesize larger sets of parameter valuations than the original method, and still preserve various properties including safety (i.e., non-reachability) properties. Those algorithms have been implemented in Imitator II and applied to various examples of asynchronous circuits and communication protocols.

   address = {Genova, Italy},
   author = {Andr{\'e}, {\'E}tienne and Soulat, Romain},
   booktitle = {{P}roceedings of the 5th {W}orkshop on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'11)},
   DOI = {10.1007/978-3-642-24288-5_5},
   editor = {Delzanno, Giorgio and Potapov, Igor},
   month = sep,
   pages = {31-44},
   publisher = {Springer},
   series = {Lecture Notes in Computer Science},
   title = {Synthesis of Timing Parameters Satisfying Safety Properties},
   url = {},
   volume = {6945},
   year = {2011},

About LSV

Select by Year