A quotient graph for asymmetric distributed systems

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) (thanks to their particular syntax) allow the automatic building of a quotient graph, called a symbolic reachability graph (SRG), able to exploit the structural symmetries of systems. The SRG reduction power vanishes when the modeled system evolves in an asymmetric way. Some proposals to enhance the SRG have been shown to be effective only when applied to nearly symmetric systems. A quotient graph, still relying on the WN formalism, is semi-formally introduced; it tries to exploit local symmetries, rather diffuse in real systems. The model of an asymmetric distributed algorithm is used as a running example, a preliminary benchmark for the technique being presented.