The VLTS Benchmark Suite

A joint project of CWI/SEN2 and INRIA/VASY

Pictures courtesy of Jan Friso Groote and Frank van Ham (Technical University of Eindhoven)

Contents

1. What is the VLTS benchmark suite?

The VLTS acronym stands for "Very Large Transition Systems".

The VLTS benchmark suite is a collection of Labelled Transition Systems (hereafter called benchmarks).

Each Labelled Transition System is a directed, connected graph, whose vertices are called states and whose edges are called transitions. There is one distinguished vertex called the initial state. Each transition is labelled by a character string called action or label. There is one distinguished label noted "i" that is used for so-called invisible transitions (also known as hidden transitions or tau-transitions).

The VLTS benchmarks have been obtained from various case studies about the modelling of communication protocols and concurrent systems. Many of these case studies correspond to real life, industrial systems.

2. Why the VLTS benchmark suite?

The VLTS benchmark suite is designed to be a reference criterion for scientific assessment of algorithms and tools operating on large graphs.

In particular, this encompasses algorithms and tools for explicit state verification of concurrent systems, including:

Algorithms and tools operating on more general graphs than transition systems may also benefit from the VLTS benchmark suite by simply discarding label information attached to transitions.

The need for the VLTS benchmark suite was recognized in several places, e.g., by Agostino Dovier, Carla Piazza, and Alberto Policriti in their CAV'2001 paper ("A Fast Bisimulation Algorithm"):

The VLTS benchmark suite intends to fill this gap by providing a comprehensive set of benchmarks. We hope that it will be as useful as other standard benchmarks, such as those developed, e.g., to assess Binary Decision Diagrams packages.

3. How to use the VLTS benchmark suite?

All the graphs are encoded in the BCG (Binary-Coded Graphs) format, then compressed using the bzip2 tool. To our knowledge, this is up to now the most compact way for storing Very Large Transition Systems.

First, you should make sure that you are working on a machine with enough free disk space available (at least 500 megabytes, 1 gigabyte to be safe).

If you do not have already the CADP tools installed on your machine, please registrate here.

After downloading a graph, say "graph.bcg.bz2", from the Table below, you must first uncompress it using the bunzip2 tool:
          bunzip2 graph.bcg.bz2
This will produce a BCG graph named "graph.bcg".

You can read and process "graph.bcg" from a computer program in two different ways:

  1. You can use the bcg_read API (Application Programming Interface), which provides a simple set of functions for handling BCG graphs. You will have to link your computer program against the BCG binary libraries.

  2. You can use the bcg_io tool, which converts BCG graphs into a dozen of other formats (mostly textual formats). To avoid disk space overflow, it is recommended to use this tool in pipe mode, so that the converted graph is not written to disk. For instance:
              bcg_io graph.bcg -aldebaran - | more

