Date and Time:Thursday, 14 February 2008, 15:30-ca. 16:30

Speaker:Bas Ploeger (OAS / TUe)

Title: Correcting a Space-Efficient Simulation Algorithm.

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. One is by Bustan and Grumberg and the other by Gentilini, Piazza and Policriti. Of these, the latter one has the best time complexity. It exploits the representation of the simulation problem as a generalized coarsest partition problem: it is based on a fixed-point operator for obtaining a generalized coarsest partition as the limit of a sequence of partition pairs.
In this talk, I show that this fixed-point theory is flawed, and that the algorithm is incorrect. I propose a solution to correct the algorithm without affecting its space and time complexities. Finally, I show that there is no fixed-point operator that corresponds to this repaired algorithm.