# Technical Report CS-2000-13

 TR#: CS-2000-13 Class: CS Title: Checking for Fair Simulation in Models with Buchi Fairness Constraints Authors: Doron Bustan and Orna Grumberg PDF CS-2000-13.pdf Abstract: Many approaches to overcoming the problem of high space requirements in model checking are based on the {\em simulation preorder}. This preorder relates the system model to some reduced model, provided that the reduced model contains all the behaviors of the system model. Reduction techniques often add unrealistic behaviors to the reduced model. Fairness constraints can then be added to exclude these behaviors from consideration during verification. The simulation preorder, in its original form, does not handle fairness constraints. {\em Fair simulation preorders} that extend the simulation preorder by referring only to the fair behaviors of the models are therefore desirable. A definition of fair simulation was introduced in \cite{FairSim}. The definition is accompanied by an algorithm for checking fair simulation in models with fairness constraints. In this work we suggest an improved algorithm for computing the fair simulation preorder. Our algorithm is significantly simpler than the one in \cite{FairSim} and therefore can be easily implemented. It has the same time complexity as the previous algorithm, and a better space complexity. Furthermore, it provides a counterexample in case the reduced model does not contain all the fair behaviors of the system model. Our algorithm is based on a game characterization of the fair simulation preorder. It works in time complexity of $O(n^3)$ and space complexity of $O(n)$, where $n$ is the product of the model sizes. Copyright The above paper is copyright by the Technion, Author(s), or others. Please contact the author(s) for more information

Remark: Any link to this technical report should be to this page (http://www.cs.technion.ac.il/users/wwwb/cgi-bin/tr-info.cgi/2000/CS/CS-2000-13), rather than to the URL of the PDF files directly. The latter URLs may change without notice.