A Benchmarks Library for Extended Parametric Timed Automata

TL;DR

This paper introduces an extended benchmarks library for parametric timed automata, including new features and challenging cases to evaluate and improve parameter synthesis algorithms for real-time systems.

Contribution

It extends the IMITATOR benchmarks library with dozens of new benchmarks featuring advanced properties and extensions, highlighting current limitations and guiding future algorithm development.

Findings

Includes benchmarks with liveness properties and multi-rate clocks

Features unsolvable toy benchmarks to test algorithm limits

Highlights the need for new parameter synthesis techniques

Abstract

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.