Timed Automata Benchmark Description

TL;DR

This paper provides detailed descriptions of six timed automata models used as benchmarks in real-time systems model checking, aiding comparison of model checker performance.

Contribution

It introduces two new models, FDDI and PATHOS, expanding the standard benchmark set for timed automata model checking.

Findings

Six benchmark models described in detail

Includes four models from previous studies

Adds two new models for benchmarking

Abstract

This report contains the descriptions of the timed automata (models) and the properties (specifications) that are used as the "benchmark examples in Data structure choices for on-the-fly model checking of real-time systems" and "The power of proofs: New algorithms for timed automata model checking." The four models from those sources are: CSMA, FISCHER, LEADER, and GRC. Additionally we include in this report two additional models: FDDI and PATHOS. These six models are often used to benchmark timed automata model checker speed throughout timed automata model checking papers.