English

Timed Automata Benchmark Description

Formal Languages and Automata Theory 2020-05-28 v1

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.

Keywords

Cite

@article{arxiv.2005.13151,
  title  = {Timed Automata Benchmark Description},
  author = {Peter Fontana and Rance Cleaveland},
  journal= {arXiv preprint arXiv:2005.13151},
  year   = {2020}
}
R2 v1 2026-06-23T15:50:34.687Z