ИСТИНА

Мы предлагаем более сложный язык спецификаций, обобщающий классические темпоральные логики на случай вычислительных систем, получающих сигналы от окружения. Этот язык может быть использован и для спецификации поведения обычных моделей Крипке, причём его выразительная сила значительно превосходит возможности логики. Ниже мы описываем синтаксис и семантику предложенного языка и формулируем утверждения о его выразительной силе, а также приводим основные идеи, лежащие в основе доказательств этих утверждений.