применяют темпоральную логику, позволяющую описывать, как поведение системы протекает во времени.
Важным вопросом спецификации является полнота. Метод проверки на модели дает возможность убедиться, что модель проектируемой системы соответствует заданной спецификации, однако определить, охватывает ли заданная спецификация все свойства, которыми должна обладать система, невозможно.
Исторические сведения
Модальные логики (Аристотель)
Аксиоматизация модальных логик (C. I. Lewis, 1910)
Семантика возможных миров (S. Kripke, 1959)
Темпоральные логики (A. N. Prior. 1957)
Применение математической логики для доказательства правильности программ (C. A. Hoare, M. Floyd, 1968)
Динамические логики (V. Pratt, 1976)