| TR#: | CS-2000-04 |
| Class: | CS |
| Title: | Simulation Based Minimization |
| Authors: | Doron Bustan and Orna Grumberg |
| 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.
To the list of the CS technical reports of 2000
To the main CS technical reports page