Equivalence Checking for Infinite Systems Using Parameterized Boolean Equation Systems

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

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

    31 Citations (Scopus)
    1 Downloads (Pure)

    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 languageEnglish
    Title of host publicationCONCUR 2007 - Concurrency Theory
    EditorsLuis Caires, Vasco T. Vasconcelos
    Place of PublicationBerlin
    PublisherSpringer
    Pages120-135
    Number of pages16
    ISBN (Electronic)978-3-540-74407-8
    ISBN (Print)978-3-540-74406-1
    DOIs
    Publication statusPublished - Sept 2007
    Event18th International Conference on Concurrency Theory, CONCUR 2007 - Lisbon, Portugal
    Duration: 3 Sept 20078 Sept 2007
    Conference number: 18

    Publication series

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

    Conference

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

    Keywords

    • FMT-MC: MODEL CHECKING

    Fingerprint

    Dive into the research topics of 'Equivalence Checking for Infinite Systems Using Parameterized Boolean Equation Systems'. Together they form a unique fingerprint.

    Cite this