Применение компонентных сетей Петри в задачах верификации параллельных распределённых систем

• Опубліковано в: : Проблеми програмування
• Дата: 2014
• Автор: Лукьянова, Е.А.
• Формат: Стаття
• Мова: Russian
• Опубліковано: Інститут програмних систем НАН України 2014
• Теми: Паралельне програмування. Розподілені системи і мережі
• Онлайн доступ: https://nasplib.isofts.kiev.ua/handle/123456789/113219
• Назва журналу: Digital Library of Periodicals of National Academy of Sciences of Ukraine
• Цитувати: Применение компонентных сетей Петри в задачах верификации параллельных распределённых систем / Е.А. Лукьянова // Проблеми програмування. — 2014. — № 2-3. — С. 93-98. — Бібліогр.: 19 назв. — рос.

В работе рассмотрены модели Крипке двух математических моделей параллельных распределённых систем, представленных детальной и её компонентной сетями Петри. Показана бисимулярность этих моделей Крипке. Установлены возможности проверки истинности логической формулы темпоральной логики, которой задаётся требуемое свойство исследуемой параллельной распределённой системы, с помощью редуцированной модели Крипке компонентной сети Петри. The paper discusses the Kripke structures of two mathematical models of parallel distributed systems that are presented by Petri detailed net and its component net. Bisimularity of these Kripke structures is displayed. The possibility for checking the validity of the logical formula of temporal logic is established, which gives the desired property of investigated parallel distributed system, using reduced Kripke structure of component Petri net.