MeFoSyLoMa CNRS Iniria
QR Code
Last modified
June 28, 2016

Aug 18, 2017
Benchmarks for Parametric Time Automata


We give below a list of (parametric) timed automata benchmarks. They mostly come from the IMITATOR case studies, which are a list case studies coming from both the literature and the industry. The original reference for each case study is given below.

The Models

For each model, we provide its origin (as a reference) and the corresponding GrML description.

Case study Reference GrML input
And Or circuit [CC05] AndOr.imi.grml
Bang & Olufsen procotol BangOlufsen.imi.grml
Bounded Retransmission Protocol [DKRT97] brp.imi.grml
CSMA/CD protocol [KNSW04] csmacdPrism.imi.grml
Sample PTA exSITH.imi.grml
Flip-Flop circuit [CC07] flipflop.imi.grml
Latch circuit [And10] latchValmem.imi.grml
SPSMALL memory [And10,CEFX09] LSV.imi.grml
Jobshop 2 [AM02] maler_2_4.imi.grml
Jobshop 3 [AM02] maler_3_4.imi.grml
Jobshop 4 [AM02] maler_4_4.imi.grml
Root Contention Protocol [KNS03] RCP.imi.grml
SIMOP [And10] simop.imi.grml
SPSMALL Memory (simplified version) [And10,CEFX09] spsmall.imi.grml
SR Latch [And10] SRlatch.imi.grml
Train [AHV93] TrainAHV93.imi.grml
WLan [CC05] wlan.imi.grml