An overview of works, early published by the authors, has been done that explains peculiarities of composition and analysis technique developed for investigation of infinite Petri nets with regular structure which were introduced for modeling networks, clusters, and computing grids. Parametric description of Petri nets, parametric representation of infinite systems for calculation place/transition invariants, and solving them in parametric form allowed the invariance proof for infinite Petri net models. Complex deadlocks were disclosed and a possibility of the network blocking via ill-intended traffic revealed. Prospective directions for future research of infinite Petri nets were formulated.
TopBackground
Components, used for composition of infinite structures, are functional subnets (clans) of Petri nets (Zaitsev, 2006; Zaitsev, 2005) which are well studied when investigating usual (finite) models, for instance, in the process of protocol TCP verification. Input places of a clan have only outgoing arcs and output places – only incoming arcs. Composition of protocol TCP model from its clans is represented in Figure 1.
Figure 1. Composition of protocol TCP model
Compositional analysis allowed speed-up of the verification processes of complex networking protocols because of solving a sequence of linear systems with lesser dimension which is essential when finding solutions in nonnegative domain (monoid) for Diophantine systems (ring).
TopIssues, Controversies, Problems
The first problem which researchers encountered, when verifying networking protocols via Petri nets, was the problem of exponential computation complexity of the majority known analysis methods.
To solve this problem, the compositional analysis of Petri nets (Zaitsev, 2006; Zaitsev, 2005) was offered based on the decomposition of a net into the set of its functional subnets (clans), solving tasks for each clan and then fulfilling, either simultaneously or sequentially, composition of functional subnets. Solving a few systems with considerably lesser dimension, under the condition of exponential complexity, allowed an exponential speed-up of computations and verification of known protocols, such as ECMA, BGP, TCP, and IOTP, in reasonable time.
The second problem arose when investigating protocols of the network Ethernet with common bus architecture. It was rather simple to construct a model of a single device. The majority of protocols stipulates interaction of two systems, for example, as protocol TCP. Electronic commerce protocol IOTP considers a few interacting systems but their number is constant: Customer, Merchant, Payment Handler, Delivery Handler, Merchant Customer Care Provider. A segment of Ethernet with common bus architecture could contain a priory unknown number of computers which is reasonable to not limit in research in spite of definite physical limitations stated in standards.
To solve this problem, infinite Petri nets with regular structure were introduced for the first time as a linear composition of the workstation models. The further progress of research was indicated by the number of dimensions and the structure of devices’ connections: tree-like structures for analysis of switched Ethernet (Shmeleva, 2007), triangular, rectangular, and hexangular grids for analysis of distributed computations, radio and television broadcasting, cellular communications (Zaitsev, 2013; Shmeleva, Zaitsev & Zaitsev, 2009) as well as various edge conditions. In the most general form, results were obtained for a hypercube with an arbitrary size and an arbitrary number of dimensions (Zaitsev & Shmeleva, 2010; Zaitsev & Shmeleva, 2008).