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.
|Title of host publication||Distributed Computing and Internet Technology|
|Subtitle of host publication||Second International Conference, ICDCIT 2005, Bhubaneswar, India, December 22-24, 2005. Proceedings|
|Place of Publication||Berlin|
|Number of pages||14|
|ISBN (Print)||3-540-30999-3, 978-3-540-30999-4|
|Publication status||Published - 2005|
|Name||Lecture Notes in Computer Science (LNCS)|