Symbolic Reachability for Process Algebras with Recursive Data Types

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    19 Citations (Scopus)
    163 Downloads (Pure)


    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 languageUndefined
    Title of host publicationTheoretical Aspects of Computing - ICTAC 2008
    EditorsJ.S. Fitzgerald, A.E. Haxthausen, H. Yenigun
    Place of PublicationBerlin
    Number of pages15
    ISBN (Print)978-3-540-85761-7
    Publication statusPublished - 25 Aug 2008
    Event5th International Colloquium on Theoretical Aspects of Computing, ICTAC 2008 - Istanbul, Turkey
    Duration: 1 Sept 20083 Sept 2008

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349


    Conference5th International Colloquium on Theoretical Aspects of Computing, ICTAC 2008
    Other1-3 September 2008


    • EWI-13443
    • METIS-251187
    • EC Grant Agreement nr.: FP6/043235
    • IR-62465

    Cite this