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 language | English |
|---|---|
| Title of host publication | Computer Aided Verification: 20th International Conference, CAV 2008 Princeton, NJ, USA, July 7-14, 2008, Proceedings |
| Editors | Aarti Gupta, Sharad Malik |
| Place of Publication | Berlin, Heidelberg |
| Publisher | Springer |
| Pages | 517-529 |
| Number of pages | 13 |
| ISBN (Electronic) | 978-3-540-70545-1 |
| ISBN (Print) | 978-3-540-70543-7 |
| DOIs | |
| Publication status | Published - 14 Jul 2008 |
| Event | The 20th International Conference on Computer Aided Verification, 2008 - Princeton, United States Duration: 7 Jul 2008 → 14 Jul 2008 Conference number: 20 https://www.princeton.edu/cav2008/ |
Publication series
| Name | Lecture Notes in Computer Science |
|---|---|
| Publisher | Springer Berlin, Heidelberg |
| Volume | 5123 |
| ISSN (Print) | 0302-9743 |
| ISSN (Electronic) | 1611-3349 |
Conference
| Conference | The 20th International Conference on Computer Aided Verification, 2008 |
|---|---|
| Abbreviated title | CAV 2008 |
| Country/Territory | United States |
| City | Princeton |
| Period | 7/07/08 → 14/07/08 |
| Internet address |