Symbolic Reachability for Process Algebras with Recursive Data Types

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

    17 Citations (Scopus)
    64 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 languageUndefined
    Title of host publicationTheoretical Aspects of Computing - ICTAC 2008
    EditorsJ.S. Fitzgerald, A.E. Haxthausen, H. Yenigun
    Place of PublicationBerlin
    PublisherSpringer
    Pages81-95
    Number of pages15
    ISBN (Print)978-3-540-85761-7
    DOIs
    Publication statusPublished - 25 Aug 2008

    Publication series

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

    Keywords

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

    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). Berlin: Springer. https://doi.org/10.1007/978-3-540-85762-4_6