Верификация вложенных сетей Петри с помощью разверток сетей.

<p>Отчет 45 с., 20 рис., 35 источников. Ключевые слова: верификация, сети Петри, вложенные сети Петри, параллелизм, проверка моделей, развертки, мультиагентные системы. Темой данного исследования является исследования метода разверток в применении к<br />верификации вложенных сетей Петри.<br />Формализм вложенных сетей Петри используется для моделирования мультиагентных<br />систем &ndash; систем, состоящих из набора автономных агентов, имеющих свое собственное по- ведение, взаимодействующие через механизмы синхронизации. Засчет наличия автономного поведения, мультиагентные системы имеют являются сильно распараллеленными.<br />При верификации параллельных и распределенных система часто возникает проблема экспоненциального роста пространства достижимых состояний системы. Одной из при- чин этого является наличие большого числа промежуточных состояний, получаемых в результате рассмотрения всех возможных последовательных исполнений системы &ndash; интер- ливинга (interleaving). Один из способов решения этой проблемы использует построение (конечных префиксов) разверток сетей.<br />Развертки сетей (net unfoldings) используются для описания поведения системы в се- мантике истинного параллелизма. В случае высокопаралленьных систем развертки (а точ- нее их конечные префиксы) имеют размер меньший чем графы достижимости, тем самым позволяя частично обойти проблему взрывоподобного роста числа достижимых состояний.<br />Основным результатом данной работы является определение разверток и ветвящихся процессов для консервативных вложенных сетей Петри, моделирующих системы с неиз- менных множеством агентов. Это определение используется для построения основанного на развертках алгоритма верификации важных поведенческих свойств для консерватив- ных вложенных сетей Петри.<br />Результаты данных исследований представлены в докладе, принятом на семинар Ve</p><p>rification and Program Transformation, в рамках международной конференции Computer Aided Verification 2014, которая будет проходить в Вене в июле этого года.</p>