# A benchmark library for parametric timed model checking

## TL;DR

This paper introduces a comprehensive benchmark library for parametric timed model checking, facilitating fair comparison and evaluation of various tools and techniques in verifying real-time systems with uncertain timing constraints.

## Contribution

It provides a curated collection of benchmarks, including academic, industrial, and challenging unsolvable cases, to support the development and assessment of parametric timed model checking tools.

## Key findings

- Benchmark library includes diverse real-world and theoretical cases.
- Enables systematic comparison of different verification techniques.
- Highlights existing limitations and challenges in the field.

## Abstract

Verification of real-time systems involving hard timing constraints and concurrency is of utmost importance. Parametric timed model checking allows for formal verification in the presence of unknown timing constants or uncertainty (e.g. imprecision for periods). With the recent development of several techniques and tools to improve the efficiency of parametric timed model checking, there is a growing need for proper benchmarks to test and compare fairly these tools. We present here a benchmark library for parametric timed model checking made of benchmarks accumulated over the years. Our benchmarks include academic benchmarks, industrial case studies and examples unsolvable using existing techniques.