Efficient symmetry reduction for an actor-based model

Symmetry reduction is a promising technique for combatting state space explosion in model checking. The problem of finding the equivalence classes, i.e., the so-called orbits, of states under symmetry is a difficult problem known to be as hard as graph isomorphism. In this paper, we show how we can automatically find the orbits in an actor-based model, called Rebeca, without enforcing any restriction on the modeler. The proposed algorithm solves the orbit problem for Rebeca models in polynomial time. As a result, the simple actor-based Rebeca language can be utilized efficiently for modeling and verification of systems, without involving the modeler with the details of the verification technique implemented.