“School of Computer Science”
Back to Papers HomeBack to Papers of School of Computer Science
| Paper IPM / Computer Science / 10871 |
|
||||||||
| Abstract: | |||||||||
|
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.
Download TeX format |
|||||||||
| back to top | |||||||||
