Correcting a space-efficient simulation algorithm

R.J. Glabbeek, van, S.C.W. Ploeger

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

    29 Citations (Scopus)

    Abstract

    Although there are many efficient algorithms for calculating the simulation preorder on finite Kripke structures, only two have been proposed of which the space complexity is of the same order as the size of the output of the algorithm. Of these, the one with the best time complexity exploits the representation of the simulation problem as a generalised coarsest partition problem. It is based on a fixed-point operator for obtaining a generalised coarsest partition as the limit of a sequence of partition pairs. We show that this fixed-point theory is flawed, and that the algorithm is incorrect. Although we do not see how the fixed-point operator can be repaired, we correct the algorithm without affecting its space and time complexity.
    Original languageEnglish
    Title of host publicationComputer Aided Verification (20th International Conference, CAV 2008, Princeton NJ, USA, July 7-14, 2008, Proceedings)
    EditorsA. Gupta, S. Malik
    Place of PublicationBerlin
    PublisherSpringer
    Pages517-529
    ISBN (Print)978-3-540-70543-7
    DOIs
    Publication statusPublished - 2008

    Publication series

    NameLecture Notes in Computer Science
    Volume5123
    ISSN (Print)0302-9743

    Fingerprint

    Dive into the research topics of 'Correcting a space-efficient simulation algorithm'. Together they form a unique fingerprint.

    Cite this