Case Studies Related to Dynamic Clock Elimination

This page is dedicated to the case studies related to the paper Dynamic Clock Elimination in Parametric Timed Automata.


The version of IMITATOR used to compute the case studies is IMITATOR 2.6.1.

It can be downloaded from the download page.

Case studies

We present in the following table a list of case studies computed using the inverse method using the above implementation of IMITATOR.

We give from left to right the name of the case study (with a link to the IMITATOR model), the reference, the reference valuation file pi0, the number |A| of automata in parallel, the number |X| of clocks, the number |P| of parameters, and for each of the 2 algorithms, the number |S| of states computed, the number |T| of transitions computed, the computation time t in seconds (excluding the generation of the graphical outputs), and whether the result is complete or maybe not complete. In the last 2 columns, we compare the results: first, we divide the number of states in IM by the number of states in IMdyn and multiply by 100 (hence, a number smaller than 100 denotes an improvement of IMdyn); second, we perform the same comparison for the computation time.

Experiments were performed on a KUbuntu 13.04 64 bits system running on an Intel Core i7 CPU 2.67GHz with 4 GiB of RAM.

Case study Reference Pi0 |X| |P| IM IMdyn Comparison
|S| |T| t Complete Result |S| |T| t Complete Result States time
Figure 2 [Andre13] loopingDynamic.pi0 2 2 - - Loop - - 2 2 0.007 s Yeslogstatestrace set 0 0
Figure 3 [Andre13] exClockElimination.pi0 2 2 - - Loop - - 6 8 0.006 s Yeslogstatestrace set 0 0
And-Or [CC05] AndOr.pi0 4 12 11 11 0.047 s Yes logstatestraces 11 11 0.05 s Yeslogstatestrace set 100 106
SPSMALL memory [AS13] spsmall.pi0 10 26 31 30 0.58 s Yes logstatestraces 31 30 0.584 s Yeslogstatestrace set 100 101
Train [AHV93] TrainAHV93.pi0 3 6 78 94 0.1 s Yes logstatestraces 61 76 0.072 s Yeslogstatestrace set 78 72
BRP [DKRT97] brp.pi0 7 6 429 474 3.5 s Yes logstatestraces 426 473 3.21 s Yeslogstatestrace set 99 92
CSMA/CD bc6 [KNSW07] csmacdPrism6.pi0 3 3 13365 14271 19.6 s Yes logstatestraces 13365 14271 19.5 s Yeslogstatestrace set 100 99
RCP [HRSV02] RCP.pi0 5 6 327 518 0.68 s Yes logstatestraces 181 282 0.41 s Yeslogstatestrace set 55 60
AAM06 [AAM06] maler_2_4.pi0 3 8 1497 1844 8.28 s Yes logstatestraces 768 997 2.92 s Yeslogstatestrace set 51 35
AM02 [AM02] am02.pi0 3 4 182 215 0.392 s Yes logstatestraces 182 215 0.386 s Yeslogstatestrace set 100 98
BB04 [BB04] bb.pi0 6 7 806 827 25.4 s ? logstatestraces 806 827 27.2 s ?logstatestrace set 100 107
CTC [???] concurent_tasks_chain.pi0 15 21 1364 1363 83.4 s Yes logstatestraces 201 291 2.52 s Yeslogstatestrace set 15 3
LA02 [Tamura07] LA02_2.pi0 3 5 6290 8023 710 s ? logstatestraces 4932 7154 473 s ?logstatestrace set 78 67
LPPRC10 [LPPRC10] hppr10_audio.pi0 4 7 78 102 0.375 s ? logstatestraces 78 102 0.395 s ?logstatestrace set 100 105

Description of the Case Studies

Looping examples

These 2 examples are presented in [Andre13].

Hardware circuits

The AndOr case study consists in an "AND" gate linked to an "OR" gate in a cyclic manner.

The SPSMALL case study is the model of an abstraction of an asynchronous circuit designed and sold by ST-Microelectronics.


This case study is classical train-gate-controller.


BRP is the bounded retransmission protocol.

The CSMA/CD model corresponds to the non-probabilistic version of the model described in [KNSW07] with a maximum backoff of 6.

RCP is the root contention protocol of the IEEE 1394 (“FireWire”) High Performance Serial Bus, considered in the parametric framework in [HRSV02].


The AAM06 case study is a problem of non-preemptive scheduling. Two sequences of tasks have to run concurrently trough 4 machines. The goal is to schedule the tasks to meet the deadline on the overall execution time.

The AM02 case study is a problem of preemptive job-shop scheduling with two jobs on three machines.

The BB04 case study corresponds to a three task example from [BB04, Section III, table 1]. It is an FP scheduling problem with three cyclic tasks on one machine.

The CTC (concurrent task chain) case study does not use cyclic tasks but instead has a 4 task chain and a concurrent 3 task chain. Each task in a chain cannot start until the previous one has not terminated. Each task in each chain has a given fixed priority. A scheduler assigns which task has the computational time with a FP policy.

The LPPRC10 is a two-cyclic-tasks problem with an EDF scheduler.

Algorithms used

For all case studies, the standard inverse method IM was called using the following options:

	> IMITATOR case_study.imi case_study.pi0 -with-dot -with-log

For all case studies, the inverse method with dynamic clock elimination IMdyn was called using the following options:

	> IMITATOR case_study.imi case_study.pi0 -dynamic-elimination -with-dot -with-log


Yasmina Abdeddaïm, Eugene Asarin, and Oded Maler. Scheduling with timed automata. In Theoretical Computer Science 354(2), pages 272–300, 2006.
Yasmina Abdeddaïm and Oded Maler. Preemptive job-shop scheduling using stopwatch automata. In TACAS'02, pages 113–126, 2002.
Étienne André. Dynamic Clock Elimination in Parametric Timed Automata. In FSFMA’13, OASIcs (volume 31), Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, pages 18–31, July 2013.
Étienne André and Romain Soulat. The Inverse Method. ISTE Ltd and John Wiley & Sons Inc., 2013.
Enrico Bini and Giorgio C. Buttazzo. Schedulability analysis of periodic fixed priority systems. IEEE Trans. Computers, 53(11):1462–1473, 2004.
Robert Clarisó, Jordi Cortadella. Verification of Concurrent Systems with Parametric Delays Using Octahedra. In ACSD’05, 2005.
P.R. D’Argenio, J.P. Katoen, T.C. Ruys, and G.J. Tretmans. The bounded retransmission protocol must be on time!. In TACAS’97.
T.S. Hune, J.M.T. Romijn, M.I.A. Stoelinga, and F.W. Vaandrager. Linear parametric model checking of timed automata. Journal of Logic and Algebraic Programming, 2002.
M. Kwiatkowska, G. Norman, J. Sproston, and F. Wang. Symbolic model checking for probabilistic timed automata. Information and Computation, 205(7):1027–1077, 2007.
Thi Thieu Hoa Le, Luigi Palopoli, Roberto Passerone, Yusi Ramadian, Alessandro Cimatti. Parametric Analysis of Distributed Firm Real-Time Systems: A Case Study. In ETFA’2010: 1-8.
Naoyuki Tamura. CSP2SAT: JSS benchmark results. 2007.


Étienne André