Об'єкт дослідження – телекомунікаційні процеси як результат програмної або апаратної реалізації телекомунікаційних протоколів, які передбачають взаємодію необмеженої кількості пристроїв. Предмет дослідження – формальні методи верифікації телекомунікаційних протоколів на основі нескінченних сіток Петрі, методи аналізу, синтезу та перетворення відповідних моделей телекомунікаційних систем реєнтерабельними розфарбованими сітками Петрі. Мета дослідження – розробка моделей, методів та інструментальних засобів аналізу, синтезу та перетворення моделей телекомунікаційних систем для верифікації протоколів і оцінки ефективності мережевих технологій, які передбачають довільну кількість взаємодіючих систем. Методи дослідження: методи теорії мультимножин і перезапису мультимножин, методи лінійної алгебри, методи теорії частково впорядкованих множин (ґраток) і теорії чисел, методи теорії графів, методи теорії сіток Петрі, методи імітаційного моделювання і математичної статистики, методи алгебри (числення) процесів, елементи теорії реєнтерабельних, преємптивних і паралельних програм. Теоретичні та практичні результати: розв'язано завдання верифікації телекомунікаційних протоколів з довільною кількістю взаємодіючих пристроїв і комплексної верифікації сімейств телекомунікаційних протоколів для чого вперше введений клас нескінченних сіток Петрі і розроблено основи теорії нескінченних сіток Петрі; отримали подальший розвиток методи теорії графів, вперше введені граф передач і граф можливих блокувань пристроїв, за допомогою яких досліджено живість моделей телекомунікаційних систем та розроблена повна класифікація тупиків; для дослідження протоколів систем радіомовлення і стільникового зв'язку, комунікаційних систем суперкомп'ютерів і мереж на чипі побудовані узагальнені моделі трикутної, шестикутної та прямокутної ґраток на площині, гіперкуба і гіпертора в багатовимірних просторах; вперше введено клас реєнтерабельних моделей телекомунікаційних мереж, який містить кожен компонент в єдиному екземплярі і задає місце розташування пакета в мережі за допомогою дескриптора топологічної інформації; перевагами реєнтерабельних моделей є скорочення розміру моделі і часу її розробки у півтори рази та повторне застосування моделі; побудовано реєнтерабельні моделі IP, MPLS, PBB мереж, прямокутних ґраток, маршрутизації IP мереж за дистанційно-векторними протоколами та отримав подальший розвиток метод вимірювальних компонентів для оцінки продуктивності і якості обслуговування безпосередньо в процесі імітаційного моделювання; реєнтерабельні моделі застосовано для дослідження аспектів кібербезпеки функціонування обчислювальних ґраток та виявлена можливість блокування ґраток через створення тупиків; в результаті виконання роботи побудовано бібліотеки моделей та програмне забезпечення для автоматичного синтезу моделей.^UObject of research – telecommunication processes, as a result of software or hardware implementation of telecommunication protocols, which stipulate unlimited number of interacting devices. Subject of research – formal methods of telecommunication protocols verification by infinite Petri nets, methods of analysis, synthesis and transformation of correspondent models of telecommunication systems by reenterable colored Petri nets. Purpose of research – development of models, methods, and tools of analysis, synthesis, and transformation of telecommunication systems models for verification of protocols and efficiency evaluation of networking technologies, which stipulate an arbitrary number of interacting systems. Research methods: methods of multisets theory and multisets rewriting systems, linear algebraic methods, theory of partially ordered sets (lattices) and number theory methods, methods of graph theory, methods of Petri net theory, simulation and mathematical statistics methods, methods of process algebra (calculus), elements of theories of reenterable, preemptive and parallel programs. Theoretical and practical results: a task of verification of telecommunication protocols with arbitrary number of communicating devices and complex verification of families of telecommunication protocols has been solved that required to introduce for the first time a class of infinite Petri nets and to develop the basics of infinite Petri nets theory; methods of graph theory have been further developed, a transmissions graph and a graph of possible blockings of devices have been introduced for the first time and applied to study the liveness of telecommunication systems models, a complete classification of deadlocks obtained; to study radio and cellular communication protocols, communication systems of supercomputers and networks-on-chip, generalized models of triangular, hexagonal, and rectangular lattices on plane, hypercube and hypertorus in multidimensional spaces have been built; for the first time, a class of reenterable models of telecommunication networks is introduced, which contains each component in a single instance and specifies the packet location within a network using a topological information descriptor; advantages of reenterable models are reduction of the model size and time of its development in one and a half times and re-use of models; reenterable models of IP, MPLS, and PBB networks, rectangular grids, IP networks routing based on distance-vector protocols have been developed, and the measuring components method has been further developed for the performance and quality of service evaluation directly in the process of simulation; reenterable models have been applied to investigate the cybersecurity aspects of the computing grids operation and a possibility of blocking grids via inducing deadlocks has been revealed; as a practical result of the dissertation, a library of models and software have been developed to automatically synthesize models.