Efficient Symmetry Reduction in 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.
- Efficient Symmetry Reduction in an Actor-Based Model
M.M. Jaghoori, M. Sirjani, M.R. Mousavi, A. Movaghar.
In: Proceedings of the 2nd International Conference on Distributed Computing and Internet Technology
(ICDCIT'05), Bhubaneswar, India, volume 3816 of Lecture Notes in Computer Science, pp. 494-?507,
Springer-Verlag, December 2005. (abstract, pdf).
|
