Метод верификации свойств реактивной системы на модели

A nes approach to verification of asynchronous discrete dynamic and active systems is discribed. This approach is founded on using temporal logic (CTL - Computation Tree Logic), Petri's nets and systems of linear Diofantine equations.