Equivalence Checking for Infinite Systems Using Parameterized Boolean Equation Systems

T. Chen, Bas Ploeger, Jan Cornelis van de Pol, Tim A.C. Willemse

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

    27 Citations (Scopus)

    Abstract

    In this paper, we provide a transformation from the branching bisimulation problem for infinite, concurrent, data-intensive systems in linear process format, into solving Parameterized Boolean Equation Systems. We prove correctness, and illustrate the approach with an unbounded queue example. We also provide some adaptations to obtain similar transformations for weak bisimulation and simulation equivalence.
    Original languageUndefined
    Title of host publicationCONCUR 2007 - Concurrency Theory
    EditorsLuis Caires, Vasco T. Vasconcelos
    Place of PublicationBerlin
    PublisherSpringer
    Pages120-135
    Number of pages16
    ISBN (Print)978-3-540-74406-1
    DOIs
    Publication statusPublished - Sep 2007
    Event18th International Conference on Concurrency Theory, CONCUR 2007 - Lisbon, Portugal
    Duration: 3 Sep 20078 Sep 2007
    Conference number: 18

    Publication series

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

    Conference

    Conference18th International Conference on Concurrency Theory, CONCUR 2007
    Abbreviated titleCONCUR
    CountryPortugal
    CityLisbon
    Period3/09/078/09/07

    Keywords

    • FMT-MC: MODEL CHECKING
    • METIS-242021
    • IR-61980
    • EWI-11289

    Cite this

    Chen, T., Ploeger, B., van de Pol, J. C., & Willemse, T. A. C. (2007). Equivalence Checking for Infinite Systems Using Parameterized Boolean Equation Systems. In L. Caires, & V. T. Vasconcelos (Eds.), CONCUR 2007 - Concurrency Theory (pp. 120-135). [10.1007/978-3-540-74407-8_9] (Lecture Notes in Computer Science; Vol. 4703, No. LNCS4549). Berlin: Springer. https://doi.org/10.1007/978-3-540-74407-8_9
    Chen, T. ; Ploeger, Bas ; van de Pol, Jan Cornelis ; Willemse, Tim A.C. / Equivalence Checking for Infinite Systems Using Parameterized Boolean Equation Systems. CONCUR 2007 - Concurrency Theory. editor / Luis Caires ; Vasco T. Vasconcelos. Berlin : Springer, 2007. pp. 120-135 (Lecture Notes in Computer Science; LNCS4549).
    @inproceedings{57c849ad1fd0423cb35121a34d582feb,
    title = "Equivalence Checking for Infinite Systems Using Parameterized Boolean Equation Systems",
    abstract = "In this paper, we provide a transformation from the branching bisimulation problem for infinite, concurrent, data-intensive systems in linear process format, into solving Parameterized Boolean Equation Systems. We prove correctness, and illustrate the approach with an unbounded queue example. We also provide some adaptations to obtain similar transformations for weak bisimulation and simulation equivalence.",
    keywords = "FMT-MC: MODEL CHECKING, METIS-242021, IR-61980, EWI-11289",
    author = "T. Chen and Bas Ploeger and {van de Pol}, {Jan Cornelis} and Willemse, {Tim A.C.}",
    note = "10.1007/978-3-540-74407-8_9",
    year = "2007",
    month = "9",
    doi = "10.1007/978-3-540-74407-8_9",
    language = "Undefined",
    isbn = "978-3-540-74406-1",
    series = "Lecture Notes in Computer Science",
    publisher = "Springer",
    number = "LNCS4549",
    pages = "120--135",
    editor = "Luis Caires and Vasconcelos, {Vasco T.}",
    booktitle = "CONCUR 2007 - Concurrency Theory",

    }

    Chen, T, Ploeger, B, van de Pol, JC & Willemse, TAC 2007, Equivalence Checking for Infinite Systems Using Parameterized Boolean Equation Systems. in L Caires & VT Vasconcelos (eds), CONCUR 2007 - Concurrency Theory., 10.1007/978-3-540-74407-8_9, Lecture Notes in Computer Science, no. LNCS4549, vol. 4703, Springer, Berlin, pp. 120-135, 18th International Conference on Concurrency Theory, CONCUR 2007, Lisbon, Portugal, 3/09/07. https://doi.org/10.1007/978-3-540-74407-8_9

    Equivalence Checking for Infinite Systems Using Parameterized Boolean Equation Systems. / Chen, T.; Ploeger, Bas; van de Pol, Jan Cornelis; Willemse, Tim A.C.

    CONCUR 2007 - Concurrency Theory. ed. / Luis Caires; Vasco T. Vasconcelos. Berlin : Springer, 2007. p. 120-135 10.1007/978-3-540-74407-8_9 (Lecture Notes in Computer Science; Vol. 4703, No. LNCS4549).

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

    TY - GEN

    T1 - Equivalence Checking for Infinite Systems Using Parameterized Boolean Equation Systems

    AU - Chen, T.

    AU - Ploeger, Bas

    AU - van de Pol, Jan Cornelis

    AU - Willemse, Tim A.C.

    N1 - 10.1007/978-3-540-74407-8_9

    PY - 2007/9

    Y1 - 2007/9

    N2 - In this paper, we provide a transformation from the branching bisimulation problem for infinite, concurrent, data-intensive systems in linear process format, into solving Parameterized Boolean Equation Systems. We prove correctness, and illustrate the approach with an unbounded queue example. We also provide some adaptations to obtain similar transformations for weak bisimulation and simulation equivalence.

    AB - In this paper, we provide a transformation from the branching bisimulation problem for infinite, concurrent, data-intensive systems in linear process format, into solving Parameterized Boolean Equation Systems. We prove correctness, and illustrate the approach with an unbounded queue example. We also provide some adaptations to obtain similar transformations for weak bisimulation and simulation equivalence.

    KW - FMT-MC: MODEL CHECKING

    KW - METIS-242021

    KW - IR-61980

    KW - EWI-11289

    U2 - 10.1007/978-3-540-74407-8_9

    DO - 10.1007/978-3-540-74407-8_9

    M3 - Conference contribution

    SN - 978-3-540-74406-1

    T3 - Lecture Notes in Computer Science

    SP - 120

    EP - 135

    BT - CONCUR 2007 - Concurrency Theory

    A2 - Caires, Luis

    A2 - Vasconcelos, Vasco T.

    PB - Springer

    CY - Berlin

    ER -

    Chen T, Ploeger B, van de Pol JC, Willemse TAC. Equivalence Checking for Infinite Systems Using Parameterized Boolean Equation Systems. In Caires L, Vasconcelos VT, editors, CONCUR 2007 - Concurrency Theory. Berlin: Springer. 2007. p. 120-135. 10.1007/978-3-540-74407-8_9. (Lecture Notes in Computer Science; LNCS4549). https://doi.org/10.1007/978-3-540-74407-8_9