Quasi-equal Clocks Reduction

TACAS 2014 Supporting Material

This page provides supporting material for the paper Quasi-equal Clock Reduction: More Networks, More Queries.
 [1], published in 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS).

Overview

Quasi-equal clock reduction for networks of timed automata replaces equivalence classes of clocks which are equal except for unstable phases, i.e., points in time where these clocks differ on their valuation, by a single representative clock. An existing approach yields significant reductions of the overall verification time but is limited to so-called well-formed networks and local queries, i.e., queries which refer to a single timed automaton only. In this work we present two new transformations. The first, for networks of timed automata, summarises unstable phases without losing information under weaker well-formedness assumptions than needed by the existing approach. The second, for queries, now sup- ports the full query language of Uppaal. We demonstrate that the cost of verifying non-local properties is much lower in transformed networks than in their original counterparts with quasi-equal clocks.

If you use our benchmarks in your work, please cite us as follows:

@inproceedings{DBLP:conf/tacas/HerreraWP14,
  author    = {Christian Herrera and
               Bernd Westphal and
               Andreas Podelski},
  title     = {Quasi-Equal Clock Reduction: More Networks, More Queries},
  booktitle = {TACAS},
  year      = {2014},
  pages     = {295-309},
  ee        = {http://dx.doi.org/10.1007/978-3-642-54862-8_20},
  crossref  = {DBLP:conf/tacas/2014},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/tacas/2014,
  editor    = {Erika {\'A}brah{\'a}m and
               Klaus Havelund},
  title     = {Tools and Algorithms for the Construction and Analysis of
               Systems - 20th International Conference, TACAS 2014, Held
               as Part of the European Joint Conferences on Theory and
               Practice of Software, ETAPS 2014, Grenoble, France, April
               5-13, 2014. Proceedings},
  booktitle = {TACAS},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {8413},
  year      = {2014},
  isbn      = {978-3-642-54861-1},
  ee        = {http://dx.doi.org/10.1007/978-3-642-54862-8},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

Downloads

Click here to download the zip file which has the following sub-folders and content that we used for the experiments in this paper:

1. CD. Benchmarks for the collision avoidance protocol.
   
2. FS. Benchmarks for the wireless fire alarm network.
3. CR. Benchmarks for the RideSharing fault tolerant aggregation protocol.
4. EP. Benhmarks for the Ethernet PowerLink protocol.
5. TT. Benchmarks for the TTP/A sensor/actuator network.
   
6. LS. Benchmarks for the Lip synchronization protocol.

For more information about the benchmarks, please take a look into the paper. For the full benchmark suite please contact the authors.