Computing refactorings of state machines

For behavior models expressed in statechart-like formalisms, we show how to compute semantically equivalent yet structurally different models. These refactorings are defined by user-provided logical predicates that partition the system's state space and that characterize coherent parts - modes or control states-of the behavior. We embed the refactorings into an incremental development process that uses a combination of both tables and graphically represented state machines for describing system