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

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. 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.

  2. 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.

  3. 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.

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

  5. 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.

  6. 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.

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

  8. 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.

  9. 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.

  10. 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, Mar.-Apr. 2006.

  11. 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.

  12. 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, Apr. 2006.

  13. 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.

  14. 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.

  15. 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

  16. 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, Nov. 2007. ACM Press.

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

  18. 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 So ftware Technology, AMAST 2008 (Urbana, IL, USA), Jul. 2008.

  19. Radu Mateescu and Anton Wijs. Efficient On-the-Fly Computation of Weak Tau-Confluence. INRIA Research Report RR-7000, Jul. 2009.

  20. Johan Oudinet Exploration aléatoire de modèles. Journal Européen des Systèmes Automatisés, vol. 43, num. 7-9, pp.905-919, 2009.

  21. Silvia Crafa, Francesco Ranzato, and Francesco Tapparo. Saving Space in a Time Efficient Simulation Algorithm. Proceedings of the 9th International Conference on Application of Concurrency to System Design (ACSD'09), pp. 60-69, 2009. IEEE Computer Society.

  22. Weisong Li. Algorithms for Computing Weak Bisimulation Equivalence. Proceedings of the 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE'09), Jul. 2009.

  23. Radu Mateescu and Anton Wijs. Hierarchical Adaptive State Space Caching Based on Level Sampling. Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'09), York, UK, Mar. 2009.

  24. Johan Oudinet, Alain Denise, and Marie-Claude Gaudel. A New Dichotomic Algorithm for the Uniform Random Generation of Words in Regular Languages. Proceedings of the Conference on Random and Exhaustive Generation of Combinatorial Objects (GASCom), Montreal, Canada, Sept. 2010. Journal version: Theoretical Computer Science, available online Aug. 2012.

  25. Francesco Ranzato and Francesco Tapparo. An Efficient Simulation Algorithm based on Abstract Interpretation. Information and Computation, vol. 208, issue 1, pp. 1-22, 2010.

  26. Lubos Brim, Jaco van de Pol, Hidde de Jong, and Radu Mateescu. Distributed Model Checking Algorithms Devised and Implemented. Deliverable D3-4 of the European project EC-MOAN, 2010.

  27. Johan Oudinet. Approches combinatoires pour le test statistique à grande échelle. Thèse de doctorat, Université Paris-Sud 11, France, Nov. 2010. English summary available as: Johan Oudinet, Random Exploration of Models, Research Report 1534, Laboratoire de Recherche en Informatique, Orsay, France.

  28. Jakub Chaloupka. Algorithms for Mean-Payoff and Energy Games. PhD thesis, Faculty of Informatics, Masaryk University, Brno, Czech Republic, Feb. 2011.

  29. Jirí Barnat, Jakub Chaloupka, and Jaco van de Pol. Distributed algorithms for SCC Decomposition. Journal of Logic and Computation, vol. 21, num. 1, pp. 23-44. Oxford University Press, 2011.

  30. Marie-Claude Gaudel. Counting for Random Testing. Proceedings of the 23rd IFIP WG 6.1 International Conference on Testing Software and Systems (ICTSS'11), Paris, France, Nov. 2011.

  31. Maria del Mar Gallardo, Christophe Joubert, Pedro Merino, and David Sanán. A Model-extraction Approach to Verifying Concurrent C Programs with CADP. Science of Computer Programming, vol. 77, num. 3, pp. 375-392, Mar. 2012.

  32. Alain Denise, Marie-Claude Gaudel, Sandrine-Dominique Gouraud, Richard Lassaigne, Johan Oudinet, and Sylvain Peyronnet. Coverage-biased Random Exploration of Large Models and Application to Testing. Software Tools for Technology Transfer, vol. 14, num. 1, pp. 73-93, 2012.

  33. Alexander Ditter, Milan Ceska, and Gerald Lüttgen. On Parallel Software Verification Using Boolean Equation Systems. Proceedings of the 19th International Workshop on Model Checking Software (SPIN'12), Oxford, UK, Jul. 2012.

  34. Radu Mateescu and Anton Wijs. Sequential and Distributed On-the-fly Computation of Weak Tau-confluence. Science of Computer Programming, vol. 77, num. 10-11, pp. 1075-1094, Sep. 2012.

  35. Javier Cámara, Gwen Salaün, Carlos Canal, and Meriem Ouederni. Interactive specification and verification of behavioral adaptation contracts. Information and Software Technology, vol. 54, num. 7, pp. 701-723, 2012.

  36. Rafal Somla. Logics and Algorithms for Verification of Concurrent Systems. PhD dissertation presented at Uppsala University, Faculty of Science and Technology, Oct. 2012.

  37. Gérard Cécé. Three Simulation Algorithms for Labelled Transition Systems. The Computing Research Repository (CoRR), 1301.1638 (2013).

  38. Konrad Kulakowski Concurrent Bisimulation Algorithm. arXiv:1311.7635 [cs.LO], Jan. 2014.

See also:


Version 1.67 - Last updated 2014/04/06 20:01:09

Back to the CADP Home Page