Symbolic Reachability for Process Algebras with Recursive Data Types


Blom, Stefan and Pol, Jaco van de (2008) Symbolic Reachability for Process Algebras with Recursive Data Types. In: 5th International Colloquium on Theoretical Aspects of Computing, ICTAC 2008, 1-3 September 2008, Istanbul, Turkey (pp. pp. 81-95).

[img] PDF (Publisher's version)
Restricted to UT campus only
: Request a copy
PDF (Author's version)
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.
Item Type:Conference or Workshop Item
Copyright:© 2008 Springer
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:
Official URL:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page

Metis ID: 251187