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. |
Year | DOI | Venue |
---|---|---|
2021 | 10.1007/978-3-030-79379-1_3 | TAP@STAF |
DocType | ISSN | Citations |
Conference | Lecture Notes in Computer Science book series (LNCS, volume
12740), 2021, pp 39-50 | 0 |
PageRank | References | Authors |
0.34 | 0 | 3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Étienne André | 1 | 294 | 35.08 |
Dylan Marinho | 2 | 0 | 0.68 |
Jaco van de Pol | 3 | 13 | 5.00 |