# Technical Report CS-2000-04

 TR#: CS-2000-04 Class: CS Title: Simulation Based Minimization Authors: Doron Bustan and Orna Grumberg PDF CS-2000-04.pdf Abstract: This work presents a minimization algorithm. The algorithm receives a Kripke structure $M$ and returns the smallest structure that is simulation equivalent to $M$. The {\em simulation equivalence} relation is weaker than bisimulation but stronger than the simulation preorder. It strongly preserves ACTL and LTL (as sub-logics of ACTL$^*$). We show that every structure $M$ has a unique up to isomorphism {\em reduced} structure that is simulation equivalent to $M$ and smallest in size. We give a Minimizing Algorithm that constructs the reduced structure. It first constructs the quotient structure for $M$, then eliminates transitions to little brothers and finally deletes unreachable states. The first step has maximal space requirements since it is based on the simulation preorder over $M$. To reduce these requirements we suggest the \partAlg which constructs the quotient structure for $M$ without ever building the simulation preorder. The \partAlg has a better space complexity but might have worse time complexity. 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-04), rather than to the URL of the PDF files directly. The latter URLs may change without notice.