Rebeca is an actor-based language with formal semantics that can be used at a high level of abstraction in modeling concurrent and distributed reactive systems. The asynchronous message-passing paradigm in Rebeca allows for efficient modeling of loosely-coupled distributed systems. The simple Java-like syntax of Rebeca, unlike the traditional notations of formal languages, is an easy-to-learn notation for software practitioners.

In this talk we study the application of partial order and symmetry reduction techniques to model checking dynamic Rebeca models. Finding symmetry-based equivalence classes of states is in general a difficult problem known to be as hard as graph isomorphism. We show how actor-based nature of Rebeca leads to a polynomial-time solution to this problem. On the other hand, the coarse-grained interleaving approach in Rebeca causes considerable reductions when partial order reduction is applied.