Quotient graphs for the analysis of asymmetric distributed systems: surveying two alternative approaches

摘要

State-space based techniques represent a powerful analysis tool of discrete-event systems. One way to face the state-space explosion is the exploitation of behavioral symmetries of distributed systems. Well-Formed Coloured Petri Nets (WN) allow the direct construction of a symbolic reachability graph (SRG) that captures symmetries suitably encoded in WN syntax. Most real systems however mix symmetric and asymmetric behaviors. The SRG, and more generally, all those approaches based on a static description of symmetries, have shown not to be effective in such cases. In this paper two quotient graphs are proposed as effective analysis frameworks for asymmetric systems. Both rely on WN syntax extended with relational operators. The first one is an extension of the SRG that exploits local symmetries. The second technique uses linear constraints and substate inclusion in order to aggregate states. An asymmetric distributed leader-election algorithm is used as running example.