Symbolic Reachability for Process Algebras with Recursive Data Types

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

    17 Citations (Scopus)
    57 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
    Blom, Stefan ; van de Pol, Jan Cornelis. / Symbolic Reachability for Process Algebras with Recursive Data Types. Theoretical Aspects of Computing - ICTAC 2008. editor / J.S. Fitzgerald ; A.E. Haxthausen ; H. Yenigun. Berlin : Springer, 2008. pp. 81-95 (Lecture Notes in Computer Science; Supplement).
    @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",
    year = "2008",
    month = "8",
    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. 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 proceedingConference contributionAcademicpeer-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

    ER -

    Blom S, van de Pol JC. Symbolic Reachability for Process Algebras with Recursive Data Types. In Fitzgerald JS, Haxthausen AE, Yenigun H, editors, Theoretical Aspects of Computing - ICTAC 2008. Berlin: Springer. 2008. p. 81-95. 10.1007/978-3-540-85762-4_6. (Lecture Notes in Computer Science; Supplement). https://doi.org/10.1007/978-3-540-85762-4_6