ків переходів.
Більше слабким, в порівнянні з еквівалентністю, є властивість включення, визначення якого збігається з визначенням еквівалентності, з точністю до заміни = на ГЌ.
Методи аналізу
Особливий інтерес викликають методи аналізу властивостей мереж Петрі, які забезпечують автоматичний аналіз модельованих систем. Спочатку розглянемо метод аналізу мереж Петрі, який заснований на використанні дерева досяжності. br/>
Дерево досяжності
Дерево досяжності представляє всі досяжні маркування мережі Петрі, а також - всі можливі послідовності запусків її переходів.
Найважливішим властивістю алгоритму побудови кінцевого дерева досяжності є те, що він за кінцеве число кроків закінчує роботу.
Аналіз властивостей мереж Петрі на основі дерева досяжності
Аналіз безпеки і обмеженості. Мережа Петрі обмежена тоді і тільки тоді, коли символ w відсутній у її дереві досяжності.
Присутність символу w в дереві досяжності ( m [х] (p) = w для деякої вершини x і позиції p) означає, що для довільного позитивного цілого k існує досяжна маркування із значенням у позиції p, більшим, ніж k (а також нескінченність безлічі досяжних маркувань). Це, у свою чергу, означає необмеженість позиції p, а отже, і самої мережі Петрі.
Відсутність символу w в дереві досяжності означає, що безліч досяжних маркувань звичайно. Отже, простим перебором можна знайти верхню межу, як для кожної позиції окремо, так і загальну верхню межу для всіх позицій. Останнє означає обмеженість мережі Петрі. Якщо межа для всіх позицій дорівнює 1, то мережа Петрі безпечна.
Аналіз збереження. Так як дерево досяжності звичайно, для кожної маркування можна обчислити суму початкової маркування. Якщо ця сума однакова для кожної досяжною маркування, то мережа Петрі є зберігає. Якщо суми не рівні, мережа не є зберігає. Якщо маркування деякої позиції збігається з w , то ця позиція повинна був виключена з розгляду.
Аналіз покриваемості. Завдання покриваемості потрібно для заданої маркування m 'визначити, чи досяжна маркування m " Ві m '. Таке завдання вирішується шляхом простого перебору вершин дерева досяжності. При цьому шукається така вершина х, що
