The IMITATOR benchmarks library

This page contains

  1. A list of selected benchmarks from the IMITATOR benchmarks library
  2. Links to several lists of benchmarks and experimental raw data from the IMITATOR publications
  3. A link to the full list of benchmarks on GitHub

1) Selected benchmarks

Hardware circuits

Case study Reference Model Model (graphics) Verification
Property Robustness Cartography
AndOr [CC05] AndOr.imi AndOr-pta.jpg sequence AndOr.pi0 AndOr.v0
Flip-flop [CC04] flipflop.imi flipflop-pta.jpg action precedence flipflop.pi0 flipflop.v0
Simple circuit [ACR15] IMPO.imi IMPO-pta.jpg non-reachability / partial orders IMPO.pi0
Simple circuit with loop [ACR15] IMPOloop.imi IMPOloop-pta.jpg non-reachability / partial orders IMPOloop.pi0


Case study Reference Model Model (graphics) Verification
Property Robustness Cartography
Bang & Olufsen BangOlufsen.imi BangOlufsen-pta.jpg sequence BangOlufsen.pi0
Bounded retransmission protocol [DKRT97] brp.imi brp-pta.jpg non-reachability brp.pi0 brp.v0
CSMA/CD [KNSW07] csmacdPrism.imi csmacdPrism-pta.jpg (probabilities) csmacdPrism.pi0 csmacdPrism.v0
Fischer mutual exclusion [AHV93] FischerAHV93.imi FischerAHV93-pta.jpg non-reachability
Fischer mutual exclusion [HRSV02] fischerHRSV02.imi fischerHRSV02-pta.jpg non-reachability fischerHRSV02.pi0 fischerHRSV02.v0
Fischer mutual exclusion (with observer) [HRSV02] fischerHRSV02_obs.imi fischerHRSV02_obs-pta.jpg non-reachability fischerHRSV02.pi0 fischerHRSV02.v0

Toy case studies

Case study Reference Model Model (graphics) Verification
Property Robustness Cartography
Coffee machine (own work) coffee.imi coffee-pta.jpg reachability coffee.pi0 coffee.v0
Coffee machine with drinker (own work) coffeeDrinker.imi coffeeDrinker-pta.jpg various properties coffeeDrinker.pi0
Noodles cooking (own work) NoodlesCooking.imi NoodlesCooking-pta.jpg non-reachability
Nuclear plant (own work) NuclearPlant.imi NuclearPlant-pta.jpg non-reachability

2) Lists of benchmarks with experimental data

We give below lists of benchmarks associated with publications related to algorithms integrated in IMITATOR, or to case studies verified using IMITATOR.

Each page associated with a publication contains the list of benchmarks, the binaries and source of the IMITATOR version used to compute the result, and all raw experimental data.

Publication Purpose List of benchmarks
[ANPS17] Non-Zeno parametric model checking benchmarks
[ACN15] Enhanced distributed cartography benchmarks
[SAL15] Solution to the Thales FMTV challenge benchmark
[ALNS15] New algorithms PRP and PRPC benchmarks
[AFKS12] Tool paper 2.5 benchmarks
[Andre10infinity] Tool paper 2.0 benchmarks
[Andre09ictac] Tool paper 1.0 benchmarks

3) The full IMITATOR benchmark library

The entire (and raw) IMITATOR benchmark library is available on GitHub (in directory "benchmarks").

These case studies shall be repatriated to this page and sorted out in a near future.


Étienne André, Camille Coti and Nguyễn Hoàng Gia. Enhanced Distributed Behavioral Cartography of Parametric Timed Automata. In Michael Butler, Sylvain Conchon and Fatiha Zaïdi (eds.), ICFEM’15, Springer LNCS 9407, pages 319–335, November 2015. [PDF | PDF (author version) | Slides]
Étienne André, Thomas Chatain and César Rodríguez. Preserving Partial Order Runs in Parametric Time Petri Nets. In Stefan Haar and Roland Meyer (eds.), ACSD’15, IEEE, pages 120–129, June 2015. [PDF | PDF (author version)]
Étienne André, Laurent Fribourg, Ulrich Kühne and Romain Soulat. IMITATOR 2.5: A Tool for Analyzing Robustness in Scheduling Problems. In Dimitra Giannakopoulou and Dominique Méry (eds.), FM’12, LNCS 7436, Springer, pages 33–36, August 2012. (English) [PDF | PDF (author version) | BibTeX]
Rajeev Alur, Thomas A. Henzinger, Moshe Y. Vardi: Parametric real-time reasoning. STOC 1993: 592-601.
Étienne André, Giuseppe Lipari, Nguyễn Hoàng Gia and Sun Youcheng. Reachability Preservation Based Parameter Synthesis for Timed Automata. In Klaus Havelund, Gerard Holzmann, Rajeev Joshi (eds.), NFM’15, LNCS 9058, Springer, pages 50–65, April 2015. (English) [PDF | PDF (author version) | BibTeX | Slides]
Étienne André, Nguyễn Hoàng Gia, Laure Petrucci and Sun Jun. Parametric model checking timed automata under non-Zenoness assumption. In Clark Barrett and Temesghen Kahsai (eds.), NFM’17, Springer LNCS, May 2017. To appear.
Étienne André. IMITATOR: A Tool for Synthesizing Constraints on Timing Bounds of Timed Automata. In Martin Leucker and Carroll Morgan (eds.), ICTAC’09, LNCS 5684, Springer, pages 336–342, August 2009. [PDF (published version) | PDF (author version) | BibTeX | Slides]
Étienne André. IMITATOR II: A Tool for Solving the Good Parameters Problem in Timed Automata. In Yu-Fang Chen and Ahmed Rezine (eds.), INFINITY’10, Electronic Proceedings in Theoretical Computer Science 39, pages 91–99, 2010. Creative Commons Attribution 3.0 Unported (CC BY 3.0) (English) [PDF (published version) | BibTeX | Slides]
Robert Clarisó, Jordi Cortadella. Verification of timed circuits with symbolic delays. In ASP-DAC 2004: 628-633, 2004.
Robert Clarisó, Jordi Cortadella. Verification of Concurrent Systems with Parametric Delays Using Octahedra. In ACSD’05, 2005.
Pedro R. D’Argenio, Joost-Pieter Katoen, Theo C. Ruys, Jan Tretmans: The Bounded Retransmission Protocol Must Be on Time! TACAS 1997: 416-431.
Thomas Hune, Judi Romijn, Mariëlle Stoelinga, Frits W. Vaandrager: Linear parametric model checking of timed automata. J. Log. Algebr. Program. 52-53: 183-220 (2002)
Marta Kwiatkowska, Gethin Norman, Jeremy Sproston, and Fuzhi Wang. Symbolic Model Checking for Probabilistic Timed Automata. Information and Computation, 205(7), pages 1027-1077. July 2007.
Sun Youcheng, Étienne André and Giuseppe Lipari. Verification of Two Real-Time Systems Using Parametric Timed Automata. In Sophie Quinton and Tullio Vardanega (eds.), WATERS’15, July 2015. (English) [PDF (author version)]