# Applying Infinite Petri Nets to the Cybersecurity of Intelligent Networks, Grids and Clouds
## 3 Getting Familiar with Petri Nets  
A Petri net [21; 27] represents a bipartite directed graph with a dynamic process defined on it. One part of vertices, depicted as circles and called places, models conditions, the other part of vertices, depicted as rectangles (bars) and called transitions, models events. Dynamic elements, called tokens, are situated inside places and are consumed and produced by transitions as a result of firing in accordance with arcs' weights; at a step, one transition fires. Introduced in 1962 in dissertation of [PERSON], the nets found wide application in wide range of domains including manufacture control, transportation, and business processes management. A Petri net is considered a convenient and powerful tool for verification of networking protocols [28] and correctness proof for parallel and distributed processes [27], including routing protocols [29] and mobile computing systems [30]. In Figure 1, a Petri net model of Transmission Control Protocol (TCP) [23; 31]--one of the most widespread Internet protocols--is shown. It covers procedures of connection three-way-handshake and disconnection. The left and right parts model the first and the second systems while the central part represents control bites of the standard messages. The Petri net completely corresponds to the TCP Connection State Diagram and TCP Header Format; for the second system states and actions, prefix \"x\" is used. As an example, let us consider the tree-way-handshake procedure implementation on request of the first (left) system. _AOpen_ transition fires modelling Active Opening of connection by the first system moving a token from place _CLOSED_ into place _SYNSENT_ and putting a token into place _SYN_ that models the corresponding flag of TCP message sent from the first (left) to the second (right) system. The second system moves a token from place _xCLOSED_ to _xLISTEN_ by transition _xPOPEN_ modelling Passive Opening of connection. Then it receives the message firing transition _xrs_ that moves a token from place _xLISTEN_ to place _xSYNRCVD_ and putting a token into place _xSYNACK_ that models thecorresponding flag of TCP message sent from the second to the first system. Then the first system, triggered by xSYNRCVD flag of received message, moves a token from place _SYNSENT_ to place _ESTAB_ by transition rsa, and sends a message with flag _SYNACK_. From the first system point of view, a connection is established that is indicated by a token in place _ESTAB_. The second system receives the message containing _SYNACK_ flag by transition _xras_ moving a token from place _xSYNRCVD_ to place _xESTAB_. Now the connection is established from the point of view of both systems. A classical Petri net is more powerful than a finite automaton (state machine) and less powerful than a Turing machine [21]. Thus, to study a Petri net, we can apply not only simulation but formal analysis techniques as well [23; 27]. Potentially infinite state space, represented with finite coverability tree, and methods of linear algebra allow us to evaluate basic properties of a Petri net such as boundedness and liveness or solve a problem of a state (marking) reachability. Among manifold tools for Petri net analysis we mention INA, Tina [32], and Snoopy. Traditionally, finite Petri nets having finite sets of places and transitions have been studied. As a first hint to the necessity of introducing infinite Petri nets, we consider [PERSON] [33] study of bus Ethernet. We can attach one, two, three, or more workstations to the bus proving properties of the protocol for each given size separately. More recently the verification of such network protocols has been extended to any number of attached workstations [23]. Then, when studying a switched Ethernet, we come to a tree-like structure and are craving for a technique to prove basic properties for any tree. The problem becomes general when considering computing and communication grids [25; 26] where we come to triangular, rectangular, or hexagonal grids.