Correcting a Space-Efficient Simulation Algorithm

Rob van Glabbeek, Bas Ploeger

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

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
EditorsAarti Gupta, Sharad Malik
Place of PublicationBerlin, Heidelberg
PublisherSpringer Berlin Heidelberg
Pages517-529
Number of pages13
ISBN (Electronic)978-3-540-70545-1
ISBN (Print)978-3-540-70543-7
DOIs
Publication statusPublished - 14 Jul 2008
EventThe 20th International Conference on Computer Aided Verification, 2008 - Princeton, United States
Duration: 7 Jul 200814 Jul 2008
Conference number: 20
https://www.princeton.edu/cav2008/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin, Heidelberg
Volume5123
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceThe 20th International Conference on Computer Aided Verification, 2008
Abbreviated titleCAV 2008
Country/TerritoryUnited States
CityPrinceton
Period7/07/0814/07/08
Internet address

Fingerprint

Dive into the research topics of 'Correcting a Space-Efficient Simulation Algorithm'. Together they form a unique fingerprint.

Cite this