Distributed Graph-Based State Space Generation

Stefan Blom, Gijs Kant, Arend Rensink

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

2 Citations (Scopus)
15 Downloads (Pure)

Abstract

LTSMIN provides a framework in which state space generation can be distributed easily over many cores on a single compute node, as well as over multiple compute nodes. The tool works on the basis of a vector representation of the states; the individual cores are assigned the task of computing all successors of states that are sent to them. In this paper we show how this framework can be applied in the case where states are essentially graphs interpreted up to isomorphism, such as the ones we have been studying for GROOVE. This involves developing a suitable vector representation for a canonical form of those graphs. The canonical forms are computed using a third tool called BLISS. We combined the three tools to form a system for distributed state space generation based on graph grammars. We show that the time performance of the resulting system scales well (i.e., close to linear) with the number of cores. We also report surprising statistics on the memory consumption, which imply that the vector representation used to store graphs in LTSMIN is more compact than the representation used in GROOVE.
Original languageUndefined
Title of host publicationProceedings of the Fourth International Workshop on Graph-Based Tools (GraBaTs 2010)
EditorsJ. De Lara, D. Varro
Place of PublicationBerlin
PublisherEuropean Association of Software Science and Technology (EASST)
Pages8
Number of pages12
Publication statusPublished - Sep 2010
EventFourth International Workshop on Graph-Based Tools, GraBaTs 2010: Proceedings of the Fourth International Workshop on Graph-Based Tools (GraBaTs 2010) - University of Twente, Enschede, Netherlands
Duration: 28 Sep 201028 Sep 2010
Conference number: 4

Publication series

NameElectronic Communications of the EASST
PublisherEuropean Association of Software Science and Technology (EASST)
NumberWP 10-06
Volume32
ISSN (Print)1863-2122
ISSN (Electronic)0929-0672

Conference

ConferenceFourth International Workshop on Graph-Based Tools, GraBaTs 2010
Abbreviated titleGraBaTs 2010
CountryNetherlands
CityEnschede
Period28/09/1028/09/10
Other28 September 2010

Keywords

  • IR-75906
  • METIS-275864
  • Symmetry Reduction
  • State Space Generation
  • EWI-19393
  • Graph Transformation
  • Distributed Computing
  • GROOVE
  • CR-D.2.4
  • LTSMIN

Cite this

Blom, S., Kant, G., & Rensink, A. (2010). Distributed Graph-Based State Space Generation. In J. De Lara, & D. Varro (Eds.), Proceedings of the Fourth International Workshop on Graph-Based Tools (GraBaTs 2010) (pp. 8). (Electronic Communications of the EASST; Vol. 32, No. WP 10-06). Berlin: European Association of Software Science and Technology (EASST).
Blom, Stefan ; Kant, Gijs ; Rensink, Arend. / Distributed Graph-Based State Space Generation. Proceedings of the Fourth International Workshop on Graph-Based Tools (GraBaTs 2010). editor / J. De Lara ; D. Varro. Berlin : European Association of Software Science and Technology (EASST), 2010. pp. 8 (Electronic Communications of the EASST; WP 10-06).
@inproceedings{a096124b1bf4469a9280c3f337de2077,
title = "Distributed Graph-Based State Space Generation",
abstract = "LTSMIN provides a framework in which state space generation can be distributed easily over many cores on a single compute node, as well as over multiple compute nodes. The tool works on the basis of a vector representation of the states; the individual cores are assigned the task of computing all successors of states that are sent to them. In this paper we show how this framework can be applied in the case where states are essentially graphs interpreted up to isomorphism, such as the ones we have been studying for GROOVE. This involves developing a suitable vector representation for a canonical form of those graphs. The canonical forms are computed using a third tool called BLISS. We combined the three tools to form a system for distributed state space generation based on graph grammars. We show that the time performance of the resulting system scales well (i.e., close to linear) with the number of cores. We also report surprising statistics on the memory consumption, which imply that the vector representation used to store graphs in LTSMIN is more compact than the representation used in GROOVE.",
keywords = "IR-75906, METIS-275864, Symmetry Reduction, State Space Generation, EWI-19393, Graph Transformation, Distributed Computing, GROOVE, CR-D.2.4, LTSMIN",
author = "Stefan Blom and Gijs Kant and Arend Rensink",
note = "Fourth International Workshop on Graph-Based Tools (GraBaTs 2010), Enschede, The Netherlands, 28 September 2010",
year = "2010",
month = "9",
language = "Undefined",
series = "Electronic Communications of the EASST",
publisher = "European Association of Software Science and Technology (EASST)",
number = "WP 10-06",
pages = "8",
editor = "{De Lara}, J. and D. Varro",
booktitle = "Proceedings of the Fourth International Workshop on Graph-Based Tools (GraBaTs 2010)",

}

