A Benchmarks Library for Extended Timed Automata


Parametric timed automata are a powerful formalism for reasoning on concurrent real-time systems with unknown or uncertain timing constants. In order to test the efficiency of new algorithms, a fair set of benchmarks is required. We present an extension of the IMITATOR benchmarks library, that accumulated over the years a number of case studies from academic and industrial contexts. We extend here the library with several dozens of new benchmarks; these benchmarks highlight several new features: liveness properties, extensions of (parametric) timed automata (including stopwatches or multi-rate clocks), and unsolvable toy benchmarks. These latter additions help to emphasize the limits of state-of-the-art parameter synthesis techniques, with the hope to develop new dedicated algorithms in the future.

Frédéric Loulergue and Franz Wotawa (eds.), TAP 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.