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

    29 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