A method, computer program and system, which, given a set of Boolean state variables, a set of state transitions described as truth tables for the state variables, a set of initial states (that is states that objects happen to be in when they are brand new or when they are introduced into the system), all established by a natural modeling of the application domain, can derive an encoding that is provably isomorphic to the initial one but smaller, and transitions that match exactly the initial transitions but operating upon the new encoding, without incurring a significant time penalty. This effect is obtained by generating the extensive set of significant states, renumbering those states, then modifying the transitions implementation so as to use the renumbered states in place of the original ones.