Метрическая темпоральная логика (MTL) - это частный случай темпоральной логики . Это расширение временной логики, в которой временные операторы заменяются версиями с ограничением по времени, такими как до , следующий , с и предыдущие операторы. Это логика линейного времени, которая предполагает и чередование, и абстракции фиктивных часов. Он определяется на основе точечной слабо-монотонной целочисленной семантики. Для MTL точная сложность проблем выполнимости известна и не зависит от интервальной или точечной, синхронной (т. Е. Строго монотонной) или асинхронной (т. Е. Слабо-монотонной) интерпретации: EXPSPACE-полная. [1]
MTL был описан как выдающийся формализм спецификации для систем реального времени. [2] Полный MTL по бесконечным синхронизированным словам неразрешим. [3]
Синтаксис
Полная метрика временная логика определяется аналогично линейной временной логики , где множество неотрицательного действительного числа добавляется временные модальные операторы U и S . Формально MTL состоит из:
- конечный набор пропозициональных переменных AP ,
- эти логические операторы ¬ и ∨, и
- временнымы модальный оператор U Я (объявленный « φ пока в I ф .»), с I интервал неотрицательного числа.
- временным модальных оператор S Я (объявленный « ф так как в I ф .»), с I , как указано выше.
Если нижний индекс опущен, он неявно равен .
Обратите внимание, что следующий оператор N не считается частью синтаксиса MTL. Вместо этого он будет определяться другими операторами.
Прошлое и будущее
Прошлое фрагмент метрики временной логики , обозначенное как прошлый-MTL определяются как ограничение полной метрики временной логики без до оператора. Точно так же будущий фрагмент временной логики метрики , обозначаемый как future-MTL , определяется как ограничение полной временной логики метрики без оператора с момента.
В зависимости от авторов MTL определяется как будущий фрагмент MTL, и в этом случае полный MTL называется MTL + Past . [2] [4] Или MTL определяется как полный MTL.
Во избежание двусмысленности в этой статье используются имена full-MTL, past-MTL и future-MTL. Когда утверждения выполняются для трех логических схем, будет просто использоваться MTL.
Модель
Позволять интуитивно представляют набор моментов времени. Позволять функция, которая связывает букву с каждым моментом . Модель формулы MTL - это такая функция. Обычно,является либо синхронизированным словом, либо сигналом . В таких случаях является либо дискретным подмножеством, либо интервалом, содержащим 0.
Семантика
Позволять а также как указано выше, и пусть какое-то фиксированное время. Теперь мы собираемся объяснить, что означает, что формула MTL держится на время , который обозначается .
Позволять а также . Рассмотрим сначала формулу. Мы говорим что тогда и только тогда, когда существует какое-то время такой, что:
- а также
- для каждого с участием , .
Теперь рассмотрим формулу (произносится " поскольку в . ") Мы говорим, что тогда и только тогда, когда существует какое-то время такой, что:
- а также
- для каждого с участием , .
Определения для значений не рассмотренное выше аналогично определению в случае LTL .
Операторы, определенные из основных операторов MTL
Некоторые формулы используются настолько часто, что для них вводится новый оператор. Эти операторы обычно не считаются принадлежащими к определению MTL, но представляют собой синтаксический сахар, который обозначает более сложную формулу MTL. Сначала рассмотрим операторы, которые также существуют в LTL. В этом разделе мы исправляем Формулы MTL и .
Операторы, аналогичные LTL
Отпустить и вернуться к
Обозначим через (произносится " выпуск в , ") формула . Эта формула верна в момент если либо:
- есть время такой, что держит, и удерживать в интервале .
- каждый раз , держит.
Название «релиз» происходит от случая LTL, где эта формула просто означает, что следует всегда держать, если только выпускает его.
Предыдущий аналог выпуска обозначается (произносится " обратно в , ") и равно формуле .
Наконец и в конце концов
Обозначим через или же (произносится как "Наконец-то в , "или" В конце концов в , ") формула . Интуитивно эта формула верна в момент если есть время такой, что держит.
Обозначим через или же (произносится как "Глобально в , ",) формула . Интуитивно эта формула верна в момент если на все времена , держит.
Обозначим через а также формула, аналогичная а также , где заменяется на . Обе формулы интуитивно имеют одно и то же значение, но когда мы рассматриваем прошлое, а не будущее.
Следующее и предыдущее
Этот случай немного отличается от предыдущих, поскольку интуитивный смысл формул «Далее» и «Ранее» различается в зависимости от типа функции. считается.
Обозначим через или же (произносится как "Далее в , ") формула . Аналогично обозначим через[5] (произносится как «Ранее в, ) формула . Следующее обсуждение оператора Next справедливо и для оператора Previously, обращая вспять прошлое и будущее.
Когда эта формула оценивается по синхронизированному слову , эта формула означает, что оба:
- в следующий раз в области определения , формула будет держать.
- кроме того, расстояние между этим следующим временем и текущим временем принадлежит интервалу .
- В частности, это следующий раз, поэтому текущее время не является концом слова.
Когда эта формула оценивается по сигналу Понятие «следующий раз» не имеет смысла. Вместо этого «следующий» означает «сразу после». Точнее средства:
- содержит интервал вида а также
- для каждого , .
Другие операторы
Теперь рассмотрим операторы, не похожие ни на какие стандартные операторы LTL.
Падение и взлет
Обозначим через (произносится "рост" "), формула, которая имеет место, когда становится правдой. Точнее, либоне удерживается в ближайшем прошлом и остается в силе в настоящее время, или не имеет силы и имеет место в ближайшем будущем. Формально определяется как . [6]
Эта формула всегда остается верной для определенных слов. Действительно а также всегда держи. Таким образом, формула эквивалентна, следовательно, верно.
Симметрично обозначим через (произносится как "Падение" ), формула, которая имеет место, когда становится ложным. Таким образом, он определяется как.
История и пророчество
Теперь введем оператор пророчества , обозначенный. Обозначим через[7] формула. Эта формула утверждает, что существует первый момент в будущем, такой что держится, и время ждать этого первого момента принадлежит .
Теперь рассмотрим эту формулу над синхронизированными словами и над сигналами. Сначала мы рассматриваем рассчитанные на время слова. Предположить, что где а также представляет либо открытые, либо закрытые границы. Позволять синхронизированное слово и в своей области определения. С течением времени формула выполняется тогда и только тогда, когда также имеет место. То есть эта формула просто утверждает, что в будущем, пока интервал встречается, не должно держаться. Более того, должен держаться когда-нибудь в интервале . Действительно, в любое время такой, что держать, существует только конечное число раз с участием а также . Таким образом, обязательно существует меньшая такая.
Давайте теперь рассмотрим сигнал. Вышеупомянутая эквивалентность больше не действует в отношении сигнала. Это связано с тем, что при использовании переменных, представленных выше, может существовать бесконечное количество правильных значений для, в связи с тем, что область определения сигнала непрерывна. Таким образом, формула также гарантирует, что первый интервал, в котором держит закрыто слева.
По временной симметрии мы определяем оператор истории , обозначаемый. Мы определяем в виде . Эта формула утверждает, что существует последний момент в прошлом, такой чтопроводится. И время с этого первого момента принадлежит.
Нестрогий оператор
Семантика операторов до и после введения не учитывает текущее время. То есть для того, чтобы держать в какое-то время , ни один ни должен удерживать время . Это не всегда требуется, например, в предложении «не будет ошибок до тех пор, пока система не будет выключена», на самом деле может потребоваться, чтобы в настоящее время ошибок не было. Таким образом, мы вводим еще один оператор до тех пор, пока он не является строгим , и обозначается через, которые учитывают текущее время.
Обозначим через а также либо:
- формулы а также если , а также
- формулы а также иначе.
Для любого из операторов введенное выше, обозначим формула, в которой используются нестрогие до и грехи. Например это сокращение от .
Строгий оператор не может быть определен с помощью нестрогого оператора. То есть не существует формулы, эквивалентнойкоторый использует только нестрогий оператор. Эта формула определяется как. Эта формула никогда не может работать одновременно если требуется, чтобы держится на время .
Пример
Приведем примеры формул MTL. Еще несколько примеров можно найти в статье фрагментов MITL, таких как временная логика метрического интервала .
- заявляет, что каждая буква после ровно через одну единицу времени следует буква .
- заявляет, что нет двух последовательных появлений могут происходить точно в одну единицу времени друг от друга.
Сравнение с LTL
Стандартное (бессрочное) бесконечное слово это функция от к . Мы можем рассмотреть такое слово, используя набор времени, а функция . В этом случае для произвольная формула LTL, если и только если , где рассматривается как формула MTL с нестрогим оператором и нижний индекс. В этом смысле MTL является расширением LTL. [ требуется разъяснение ]
По этой причине формула, использующая только нестрогий оператор с нижний индекс называется формулой LTL. Это потому, что [ требуется дальнейшее объяснение ]
Алгоритмическая сложность
Фрагменты MTL
Теперь рассмотрим некоторые фрагменты MTL.
MITL
Важным подмножеством MTL является временная логика метрических интервалов ( MITL ). Это определяется аналогично MTL с ограничением, что наборы, используется в а также , являются интервалами, которые не являются одиночными и имеют границы натуральных чисел или бесконечности.
Некоторые другие подмножества MITL определены в статье MITL .
Будущие фрагменты
Future-MTL уже был представлен выше. И над синхронизированными словами, и над сигналами он менее выразителен, чем Full-MTL [4] : 3 .
Временная логика событий-часов
Фрагмент Event-Clock Temporal Logic [7] MTL, обозначенный как EventClockTL или ECL , допускает только следующие операторы:
- логические операторы and, or, not
- несвоевременные операторы до и с.
- Операторы предсказания времени и истории.
По сигналам ECL столь же выразителен, как MITL и MITL 0 . Эквивалентность двух последних логик объясняется в статье MITL 0 . Мы делаем набросок эквивалентности этих логик с помощью ECL.
Если не синглтон и формула MITL, определяется как формула MITL. Если синглтон, то эквивалентно которая является формулой MITL. Взаимно, для ECL-формула, и интервал, нижняя граница которого равна 0, эквивалентно ECL-формуле .
Выполнимость ECL над сигналами полностью соответствует требованиям PSPACE . [7]
Положительная нормальная форма
MTL-формула в положительной нормальной форме определяется почти как любая MTL-формула с двумя следующими изменениями:
- операторы Release и Back вводятся в логическом языке и больше не считаются обозначениями для некоторых других формул.
- отрицания могут применяться только к буквам.
Любая формула MTL эквивалентна формуле в нормальной форме. Это можно показать простой индукцией по формулам. Например, формула эквивалентно формуле . Точно так же союзы и дизъюнкции можно рассматривать с помощью законов Де Моргана .
Строго говоря, множество формул в положительной нормальной форме не является фрагментом MTL.
Смотрите также
- Временная логика высказываний , еще одно расширение LTL, в котором время можно измерить.
Рекомендации
- ^ Alur R., Henzinger TA (1992) Логика и модели реального времени: обзор. В: de Bakker JW, Huizing C., de Roever WP, Rozenberg G. (eds) Реальное время: теория на практике. REX 1991. Lecture Notes in Computer Science, vol 600. Springer, Berlin, Heidelberg.
- ^ a b Дж. Уакнин и Дж. Уоррелл, «О разрешимости метрической темпоральной логики», 20-й ежегодный симпозиум IEEE по логике в компьютерных науках (LICS '05), 2005 г., стр. 188–197.
- ^ Уакнин Дж., Уоррелл Дж. (2006) О метрической временной логике и неисправных машинах Тьюринга. В: Aceto L., Ingólfsdóttir A. (eds) Основы науки о программном обеспечении и вычислительных структур. FoSSaCS 2006. Lecture Notes in Computer Science, vol 3921. Springer, Berlin, Heidelberg.
- ^ a b Буйе, Патрисия ; Шевалье, Фабрис; Марки, Николас (2005). «О выразительности TPTL и MTL» . Материалы 25-й конференции по основам программных технологий и теоретической информатики : 436. doi : 10.1007 / 11590156_3 .
- ^ Малер, Одед; Никович, Деян; Пнуэли, Амир (2008). Столпы информатики . ACM. п. 478. ISBN 978-3-540-78126-4.
- ^ Никович, Деян (31 августа 2009 г.). «3» . Проверка временных и гибридных свойств: теория и приложения (Диссертация).
- ^ а б в г Henzinger, TA; Раскин, JF; Schobben, P.-Y. (1998). «Обычные языки реального времени». Конспект лекций по информатике . 1443 : 590. DOI : 10.1007 / BFb0055086 . ISBN 978-3-540-64781-2.