In: Proceedings of Odessa National Telecommunication Academy, no. 2, 2004, pages 19-27. 2004. In Russian.
Abstract: Proof of the invariance of Petri net model for connection and disconnection phases of TCP protocol was implemented. Decomposition of Petri net model into functional subnets was realized. Calculation of invariants was implemented in the process of sequential composition, which allows the essential acceleration of computations.
Keywords: TCP; Petri net; invariant; functional subnet.