У статті розглядається метод опису моделювання програм за допомогою предикатів, у результаті якого створюється модель у вигляді недетермінованого скінченного автомата. Пропонується формат опису предикатів із розділенням змістовної та умовною частин. Для опису змістовної частини предиката мають застосовуватись арифметичні оператори, дужки, стандартні функції та оператори темпоральної логіки U та N. Для логічної частини предикатів, крім логічних функцій, пропонується застосовувати також операції відношення і арифметичні оператори, дужки, стандартні функції. Формування опису кожного стану автоматної моделі програми має завершуватись розгалуженням по різних гілках моделі. Для опису моделей паралельних програм введені спеціальні стани: стан-монітор для доступу різних процесів до спільних ресурсів та стан-протокол для опису незалежних паралельних гілок. Модель створюється у процесі її опису, тому не потребує подальшої верифікації.