Note: In addition to the VLTS benchmarks, you might be interested by the various classes of `regular' benchmarks produced by the bcg_graph tool.

4. History of versions - Contributors

5. Detailed description of the VLTS benchmark suite

The VLTS benchmarks can be downloaded from the Table below. Each row of the Table corresponds to one benchmark. The columns of the Table contain the following data:

Name
(.bcg.bz2)		 #States #Transitions #Tau-
transitions		 #Labels Branching factor
avg [min - max]		 Deadlocks Livelocks Deterministic Version Size (.bcg) Size (.bz2)
vasy_0_1 289 1,224 0 2 4.24 [4 - 8] - - - VLTS-1 4 2
cwi_1_2 1,952 2,387 2,215 26 1.22 [1 - 16] - - - VLTS-1 8 2
vasy_1_4 1,183 4,464 1,213 6 3.77 [2 - 5] - - - VLTS-1 10 6
cwi_3_14 3,996 14,552 14,551 2 3.64 [0 - 6] X - - VLTS-1 13 7
vasy_5_9 5,486 9,676 2,094 31 1.76 [0 - 6] X - - VLTS-1 20 8
vasy_8_24 8,879 24,411 8,534 11 2.75 [1 - 5] - - - VLTS-1 47 32
vasy_8_38 8,921 38,424 2,916 81 4.31 [0 - 10] X - X VLTS-1 69 21
vasy_10_56 10,849 56,156 2,680 12 5.18 [4 - 6] - - X VLTS-1 120 34
vasy_18_73 18,746 73,043 39,217 17 3.90 [1 - 6] - - - VLTS-1 118 97
vasy_25_25 25,217 25,216 0 25,216 1.00 [0 - 1] X - X VLTS-1 3,454 245
vasy_40_60 40,006 60,007 20,003 3 1.50 [1 - 2] - - X VLTS-1 80 1
vasy_52_318 52,268 318,126 130,752 17 6.09 [1 - 17] - X - VLTS-1 696 566
vasy_65_2621 65,537 2,621,480 0 72 40.00 [40 - 40] - - X VLTS-1 5,272 835
vasy_66_1302 66,929 1,302,664 117,866 81 19.46 [2 - 42] - - - VLTS-1 2,617 1,441
vasy_69_520 69,754 520,633 1 135 7.46 [0 - 35] X - - VLTS-1 1,136 727
vasy_83_325 83,436 325,584 45,696 211 3.90 [0 - 96] X - - VLTS-1 822 474
vasy_116_368 116,456 368,569 263,296 21 3.16 [1 - 8] - - - VLTS-1 538 419
cwi_142_925 142,472 925,429 862,298 7 6.50 [0 - 9] X - - VLTS-1 1,147 994
vasy_157_297 157,604 297,000 31,798 235 1.88 [0 - 48] X - X VLTS-1 540 53
vasy_164_1619 164,865 1,619,204 109,910 37 9.82 [1 - 16] - - - VLTS-1 3,318 870
vasy_166_651 166,464 651,168 91,392 211 3.91 [0 - 96] X - - VLTS-1 1,513 554
cwi_214_684 214,202 684,419 550,611 5 3.20 [0 - 7] X X - VLTS-1 904 464
cwi_371_641 371,804 641,565 445,600 61 1.73 [1 - 25] - X - VLTS-1 942 167
vasy_386_1171 386,496 1,171,872 122,976 73 3.03 [1 - 38] - - - VLTS-1 1,705 122
cwi_566_3984 566,640 3,984,157 3,666,614 11 7.03 [0 - 10] X - - VLTS-1 4,743 3,988
vasy_574_13561 574,057 13,561,040 0 141 23.62 [1 - 64] - - X VLTS-1 22,446 687
vasy_720_390 720,247* 390,999* 1 49 0.54 [0 - 39] X - X VLTS-1 1,279 171
vasy_1112_5290 1,112,490 5,290,860 0 23 4.76 [3 - 6] - - X VLTS-1 12,956 8,330
cwi_2165_8723 2,165,446 8,723,465 3,830,225 26 4.03 [1 - 14] - X - VLTS-1 15,088 8,596
cwi_2416_17605 2,416,632 17,605,592 17,490,904 15 7.29 [0 - 14] X X - VLTS-1 22,298 19,398
vasy_2581_11442 2,581,374 11,442,382 2,508,518 223 4.43 [0 - 97] X - - VLTS-1 25,882 17,732
vasy_4220_13944 4,220,790 13,944,372 2,546,649 223 3.30 [0 - 97] X - - VLTS-1 30,823 8,450
vasy_4338_15666 4,338,672 15,666,588 3,127,116 223 3.61 [0 - 97] X - - VLTS-1 37,119 15,422
vasy_6020_19353 6,020,550 19,353,474 17,526,144 511 3.21 [2 - 260] - X - VLTS-1 22,072 565
vasy_6120_11031 6,120,718 11,031,292 3,152,976 125 1.80 [0 - 16] X - - VLTS-1 19,256 4,169
cwi_7838_59101 7,838,608 59,101,007 22,842,122 20 7.54 [3 - 13] - X - VLTS-1 114,277 64,427
vasy_8082_42933 8,082,905 42,933,110 2,535,944 211 5.31 [0 - 48] X - X VLTS-1 76,670 2,452
vasy_11026_24660 11,026,932 24,660,513 2,748,559 119 2.24 [0 - 13] X - - VLTS-1 51,740 29,016
vasy_12323_27667 12,323,703 27,667,803 3,153,502 119 2.25 [0 - 13] X - - VLTS-1 58,058 32,430
cwi_33949_165318 33,949,609 165,318,222 74,133,306 31 4.87 [1 - 17] - X - VLTS-1 312,337 240,432

* Note: Benchmark "vasy_720_390" is not a connected graph: there are states and transitions that cannot be reached from the initial state. This fact is clear as the number of states is greater than the number of transitions, and is also confirmed by the bcg_info tool with option -unreachable: states 87,739...720,126 and 720,128...720,246 are unreachable (there are only 87,740 reachable states and 390,510 reachable transitions). This benchmark is included to make sure that tools operating on VLTSs handle disconnected graphs properly (i.e., that they do not crash nor loop indefinitely). There are two main reasons for this requirement: (1) the usual definition of Labelled Transition Systems given in most scientific papers and textbooks is not restricted to connected graphs, and (2) in practice, disconnected graphs are produced by distributed state space generation algorithms, which construct the global state space as a collection of several disconnected graph fragments (see, e.g., the definition of a partitioned LTS).

The diagram below summarizes facts about the dispersion of the VLTS-1 benchmarks. The average branching factor is equal to the number of transitions divided by the number of states. To obtain a diagram of reasonable size, the three benchmarks with the highest branching factor are represented with a lower ordinate (Y-axis) than actually.

VLTS-1 dispersion diagram

For some of the above benchmarks, you can find here a fancy graphical visualization provided by Jan Friso Groote and Frank van Ham (Technical University of Eindhoven).

Annex A. How to donate new benchmarks?

We plan to extend the benchmark suite in the future. We are therefore interested in getting new benchmarks of various origins.

However, due to the limited capacity of our ftp site, a selection might be needed before including new benchmarks.

If you plan to donate new benchmarks, please keep in mind the following guidelines:

Please keep in mind that we will not update the benchmark suite every time a new benchmark is donated. We will wait to have a critical mass of new benchmarks before issuing a new version of the benchmark suite.

Annex B. How to scramble BCG graphs?

The bcg_labels tool with its -scramble option can be used to remove information contained in the labels of a BCG graph. This enables to donate a benchmark produced from an industrial case study without revealing intellectual property covered by non-disclosure agreements. Option -scramble is available since CADP BETA-VERSION 2008-g (December 2009). See the bcg_labels manual page for more information.

Annex C. Scientific publications using the VLTS benchmark suite (Last updated Oct. 24, 2008)

This Annex gives a (non exhaustive) list of publications referencing the VLTS benchmark suite. Please, let us know if you are aware of further references.
  1. Jirí Barnat, Jakub Chaloupka, and Jaco van de Pol. Improved Distributed Algorithms for SCC Decomposition. In: Proceedings of the 6th International Workshop on Parallel and Distributed Methods in verifiCation, 8 Jul 2007, Berlin. pp. 63-77. Electronic Notes in Theoretical Computer Science 198 (1). Elsevier. ISSN 1571-0661

  2. Damien Bergamini, Nicolas Descoubes, Christophe Joubert, and Radu Mateescu. BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking. Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2005 (Edinburgh, Scotland), volume 3440 of Lecture Notes in Computer Science, pp. 581-585. Springer Verlag, April 2005.

  3. Stefan Blom and Simona Orzan. A Distributed Algorithm for Strong Bisimulation Reduction of State Spaces. Early version: Proceedings PDMC'02 (Brno, Czech Republic), Electronic Notes in Theoretical Computer Science (ENTCS), vol. 68, num. 4, Elsevier, Aug. 2002. Full version: Software Tools for Technology Transfer (STTT), vol. 7, num. 1, pp 74-86, Springer, 2005.

  4. Stefan Blom and Simona Orzan. Distributed State Space Minimization Early version: Proceedings FMICS'03 (Roros, Norway), Electronic Notes in Theoretical Computer Science (ENTCS), vol. 80, Elsevier, Jun. 2003. Full version: Software Tools for Technology Transfer (STTT), vol. 7, num. 3, Springer, 2005.

  5. Stefan Blom, Izak van Langevelde, and Bert Lisser. Compressed and Distributed File Formats for Labeled Transition Systems. Proceedings PDMC'03 (Boulder, Colorado, USA), Electronic Notes in Theoretical Computer Science (ENTCS), vol. 89, num. 1, Elsevier, 2003.

  6. María del Mar Gallardo, Christophe Joubert and Pedro Merino. On-the-Fly Data Flow Analysis based on Verification Technology. Proceedings of the 6th International Workshop on Compiler Optimization meets Compiler Verification COCV'2007 (Braga, Portugal), Mar 2007.

  7. María del Mar Gallardo, Christophe Joubert, Pedro Merino and David Sanán. C.OPEN and ANNOTATOR: Tools for On-the-Fly Model Checking C Programs. Proceedings of the 14th International SPIN Workshop on Model Checking of Software SPIN'07 (Berlin, Germany), Jul 2007.

  8. Hubert Garavel, Radu Mateescu, Damien Bergamini, Adrian Curic, Nicolas Descoubes, Christophe Joubert, Irina Smarandache-Sturm and Gilles Stragier. DISTRIBUTOR and BCG_MERGE: Tools for Distributed Explicit State Space Generat ion. Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2006 (Vienna, Austria), volume 3920 of Lecture Notes in Computer Science, pp. 445-449. Springer Verlag, March-April 2006.

  9. Jan Friso Groote and Frank van Ham. Interactive Visualization of Large State Spaces. Early version: Eindhoven University of Technology, Department of Computer Science, CS-Report 02-14, 2002. Full version: Software Tools for Technology Transfer (STTT), vol. 8, num. 1, pp. 77-91, 2006.

  10. Fredrik Holmén, Martin Leucker, and Marcus Lindstrom. UppDMC: A Distributed Model Checker for Fragments of the mu-Calculus. Proceedings PDMC'04 (London, U.K.), Electronic Notes in Theoretical Computer Science (ENTCS), Sept. 2004.

  11. Katia Hristova, Yanhong A. Liu, and K. Tuncay Tekle. Generating Specialized Rules and Programs for Demand-Driven Analysis. Proceedings of the 12th international conference on Algebraic Methodology and Software Technology, AMAST 2008 (Urbana, IL, USA), Jul. 2008.

  12. Christophe Joubert and Radu Mateescu. Distributed On-the-Fly Equivalence Checking. Proceedings PDMC'04 (London, U.K.), Electronic Notes in Theoretical Computer Sci ence (ENTCS), Sept. 2004.

  13. Christophe Joubert and Radu Mateescu. Distributed On-the-Fly Model Checking and Test Case Generation. Proceedings of SPIN'2006 (Vienna, Austria), LNCS 3923, pp 126-145, April 2006.

  14. Yanhong A. Liu, Tom Rothamel, Fuxiang Yu, Scott D. Stoller, and Nanjun Hu. Parametric Regular Path Queries. Proceedings of PLDI'2004, ACM SIGPLAN Notices, vol. 39, num. 6, May 2004.

  15. Carla Piazza and Alberto Policriti. Ackermann Encoding, Bisimulations, and OBDDs. Full version: Theory and Practice of Logic Programming (TPLP) vol. 4, num. 5-6, pp 695-718, 2004.

  16. Simona Orzan. On Distributed Verification and Verified Distribution. PhD thesis, defended on November 25, 2004, at the Free University of Amsterdam.

  17. Johan Oudinet Uniform Random Walks in Very Large Models. Proceedings of the 2nd International Workshop on Random Testing RT'07, pp. 26-29, Atlanta, GA, USA, November 2007. ACM Press.

  18. Francesco Ranzato and Francesco Tapparo. Generalizing the Paige-Tarjan Algorithm by Abstract Interpretation. Information and Computation, vol. 206, num. 5, pp. 620-651, 2008.

See also:

Version 1.45 - Last updated 09/12/04 12:45:25

Back to the VASY Home Page