Symmetry and Partial Order Reduction Techniques in Model Checking 'Rebeca'

摘要

Rebeca is an actor-based language with formal semantics that can be used in modeling concurrent and distributed software and protocols. In this paper, 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, for 'Rebeca' models, we can tackle this problem with a polynomial-time solution. Moreover, the coarse-grained interleaving semantics of Rebeca causes considerable reductions when partial order reduction is applied. We have also developed a tool that can make use of both techniques in combination or separately. The evaluation results show significant improvements in model size and model-checking time.