Symbolic Reachability for Process Algebras with Recursive Data Types

Stefan Blom; Jan Cornelis van de Pol

doi:10.1007/978-3-540-85762-4_6

Symbolic Reachability for Process Algebras with Recursive Data Types

Stefan Blom, Jan Cornelis van de Pol

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

19 Citations (Scopus)

163 Downloads (Pure)

Abstract

In this paper, we present a symbolic reachability algorithm for process algebras with recursive data types. Like the various saturation based algorithms of Ciardo et al, the algorithm is based on partitioning of the transition relation into events whose influence is local. As new features, our algorithm supports recursive data types and allows unbounded non-determinism, which is needed to support open systems with data. The algorithm does not use any specific features of process algebras. That is, it will work for any system that consists of a fixed number of communicating processes, where in each atomic step only a subset of the processes participate. As proof of concept we have implemented the algorithm in the context of the μCRL toolset. We also compared the performance of this prototype with the performance of the existing explicit tools on a set of typical case studies.

Original language	Undefined
Title of host publication	Theoretical Aspects of Computing - ICTAC 2008
Editors	J.S. Fitzgerald, A.E. Haxthausen, H. Yenigun
Place of Publication	Berlin
Publisher	Springer
Pages	81-95
Number of pages	15
ISBN (Print)	978-3-540-85761-7
DOIs	https://doi.org/10.1007/978-3-540-85762-4_6
Publication status	Published - 25 Aug 2008
Event	5th International Colloquium on Theoretical Aspects of Computing, ICTAC 2008 - Istanbul, Turkey Duration: 1 Sept 2008 → 3 Sept 2008

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Verlag
Number	Supplement
Volume	5160
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	5th International Colloquium on Theoretical Aspects of Computing, ICTAC 2008
Period	1/09/08 → 3/09/08
Other	1-3 September 2008

Keywords

EWI-13443
FMT-MC: MODEL CHECKING
METIS-251187
EC Grant Agreement nr.: FP6/043235
IR-62465

Access to Document

10.1007/978-3-540-85762-4_6

http://eprints.eemcs.utwente.nl/secure2/13443/01/ictac_springer.pdf

Cite this

Blom, S., & van de Pol, J. C. (2008). Symbolic Reachability for Process Algebras with Recursive Data Types. In J. S. Fitzgerald, A. E. Haxthausen, & H. Yenigun (Eds.), Theoretical Aspects of Computing - ICTAC 2008 (pp. 81-95). [10.1007/978-3-540-85762-4_6] (Lecture Notes in Computer Science; Vol. 5160, No. Supplement). Springer. https://doi.org/10.1007/978-3-540-85762-4_6

@inproceedings{aeb54cddd5b248b383cf4a7222749107,

title = "Symbolic Reachability for Process Algebras with Recursive Data Types",

abstract = "In this paper, we present a symbolic reachability algorithm for process algebras with recursive data types. Like the various saturation based algorithms of Ciardo et al, the algorithm is based on partitioning of the transition relation into events whose influence is local. As new features, our algorithm supports recursive data types and allows unbounded non-determinism, which is needed to support open systems with data. The algorithm does not use any specific features of process algebras. That is, it will work for any system that consists of a fixed number of communicating processes, where in each atomic step only a subset of the processes participate. As proof of concept we have implemented the algorithm in the context of the μCRL toolset. We also compared the performance of this prototype with the performance of the existing explicit tools on a set of typical case studies.",

keywords = "EWI-13443, FMT-MC: MODEL CHECKING, METIS-251187, EC Grant Agreement nr.: FP6/043235, IR-62465",

author = "Stefan Blom and {van de Pol}, {Jan Cornelis}",

note = "10.1007/978-3-540-85762-4_6 ; 5th International Colloquium on Theoretical Aspects of Computing, ICTAC 2008 ; Conference date: 01-09-2008 Through 03-09-2008",

year = "2008",

month = aug,

day = "25",

doi = "10.1007/978-3-540-85762-4_6",

language = "Undefined",

isbn = "978-3-540-85761-7",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

number = "Supplement",

pages = "81--95",

editor = "J.S. Fitzgerald and A.E. Haxthausen and H. Yenigun",

booktitle = "Theoretical Aspects of Computing - ICTAC 2008",

}

Blom, S & van de Pol, JC 2008, Symbolic Reachability for Process Algebras with Recursive Data Types. in JS Fitzgerald, AE Haxthausen & H Yenigun (eds), Theoretical Aspects of Computing - ICTAC 2008., 10.1007/978-3-540-85762-4_6, Lecture Notes in Computer Science, no. Supplement, vol. 5160, Springer, Berlin, pp. 81-95, 5th International Colloquium on Theoretical Aspects of Computing, ICTAC 2008, 1/09/08. https://doi.org/10.1007/978-3-540-85762-4_6

Symbolic Reachability for Process Algebras with Recursive Data Types. / Blom, Stefan; van de Pol, Jan Cornelis.
Theoretical Aspects of Computing - ICTAC 2008. ed. / J.S. Fitzgerald; A.E. Haxthausen; H. Yenigun. Berlin: Springer, 2008. p. 81-95 10.1007/978-3-540-85762-4_6 (Lecture Notes in Computer Science; Vol. 5160, No. Supplement).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Symbolic Reachability for Process Algebras with Recursive Data Types

AU - Blom, Stefan

AU - van de Pol, Jan Cornelis

N1 - 10.1007/978-3-540-85762-4_6

PY - 2008/8/25

Y1 - 2008/8/25

N2 - In this paper, we present a symbolic reachability algorithm for process algebras with recursive data types. Like the various saturation based algorithms of Ciardo et al, the algorithm is based on partitioning of the transition relation into events whose influence is local. As new features, our algorithm supports recursive data types and allows unbounded non-determinism, which is needed to support open systems with data. The algorithm does not use any specific features of process algebras. That is, it will work for any system that consists of a fixed number of communicating processes, where in each atomic step only a subset of the processes participate. As proof of concept we have implemented the algorithm in the context of the μCRL toolset. We also compared the performance of this prototype with the performance of the existing explicit tools on a set of typical case studies.

AB - In this paper, we present a symbolic reachability algorithm for process algebras with recursive data types. Like the various saturation based algorithms of Ciardo et al, the algorithm is based on partitioning of the transition relation into events whose influence is local. As new features, our algorithm supports recursive data types and allows unbounded non-determinism, which is needed to support open systems with data. The algorithm does not use any specific features of process algebras. That is, it will work for any system that consists of a fixed number of communicating processes, where in each atomic step only a subset of the processes participate. As proof of concept we have implemented the algorithm in the context of the μCRL toolset. We also compared the performance of this prototype with the performance of the existing explicit tools on a set of typical case studies.

KW - EWI-13443

KW - FMT-MC: MODEL CHECKING

KW - METIS-251187

KW - EC Grant Agreement nr.: FP6/043235

KW - IR-62465

U2 - 10.1007/978-3-540-85762-4_6

DO - 10.1007/978-3-540-85762-4_6

M3 - Conference contribution

SN - 978-3-540-85761-7

T3 - Lecture Notes in Computer Science

SP - 81

EP - 95

BT - Theoretical Aspects of Computing - ICTAC 2008

A2 - Fitzgerald, J.S.

A2 - Haxthausen, A.E.

A2 - Yenigun, H.

PB - Springer

CY - Berlin

T2 - 5th International Colloquium on Theoretical Aspects of Computing, ICTAC 2008

Y2 - 1 September 2008 through 3 September 2008

ER -