Two Kinds of Infinite Petri Nets for Modeling Computing and Communication Systems

Correctness of networking protocols represents the principal requirement of cybersecurity. Correctness of protocols is established via the procedures of their verification. A classical communication system includes a pair of interacting systems. Recent developments of computing and communication grids for radio broadcasting, cellular networks, communication subsystems of supercomputers, specialized grids for numerical methods, and networks on chips require verification of protocols for any number of devices. For analysis of computing and communication grid structures, a new class of infinite Petri nets has been introduced and studied for more than 10 years. Infinite Petri nets were applied also for simulating cellular automata. Rectangular, triangular, and hexagonal grids on plane, hyper cube and hyper torus in multidimensional space have been considered. Composing and solving in parametric form infinite Diophantine systems of linear equations allowed us to prove the protocol properties for any grid size and any number of dimensions. In the present paper, infinite Petri nets are divided into two following kinds: a single infinite construct and an infinite set of constructs of specified size (and number of dimensions). Finally the paper discusses possible future work directions.