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

Jan Friso Groote; Kevin H.J. Jilissen; Maurice Laveaux; P. H.M. van Spaendonck; Tim A.C. Willemse

doi:10.1007/978-3-031-15629-8_16

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

Jan Friso Groote, Kevin H.J. Jilissen, Maurice Laveaux, P. H.M. van Spaendonck, Tim A.C. Willemse

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/Congresprocedure › Hoofdstuk › Academic › peer review

1 Citaat (Scopus)

Samenvatting

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.

Originele taal-2	Engels
Titel	A Journey from Process Algebra via Timed Automata to Model Learning
Redacteuren	Nils Jansen, Mariëlle Stoelinga, Petra van den Bos
Uitgeverij	Springer
Pagina's	306-320
Aantal pagina's	15
ISBN van elektronische versie	978-3-031-15629-8
ISBN van geprinte versie	978-3-031-15628-1
DOI's	https://doi.org/10.1007/978-3-031-15629-8_16
Status	Gepubliceerd - 2022

Publicatie series

Naam	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	13560 LNCS
ISSN van geprinte versie	0302-9743
ISSN van elektronische versie	1611-3349

Bibliografische nota

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

Toegang tot document

10.1007/978-3-031-15629-8_16

Andere bestanden en links

Link naar publicatie in Scopus

Citeer dit

Groote, J. F., Jilissen, K. H. J., Laveaux, M., van Spaendonck, P. H. M., & Willemse, T. A. C. (2022). Using the Parallel ATerm Library for Parallel Model Checking and State Space Generation. In N. Jansen, M. Stoelinga, & P. van den Bos (editors), A Journey from Process Algebra via Timed Automata to Model Learning (blz. 306-320). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 13560 LNCS). Springer. https://doi.org/10.1007/978-3-031-15629-8_16

Groote, Jan Friso ; Jilissen, Kevin H.J. ; Laveaux, Maurice et al. / Using the Parallel ATerm Library for Parallel Model Checking and State Space Generation. A Journey from Process Algebra via Timed Automata to Model Learning. redacteur / Nils Jansen ; Mariëlle Stoelinga ; Petra van den Bos. Springer, 2022. blz. 306-320 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inbook{2d5d5a73d2fd493db739507d67147957,

title = "Using the Parallel ATerm Library for Parallel Model Checking and State Space Generation",

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

keywords = "A parallel ATerm library, Parallel model checking, Parallel state space generation, The mCRL2 toolset",

author = "Groote, {Jan Friso} and Jilissen, {Kevin H.J.} and Maurice Laveaux and {van Spaendonck}, {P. H.M.} and Willemse, {Tim A.C.}",

note = "Funding Information: Partially supported by the projects 612.001.751 (NWO, AVVA) and 00795160 (TTW, MASCOT). Publisher Copyright: {\textcopyright} 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.",

year = "2022",

doi = "10.1007/978-3-031-15629-8_16",

language = "English",

isbn = "978-3-031-15628-1",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "306--320",

editor = "Nils Jansen and Mari{\"e}lle Stoelinga and {van den Bos}, Petra",

booktitle = "A Journey from Process Algebra via Timed Automata to Model Learning",

address = "Germany",

}

Groote, JF , Jilissen, KHJ , Laveaux, M , van Spaendonck, PHM & Willemse, TAC 2022, Using the Parallel ATerm Library for Parallel Model Checking and State Space Generation. in N Jansen, M Stoelinga & P van den Bos (uitgave), A Journey from Process Algebra via Timed Automata to Model Learning. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 13560 LNCS, Springer, blz. 306-320. https://doi.org/10.1007/978-3-031-15629-8_16

Using the Parallel ATerm Library for Parallel Model Checking and State Space Generation. / Groote, Jan Friso ; Jilissen, Kevin H.J.; Laveaux, Maurice et al.
A Journey from Process Algebra via Timed Automata to Model Learning. uitgave / Nils Jansen; Mariëlle Stoelinga; Petra van den Bos. Springer, 2022. blz. 306-320 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 13560 LNCS).

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/Congresprocedure › Hoofdstuk › Academic › peer review

TY - CHAP

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

AU - Groote, Jan Friso

AU - Jilissen, Kevin H.J.

AU - Laveaux, Maurice

AU - van Spaendonck, P. H.M.

AU - Willemse, Tim A.C.

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

PY - 2022

Y1 - 2022

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

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

KW - A parallel ATerm library

KW - Parallel model checking

KW - Parallel state space generation

KW - The mCRL2 toolset

UR - http://www.scopus.com/inward/record.url?scp=85138132634&partnerID=8YFLogxK

U2 - 10.1007/978-3-031-15629-8_16

DO - 10.1007/978-3-031-15629-8_16

M3 - Chapter

AN - SCOPUS:85138132634

SN - 978-3-031-15628-1

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 306

EP - 320

BT - A Journey from Process Algebra via Timed Automata to Model Learning

A2 - Jansen, Nils

A2 - Stoelinga, Mariëlle

A2 - van den Bos, Petra

PB - Springer

ER -

Groote JF , Jilissen KHJ , Laveaux M , van Spaendonck PHM , Willemse TAC. Using the Parallel ATerm Library for Parallel Model Checking and State Space Generation. In Jansen N, Stoelinga M, van den Bos P, redacteurs, A Journey from Process Algebra via Timed Automata to Model Learning. Springer. 2022. blz. 306-320. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-031-15629-8_16