Развертывание сети Петри

Анализ сетей Петри может быть выполнен посредством построения либо достижимых пространств состояний (или достижимых разметок), либо посредством процесса развертки на основе графов. Префикс развертки сети Петри, который представляет собой ациклический граф сети Петри, содержит ту же информацию о свойствах сети Петри, что и граф достижимости, плюс он содержит информацию о последовательности, параллелизме и конфликтных отношениях между переходами сети Петри и сетью Петри. места. Преимущества использования развертки на практике обычно связаны с тем, что префикс развертки гораздо компактнее графа достижимости анализируемой сети Петри.

Развертки сети Петри были первоначально предложены Кеном Макмилланом . ^{[ 1 ]} В дальнейшем их изучали несколько авторов, которые усовершенствовали исходный критерий получения префикса развертки с точки зрения его компактности и, следовательно, эффективности анализа. ^{[ 2 ]}^{[ 3 ]}

Существуют применения разверток сетей Петри в анализе и синтезе параллельных систем и асинхронных схем . ^{[ 4 ]}^{[ 5 ]} Последнее обычно достигается за счет использования графов перехода сигналов (STG).

Ссылки

^ Макмиллан, КЛ (1993). «Использование разверток, чтобы избежать проблемы взрыва состояний при проверке асинхронных схем». Фон Бохманн, Грегор; Пробст, Дэвид Карл (ред.). Компьютерная проверка . Конспекты лекций по информатике. Том. 663. Берлин, Гейдельберг: Springer. стр. 164–177. дои : 10.1007/3-540-56496-9_14 . ISBN 978-3-540-47572-9 . S2CID 44597274 .
^ Эспарса, Хавьер; Ремер, Стефан; Фоглер, Уолтер (1 мая 2002 г.). «Улучшение алгоритма разворачивания Макмиллана» . Формальные методы проектирования систем . 20 (3): 285–310. дои : 10.1023/А:1014746130920 . ISSN 1572-8102 . S2CID 15149333 .
^ Хелианко, Кейджо (1999). «Минимизация конечных полных префиксов» (PDF) .
^ Семенов, Алексей (1997). «Верификация и синтез асинхронных схем управления с использованием разверток сетей Петри, докторская диссертация, Университет Ньюкасла» .
^ Хоменко, Виктор (2003). «Проверка моделей на основе префиксов разверток сети Петри, докторская диссертация, Университет Ньюкасла» (PDF) .

Дальнейшее чтение

Веб-сайт мира сетей Петри, https://www2.informatik.uni-hamburg.de/TGI/PetriNets/index.php
Веб-сайт асинхронного проектирования Университета Ньюкасла http://async.org.uk

П ≟ НП

Эта теоретической информатикой, статья, связанная с незавершена . Вы можете помочь Википедии, расширив ее .

[1] Макмиллан, КЛ (1993). «Использование разверток, чтобы избежать проблемы взрыва состояний при проверке асинхронных схем». Фон Бохманн, Грегор; Пробст, Дэвид Карл (ред.). Компьютерная проверка . Конспекты лекций по информатике. Том. 663. Берлин, Гейдельберг: Springer. стр. 164–177. дои : 10.1007/3-540-56496-9_14 . ISBN 978-3-540-47572-9 . S2CID 44597274 .

[2] Эспарса, Хавьер; Ремер, Стефан; Фоглер, Уолтер (1 мая 2002 г.). «Улучшение алгоритма разворачивания Макмиллана» . Формальные методы проектирования систем . 20 (3): 285–310. дои : 10.1023/А:1014746130920 . ISSN 1572-8102 . S2CID 15149333 .

[3] Хелианко, Кейджо (1999). «Минимизация конечных полных префиксов» (PDF) .

[4] Семенов, Алексей (1997). «Верификация и синтез асинхронных схем управления с использованием разверток сетей Петри, докторская диссертация, Университет Ньюкасла» .

[5] Хоменко, Виктор (2003). «Проверка моделей на основе префиксов разверток сети Петри, докторская диссертация, Университет Ньюкасла» (PDF) .

[ 1 ]

[ 2 ]

[ 3 ]

[ 4 ]

[ 5 ]