A Benchmarks Library for Extended Timed Automata


Parametric timed automata are a powerful formalism for rea-soning on concurrent real-time systems with unknown or uncertain tim-ing constants. In order to test the efficiency of new algorithms, a fairset of benchmarks is required. We present an extension of theIMITA-TORbenchmarks library, that accumulated over the years a number ofcase studies from academic and industrial contexts. We extend here thelibrary with several dozens of new benchmarks; these benchmarks high-light several new features: liveness properties, extensions of (parametric)timed automata (including stopwatches or multi-rate clocks), and un-solvable toy benchmarks. These latter additions help to emphasize thelimits of state-of-the-art parameter synthesis techniques, with the hopeto develop new dedicated algorithms in the future.

Jun 21, 2021 — Jun 22, 2021
Dylan Marinho
Dylan Marinho
PhD Student

Dylan est en préparation d’un doctorat au sein de l'Université de Lorraine et de l’école doctorale IAEM en Science Informatique. Il est rattaché à l’équipe VeriDis du LORIA et de l'Inria.

Sur le même sujet