Simulation Reduction as Constraint

The simulation relation is largely used in Model Checking where it allows to reduce Kripke structures, on which verification takes place, while preserving significant fragments of Temporal Logic. Our approach to the problem of simulation computation here has two aims: on the one hand we want to provide a framework in which developing algorithms competitive with the best ones in the literature, on the other hand we want to show how it is extremely natural to view such algorithms as constraint solving procedures to be easily implemented in a constraint logic programming scheme