Distributed Branching Bisimulation Minimization by Inductive Signatures

Stefan Blom

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

    55 Downloads (Pure)

    Abstract

    We present a new distributed algorithm for state space minimization modulo branching bisimulation. Like its predecessor it uses signatures for refinement, but the refinement process and the signatures have been optimized to exploit the fact that the input graph contains no tau-loops. The optimization in the refinement process is meant to reduce both the number of iterations needed and the memory requirements. In the former case we cannot prove that there is an improvement, but our experiments show that in many cases the number of iterations is smaller. In the latter case, we can prove that the worst case memory use of the new algorithm is linear in the size of the state space, whereas the old algorithm has a quadratic upper bound. The paper includes a proof of correctness of the new algorithm and the results of a number of experiments that compare the performance of the old and the new algorithms.
    Original languageUndefined
    Title of host publicationProceedings 8th International Workshop on Parallel and Distributed Methods in verifiCation
    EditorsL. Brim, Jan Cornelis van de Pol
    Place of PublicationAustralia
    PublisherOpen Publishing Association
    Pages32-46
    Number of pages15
    ISBN (Print)2075-2180
    DOIs
    Publication statusPublished - 13 Dec 2009
    Event8th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2009 - Eindhoven, Netherlands
    Duration: 4 Nov 20094 Nov 2009
    Conference number: 8
    http://anna.fi.muni.cz/PDMC/PDMC09/

    Publication series

    NameElectronic Proceedings in Theoretical Computer Science
    PublisherOpen Publishing Association
    Volume14
    ISSN (Print)2075-2180

    Workshop

    Workshop8th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2009
    Abbreviated titlePDMC
    CountryNetherlands
    CityEindhoven
    Period4/11/094/11/09
    Internet address

    Keywords

    • METIS-264283
    • IR-69463
    • Branching bisimulation
    • Distributed reduction algorithm
    • CR-C.2.4
    • EC Grant Agreement nr.: FP6/043235
    • minimization
    • FMT-MC: MODEL CHECKING
    • EWI-17088

    Cite this