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