In: The IEEE Computer Society's 12th Annual International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunications Systems (MASCOTS'04), October 04 - 08, 2004, Volendam, The Netherlands, pages 560-568. IEEE Press, October 2004.
Abstract: Most analysis techniques for discrete-event systems rely on building the system state-transition graphs. A known critical issue is represented by the state-space explosion. One way to face this problem is the exploitation of behavioral symmetries. Well-Formed Coloured Petri Nets (WN) allow (thanks to their particular syntax) the automatical building of a quotient graph, called Symbolic Reachability Graph -SRG, able to exploit the structural symmetries of systems. The SRG reduction power vanishes when the modeled system evolves in asymmetric way. Some proposals presented in literature to enhance the SRG have actually shown to be effective only when applied to nearly symmetric systems. In this paper a quotient graph still relying on the WN formalism is semi-formally introduced, that tries to exploit local symmetries, rather diffuse in real systems. The model of an asymmetric distributed algorithm is used throughout the paper as running example, and preliminary benchmark for the technique being presented.
Keywords: Colored Petri Nets; quotient state-spaces; asymmetric systems.