M.M. Jaghoori, M. Sirjani, M.R. Mousavi, A. Movaghar, To appear in the Proceedings of the 2nd International Conference on Distributed Computing and Internet Technology (ICDCIT'05), Bhubaneswar, India, volume 3816 Lecture Notes in Computer Science, pp. 494--507, Springer-Verlag, December 2005.
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 {\em orbits}, of states under symmetry is in its general form NP-hard. 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 object-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.
(Paper in .ps format in .pdf format)
@InProceedings{MousaviICDCIT05,
author = "Jaghoori, MohammadMahdi and Sirjani, Marjan and Mousavi, MohammadReza and Movaghar, Ali",
title = "Efficient Symmetry Reduction in an Actor-Based Model",
booktitle = "Proceedings of the 2nd International Conference on Distributed Computing and Internet Technology (ICDCIT'05)",
editor = "Chakraborty, Goutam",
volume = "3816",
pages = "494-–507",
series = "Lecture Notes in Computer Science",
address = "Bhubaneswar, India",
publisher = "Springer-Verlag, Berlin, Germany",
year = "2005"
}