In: Proceedings of the Design, Analysis, and Simulation of Distributed Systems Symposium, April 2-8, 2005, San Diego, USA, pages 72-78. April 2005.
Abstract: Petri net model of the widely known protocol BGP of Internet backbone routing was constructed. The decomposition of Petri net model of communication protocol BGP into functional subnets was implemented. Invariance of the source model was proved on the base of established invariance of its functional subnets. The speed-up of computations obtained is exponential with respect to dimension of Petri net.
Keywords: Petri net; BGP; Invariance; Decomposition; Functional subnet.