Simulation-based minimization

We present a minimization algorithm that receives a Kripke structure M and returns the smallest structure that is simulation equivalent to M. The simulation equivalence relation is weaker than bisimulation but stronger than the simulation preorder. It strongly preserves ACTL and LTL (as sublogics of ACTL*). We show that every structure M has a unique-up-to-isomorphism reduced structure that is simulation equivalent to M and smallest in size. Our Minimizing Algorithm constructs this reduced structure. It first constructs the quotient structure for M, then eliminates transitions to little brothers, and finally deletes unreachable states. Since the first step of the algorithm is based on the simulation preorder over M, it has maximal space requirements. To reduce them, we present the Partitioning Algorithm, which constructs the quotient structure for M without ever building the simulation preorder. The Partitioning Algorithm has improved space complexity, but its time complexity might have worse.