Simulation-based minimization

Abstract

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.