Partition refinement for emulation

Kripke models are useful to express static knowledge or belief. On the other hand, action models describe information flow and dynamic knowledge or belief. The technique of refinement partition has been used to find the smallest Kripke model under bisimulation, which is sufficient and necessary for the semantic equivalence of Kripke models. In this paper, we generalize refinement partition to action models to find the smallest action model under propositional action emulation, which is sufficient for the semantic equivalence of action models, and sufficient and necessary if the action models are required to be propositional.