Symbolic Reachability for Process Algebras with Recursive Data Types


Share/Save/Bookmark

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
555kB
[img]
Preview
PDF (Author's version)
220kB
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
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/62465
Official URL:http://dx.doi.org/10.1007/978-3-540-85762-4_6
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page

Metis ID: 251187