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 is a PhD-student at Université de Lorraine, at the IAEM Doctoral School in computer science. He belongs to the VeriDis team of the LORIA and Inria.