?
Relaxed Lazy Soundness Verification for Data Petri nets
Для представления модели, включающей как данные, так и ресурсы, можно использовать сети Петри с данными. Каждому переходу в таких сетях сопоставлено ограничение, включающее условия на входные и выходные значения переменных. Условия на входные значения определяют правила, при которых переход может сработать. Условия на выходные значения определяют правила, согласно которым осуществляется изменение значений переменных при срабатывании перехода. Чтобы оставаться в границах разрешимости, условия не должны содержать арифметические операции, ввиду чего ресурсы обычно представляются как отдельные позиции. Существующие критерии бездефектности, такие как простая, ослабленная и ленивая бездефектность, могут быть адаптированы к ресурсно-ориентированным сетям Петри с данными, но для их вычисления требуется решение проблемы достижимости, имеющей высокую вычислительную сложность даже для классических сетей Петри. В этой статье мы предлагаем новое свойство бездефектности, называемое ослабленной ленивой бездефектностью, которое включает в себя основные характеристики вышеупомянутых свойств и которое может быть определено путем решения проблемы покрытия, имеющей меньшую вычислительную сложность чем проблема достижимости. Мы представляем алгоритм для проверки данного свойства, доказываем его корректность и реализуем его в существующем наборе инструментов проверки бездефектности. Результаты оценки производительности подтверждают применимость алгоритма для верификации моделей среднего размера. Алгоритм можно использовать как для проверки ресурсно-ориентированных моделей, так и для предварительной проверки произвольных моделей, представленных сетями Петри с данными.