Using the Parallel ATerm Library for Parallel Model Checking and State Space Generation

Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

1 Citation (Scopus)

Abstract

Process algebras are used to study the behaviour of parallel systems. The mCRL2 toolset has been designed to analyse process algebraic models of such systems. Given that almost any contemporary desktop computer has multiple processors on board it seems natural that a toolset to analyse parallel behaviour now also employs parallelism. This paper gives a compact account of the recently developed parallel term library [13]; terms are used to represent almost any main concept in the mCRL2 toolset. It subsequently reports on how the library is used to make parallel implementations of the generation of state spaces and the instantiation of Parameterised Boolean Equation Systems (PBES). We show that a gain of an order of magnitude is possible using parallel processing on contemporary hardware.

Original languageEnglish
Title of host publicationA Journey from Process Algebra via Timed Automata to Model Learning
EditorsNils Jansen, Mariëlle Stoelinga, Petra van den Bos
PublisherSpringer
Pages306-320
Number of pages15
ISBN (Electronic)978-3-031-15629-8
ISBN (Print)978-3-031-15628-1
DOIs
Publication statusPublished - 2022

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume13560 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Bibliographical note

Funding Information:
Partially supported by the projects 612.001.751 (NWO, AVVA) and 00795160 (TTW, MASCOT).

Publisher Copyright:
© 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.

Funding

Partially supported by the projects 612.001.751 (NWO, AVVA) and 00795160 (TTW, MASCOT).

Keywords

  • A parallel ATerm library
  • Parallel model checking
  • Parallel state space generation
  • The mCRL2 toolset

Fingerprint

Dive into the research topics of 'Using the Parallel ATerm Library for Parallel Model Checking and State Space Generation'. Together they form a unique fingerprint.

Cite this