Сборники трудов ИСП РАН


Трансляция вложенных сетей Петри в классические сети Петри для верификации разверток

В.О. Ермакова (ВШЭ, Москва, Россия)
И.А. Ломазова (ВШЭ, Москва, Россия)

Аннотация

Вложенные сети Петри являются одним из удобных формализмов для моделирования и анализа поведения распределенных мультиагентных систем. Они естественным образом представляют структуру мультиагентных систем, так как фишки в системной сети сами являются классическими сетями Петри и могут иметь автономное поведение. Мультиагентные системы являются системами с высоким уровнем параллелизма. При верификации таких систем методами проверки модели (model checking) возникают серьезные трудности, связанные с взрывным ростом числа промежуточных состояний системы (state-space explosion problem). Для решения этой проблемы в литературе был предложен подход, основанный на построении развертки поведения системы. Ранее была изучена применимость разверток для верификации вложенных сетей Петри и предложен метод построения разверток для безопасных консервативных вложенных сетей Петри. В этой работе предлагается другой метод построения разверток для безопасных консервативных вложенных сетей Петри, основанный на трансляции таких сетей в классические сети Петри. Для классических сетей Петри затем применяются стандартные методы построения разверток. Также в работе обсуждаются сравнительные достоинства двух подходов.

Ключевые слова

мультиагентные системы; верификация; сети Петри; вложенные сети Петри; развертки

Издание

Труды Института системного программирования РАН, том 28, вып. 4, 2016, стр. 115-136.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2016-28(4)-7

Полный текст статьи в формате pdf Вернуться к содержанию тома