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