Blom, S, Kant, G & Rensink, A 2010, Distributed Graph-Based State Space Generation. in J De Lara & D Varro (eds), Proceedings of the Fourth International Workshop on Graph-Based Tools (GraBaTs 2010). Electronic Communications of the EASST, no. WP 10-06, vol. 32, European Association of Software Science and Technology (EASST), Berlin, pp. 8, Fourth International Workshop on Graph-Based Tools, GraBaTs 2010, Enschede, Netherlands, 28/09/10.

Distributed Graph-Based State Space Generation. / Blom, Stefan; Kant, Gijs; Rensink, Arend.

Proceedings of the Fourth International Workshop on Graph-Based Tools (GraBaTs 2010). ed. / J. De Lara; D. Varro. Berlin : European Association of Software Science and Technology (EASST), 2010. p. 8 (Electronic Communications of the EASST; Vol. 32, No. WP 10-06).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - Distributed Graph-Based State Space Generation

AU - Blom, Stefan

AU - Kant, Gijs

AU - Rensink, Arend

N1 - Fourth International Workshop on Graph-Based Tools (GraBaTs 2010), Enschede, The Netherlands, 28 September 2010

PY - 2010/9

Y1 - 2010/9

N2 - LTSMIN provides a framework in which state space generation can be distributed easily over many cores on a single compute node, as well as over multiple compute nodes. The tool works on the basis of a vector representation of the states; the individual cores are assigned the task of computing all successors of states that are sent to them. In this paper we show how this framework can be applied in the case where states are essentially graphs interpreted up to isomorphism, such as the ones we have been studying for GROOVE. This involves developing a suitable vector representation for a canonical form of those graphs. The canonical forms are computed using a third tool called BLISS. We combined the three tools to form a system for distributed state space generation based on graph grammars. We show that the time performance of the resulting system scales well (i.e., close to linear) with the number of cores. We also report surprising statistics on the memory consumption, which imply that the vector representation used to store graphs in LTSMIN is more compact than the representation used in GROOVE.

AB - LTSMIN provides a framework in which state space generation can be distributed easily over many cores on a single compute node, as well as over multiple compute nodes. The tool works on the basis of a vector representation of the states; the individual cores are assigned the task of computing all successors of states that are sent to them. In this paper we show how this framework can be applied in the case where states are essentially graphs interpreted up to isomorphism, such as the ones we have been studying for GROOVE. This involves developing a suitable vector representation for a canonical form of those graphs. The canonical forms are computed using a third tool called BLISS. We combined the three tools to form a system for distributed state space generation based on graph grammars. We show that the time performance of the resulting system scales well (i.e., close to linear) with the number of cores. We also report surprising statistics on the memory consumption, which imply that the vector representation used to store graphs in LTSMIN is more compact than the representation used in GROOVE.

KW - IR-75906

KW - METIS-275864

KW - Symmetry Reduction

KW - State Space Generation

KW - EWI-19393

KW - Graph Transformation

KW - Distributed Computing

KW - GROOVE

KW - CR-D.2.4

KW - LTSMIN

M3 - Conference contribution

T3 - Electronic Communications of the EASST

SP - 8

BT - Proceedings of the Fourth International Workshop on Graph-Based Tools (GraBaTs 2010)

A2 - De Lara, J.

A2 - Varro, D.

PB - European Association of Software Science and Technology (EASST)

CY - Berlin

ER -

Blom S, Kant G, Rensink A. Distributed Graph-Based State Space Generation. In De Lara J, Varro D, editors, Proceedings of the Fourth International Workshop on Graph-Based Tools (GraBaTs 2010). Berlin: European Association of Software Science and Technology (EASST). 2010. p. 8. (Electronic Communications of the EASST; WP 10-06).