Метрическая темпоральная логика

Метрическая темпоральная логика (MTL) — это частный случай темпоральной логики . Это расширение темпоральной логики, в котором темпоральные операторы заменяются ограниченными по времени версиями, такими как до , следующий , с тех пор и предыдущие операторы. Это логика линейного времени, которая предполагает абстракции как чередования, так и фиктивных часов. Он определяется на основе точечной слабомонотонной семантики целочисленного времени.

MTL описывается как известный формализм спецификации для систем реального времени. ^[1] Полный MTL для бесконечных синхронизированных слов неразрешим. ^[2]

Синтаксис

Полная метрическая темпоральная логика определяется аналогично линейной темпоральной логике добавляется набор неотрицательных действительных чисел , где к темпоральным модальным операторам U и S . Формально MTL состоит из:

конечное множество пропозициональных переменных AP ,
логические операторы ¬ и ∨, и
временной интервал модальный оператор $(UI$ произносится как « $φ$ до тех пор, пока в $I$ $ψ$ .»), где $I —$ неотрицательных чисел.
временной как модальный оператор $S I$ (произносится как « $φ,$ так как в $I$ $ψ$ .»), с $I,$ указано выше.

Когда нижний индекс опущен, он неявно равен $[0,\infty )$ .

Обратите внимание, что следующий оператор N не считается частью синтаксиса MTL. Вместо этого он будет определен из других операторов.

Прошлое и будущее

Прошлый фрагмент метрической темпоральной логики , обозначаемый как Past-MTL, определяется как ограничение полной метрической темпоральной логики без оператора Until. Аналогично, будущий фрагмент метрической темпоральной логики , обозначаемый как Future-MTL, определяется как ограничение полной метрической темпоральной логики без оператора с тех пор.

В зависимости от авторов, MTL либо определяется как будущий фрагмент MTL, и в этом случае полный MTL называется MTL+Past . ^[1]^[3] Или MTL определяется как полный MTL.

Во избежание двусмысленности в этой статье используются названия полный-MTL, прошлый-MTL и будущий-MTL. Когда утверждения справедливы для трех логик, будет просто использоваться MTL.

Модель

Позволять $T\subseteq \mathbb {R} _{+}$ интуитивно представлять наборточек во времени. Позволять $\gamma :T\to A$ функция, которая связывает букву скаждый момент $t\in T$ . Модель формулы MTL:такая функция $\gamma$ . Обычно, $\gamma$ являетсялибо синхронизированное слово , либо сигнал . Вте случаи, $T$ является либо дискретным подмножеством, либо интерваломсодержащий 0.

Семантика

Позволять $T$ и $\gamma$ как указано выше, и пусть $t\in T$ некоторое фиксированное время. Сейчас мы объясним, что это значитчто формула MTL $\phi$ держится вовремя $t$ ,который обозначается $\gamma ,t\models \phi$ .

Позволять $I\subseteq \mathbb {R} _{+}$ и $\phi ,\psi \in MTL$ . Сначала рассмотрим формулу $\phi {\mathcal {U}}_{I}\psi$ . Мы говоримчто $\gamma ,t\models \phi {\mathcal {U}}_{I}\psi$ тогда и только тогда, когдасуществует некоторое время $t'\in I+t$ такой, что:

$\gamma ,t'\models \psi$ и
для каждого $t''\in T$ с $t<t''<t'$ , $\gamma ,t''\models \phi$ .

Теперь рассмотрим формулу $\phi {\mathcal {S}}_{I}\psi$ (произносится « $\phi$ св $I$ $\psi$ .») Мы говоримчто $\gamma ,t\models \phi {\mathcal {S}}_{I}\psi$ тогда и только тогда, когдасуществует некоторое время $t'\in I-t$ такой, что:

$\gamma ,t'\models \psi$ и
для каждого $t''\in T$ с $t'<t''<t$ , $\gamma ,t''\models \phi$ .

Определения $\gamma ,t\models \phi$ для ценностейиз $\phi$ не рассмотренное выше аналогично определениюв случае LTL .

Операторы, определенные на основе базовых операторов MTL

Некоторые формулы используются настолько часто, что для них вводится новый оператор.их. Эти операторы обычно не считаются принадлежащими копределение MTL, но являются синтаксическим сахаром , обозначающим болеесложная формула MTL. Сначала мы рассмотрим операторы, которые также существуют в LTL. Вэтот раздел, мы исправим $\phi ,\psi$ Формулы MTLи $I\subseteq \mathbb {R} _{+}$ .

Операторы аналогичные операторам LTL

Выпустить и вернуться к

Обозначим через $\phi {\mathcal {R}}_{I}\psi$ (произносится « $\phi$ выпускатьв $I$ , $\psi$ ")формула $\neg \phi {\mathcal {U}}_{I}\neg \psi$ . Эта формула имеет местово время $t$ если либо:

есть немного времени $t'\in t+I$ такой, что $\phi$ держится, и $\psi$ держать в интервале $(t,t')\cap (t+I)$ .
в каждый момент времени $t'\in t+I$ , $\phi$ держит.

Название «выпуск» происходит от случая LTL, где эта формула простоозначает, что $\phi$ всегда должен удерживаться,пока не $\psi$ выпускает его.

Прошлый аналог выпуска обозначается $\phi {\mathcal {B}}_{I}\psi$ (произносится « $\phi$ вернуться кв $I$ , $\psi$ ") и равенформула $\neg \phi {\mathcal {S}}_{I}\neg \psi$ .

Наконец и в конце концов

Обозначим через $\Diamond _{I}\phi$ или ${\mathcal {F}}_{I}\phi$ (произносится «Наконец-тов $I$ , $\phi$ или «В конце концовв $I$ , $\phi$ ") формула $\top {\mathcal {U}}_{I}\phi$ . Интуитивно эта формула справедлива в момент времени $t$ если будет время $t'\in t+I$ такойчто $\phi$ держит.

Обозначим через $\Box _{I}\phi$ или ${\mathcal {G}}_{I}\phi$ (произносится «Глобальнов $I$ , $\phi$ ",)формула $\neg \Diamond _{I}\neg \phi$ . Интуитивно эта формуладержится вовремя $t$ если на все времена $t'\in t+I$ , $\phi$ держит.

Обозначим через ${\overleftarrow {\Box }}_{I}\phi$ и ${\overleftarrow {\Diamond }}_{I}\phi$ формула похожак $\Box _{I}\phi$ и $\Diamond _{I}\phi$ ,где ${\mathcal {U}}$ заменяется на ${\mathcal {S}}$ . Обе формулы интуитивно имеют один и тот же смысл, но когда мырассматривать прошлое вместо будущего.

Следующий и предыдущий

Этот случай немного отличается от предыдущих, поскольку интуитивно понятный смысл формул «Далее» и «Предыдущее» различается в зависимости от вида функции. $\gamma$ обдуманный.

Обозначим через $\bigcirc _{I}\phi$ или ${\mathcal {N}}_{I}\phi$ (произносится «Следующий в $I$ , $\phi$ ")формула $\bot {\mathcal {U}}_{I}\phi$ . Аналогично обозначим через $\ominus _{I}\phi$ ^[4] (произносится «Ранее в $I$ , $\phi$ ) формула $\bot {\mathcal {S}}_{I}\phi$ . Следующее обсуждение оператора Next также справедливо и для оператора Ранее, меняя местами прошлое и будущее.

Когда эта формула вычисляется по синхронизированному слову $\gamma :T\to A$ , эта формулаозначает, что оба:

в следующий раз в области определения $T$ , формула $\phi$ будет держаться.
при этом расстояние между этим следующим временем и текущим временем принадлежит интервалу $I$ .
В частности, этот следующий раз имеет место, поэтому текущее время не является концом слова.

Когда эта формула оценивается по сигналу $\gamma$ , понятие следующего разане имеет смысла. Вместо этого «следующий» означает «сразу после». Болееименно так $\gamma ,t\models \circ \phi$ означает:

$I$ содержит интервал вида $(0,\epsilon )$ и
для каждого $t'\in (t,t+\epsilon )$ , $\gamma ,t'\models \phi$ .

Другие операторы

Теперь мы рассмотрим операторы, которые не похожи ни на один стандартный оператор LTL.

Падение и взлет

Обозначим через $\uparrow \phi$ (произносится как «подъем $\phi$ "), формула, которая справедлива, когда $\phi$ становится правдой. Точнее, либо $\phi$ не имело места в ближайшем прошлом и имеет место в настоящее время, или оно не имеет места и имеет место в ближайшем будущем. Формально $\uparrow \phi$ определяется как $(\phi \land (\neg \phi {\mathcal {S}}\top ))\lor (\neg \phi \land (\phi {\mathcal {U}}\top ))$ . ^[5]

В отношении слов, рассчитанных по времени, эта формула всегда справедлива. Действительно $\phi {\mathcal {U}}\top$ и $\neg \phi {\mathcal {S}}\top$ всегда держи. Таким образом, формула эквивалентна $\phi \lor \neg \phi$ , следовательно, верно.

Симметрией обозначим через $\downarrow \phi$ (произносится «Падение $\phi$ ), формула, которая справедлива, когда $\phi$ становится ложным. Таким образом, он определяется как $(\neg \phi \land (\phi {\mathcal {S}}\top ))\land (\phi \land (\neg \phi {\mathcal {U}}\top ))$ .

История и пророчество

Теперь введем оператор пророчества , обозначаемый $\triangleright$ . Обозначим через $\triangleright _{I}\phi$ ^[6] формула $\neg \phi {\mathcal {U}}_{I}\phi$ . Эта формула утверждает, что в будущем существует такой первый момент, что $\phi$ сохраняется, и время ожидания этого первого момента принадлежит $I$ .

Теперь мы рассмотрим эту формулу для синхронизированных слов и сигналов. Сначала мы рассматриваем синхронизированные слова. Предположим, что $I=\mid a,b\mid '$ где $\mid$ и $\mid '$ представляет либо открытые, либо закрытые границы. Позволять $\gamma$ временное слово и $t$ в своей области определения. По времени слова, формула $\gamma ,t\models \triangleright _{I}\phi$ имеет место тогда и только тогда, когда $\gamma ,t\models \Box _{]0,b[\setminus I}\neg \phi \land \Diamond _{I}\phi$ тоже держит. То есть эта формула просто утверждает, что в будущем, пока интервал $t+I$ встречается, $\phi$ не должно держаться. Более того, $\phi$ должно удерживаться где-то в интервале $t+I$ . Действительно, учитывая любое время $t''\in t+I$ такой, что $\gamma ,t''\models \phi$ верно, существует только конечное число времени $t'\in t+I$ с $t'<t''$ и $\gamma ,t'\models \phi$ . Таким образом, обязательно существует меньший такой $t''$ .

Давайте теперь рассмотрим сигнал. Упомянутая выше эквивалентность больше не распространяется на сигнал. Это связано с тем, что при использовании введенных выше переменных может существовать бесконечное количество правильных значений для $t'$ , в связи с тем, что область определения сигнала непрерывна. Таким образом, формула $\triangleright _{I}\phi$ также гарантирует, что первый интервал, в котором $\phi$ трюм закрыт слева.

В силу временной симметрии мы определяем оператор истории , обозначаемый $\triangleleft$ . Мы определяем $\triangleleft _{I}\phi$ как $\neg \phi {\mathcal {S}}_{I}\phi$ . Эта формула утверждает, что в прошлом существует такой последний момент, что $\phi$ держал. И время, прошедшее с этого первого момента, принадлежит $I$ .

Нестрогий оператор

Семантика операторов до и после введения не учитывает текущее время. То есть для того, чтобы $\phi _{1}{\mathcal {U}}\phi _{2}$ держаться какое-то время $t$ , ни один $\phi _{1}$ ни $\phi _{2}$ должен удерживать время $t$ . Это не всегда желательно, например, в предложении «нет ошибок, пока система не будет выключена», на самом деле может быть желательно, чтобы в текущий момент ошибок не было. Таким образом, мы вводим еще один оператор до тех пор, пока не будем называть его нестрогим до тех пор , пока не обозначим через ${\overline {\mathcal {U}}}$ , которые учитывают текущее время.

Обозначим через $\phi _{1}{\overline {\mathcal {U}}}_{I}\phi _{2}$ и $\phi _{1}{\overline {\mathcal {S}}}_{I}\phi _{2}$ или:

формулы $\phi _{2}\lor (\phi _{1}\land (\phi _{1}{\mathcal {U}}_{I}\phi _{2}))$ и $\phi _{2}\lor (\phi _{1}\land (\phi _{1}{\mathcal {S}}_{I}\phi _{2}))$ если $0\in I$ , и
формулы $\phi _{1}\land (\phi _{1}{\mathcal {U}}_{I}\phi _{2})$ и $\phi _{1}\land (\phi _{1}{\mathcal {S}}_{I}\phi _{2})$ в противном случае.

Для любого из операторов ${\mathcal {O}}$ введенное выше, обозначим ${\overline {\mathcal {O}}}$ формула, в которой используются нестрогие до и с тех пор. Например ${\overline {\Diamond }}p$ это аббревиатура от $\top {\overline {\mathcal {U}}}p$ .

Строгий оператор не может быть определен с помощью нестрогого оператора. То есть не существует формулы, эквивалентной $\bigcirc _{I}p$ который использует только нестрогий оператор. Эта формула определяется как $\bot {\mathcal {U}}_{I}p$ . Эта формула никогда не может выполняться одновременно $t$ если это требуется $\bot$ держится вовремя $t$ .

Пример

Теперь приведем примеры формул MTL. Еще несколько примеров можно найти в статье фрагментов MITL, таких как метрическая интервальная темпоральная логика .

$\Box (p\implies \Diamond _{\{1\}}q)$ утверждает, что каждая буква $p$ ровно через единицу времени следует буква $q$ .
$\Box (p\implies \neg \Diamond _{\{1\}}p)$ утверждает, что никакие два последовательных появления $p$ могут произойти ровно в одной единице времени друг от друга.

Сравнение с ЛТЛ

Стандартное (неограниченное по времени) бесконечное слово $w=a_{0},a_{1},\dots ,$ этофункция от $\mathbb {N}$ к $A$ . Мы можемрассмотрим такое слово, используя набор времени $T=\mathbb {N}$ ,и функция $\gamma (i)=a_{i}$ . В этом случае,для $\phi$ произвольный LTLформула, $w,i\models \phi$ если и толькоесли $\gamma ,i\models \phi$ , где $\phi$ являетсярассматривается как формула MTL с нестрогим оператором и $[0,\infty )$ индекс. В этом смысле MTL является расширением LTL. ^{[ нужны разъяснения ]}

По этой причине формула, использующая только нестрогий оператор с $[0,\infty )$ нижний индекс называется формулой LTL. Это потому, что ^{[ нужны дальнейшие объяснения ]}

Алгоритмическая сложность

Выполнимость ECL по сигналам является EXPSPACE - полной . ^[6]

Фрагменты МТЛ

Теперь рассмотрим некоторые фрагменты MTL.

МИТЛ

Важным подмножеством MTL является метрическая интервальная временная логика ( MITL ). Это определяется аналогично MTL, сограничение на то, что множества $I$ , используется в ${\mathcal {U}}$ и ${\mathcal {S}}$ , являются интервалами, которые неодиночные элементы, границы которых являются натуральными числами или бесконечностью.

Некоторые другие подмножества MITL определены в статье MITL .

Будущие фрагменты

Future-MTL уже был представлен выше. И по синхронизированным словам, и по сигналам он менее выразителен, чем Full-MTL. ^[3]^: 3.

Временная логика Event-Clock

Фрагмент Event-Clock Temporal Logic ^[6] MTL, обозначаемый EventClockTL или ECL , допускает только следующие операторы:

логические операторы и, или, не
операторы без времени до и после.
Временное пророчество и операторы истории.

Что касается сигналов, ECL столь же выразителен, как MITL и MITL ₀ . Эквивалентность между двумя последними логиками объясняется в статье MITL ₀ . Мы обрисуем эквивалентность этой логики с ECL.

Если $I$ не является синглтоном и $\phi$ это формула MITL, $\triangleright _{I}\phi$ определяется как формула MITL. Если $I=\{i\}$ является синглтоном, тогда $\triangleright _{I}\phi$ эквивалентно $\Box _{]0,i[}\neg \phi \land \Diamond _{]0,i]}\phi$ что представляет собой MITL-формулу. Взаимно, для $\psi$ ECL-формула и $I$ интервал, нижняя граница которого равна 0, $\Box _{I}\psi$ эквивалентно формуле ECL $\neg \triangleright _{I}\neg \psi$ .

Выполнимость ECL по сигналам является PSPACE-полной . ^[6]

Положительная нормальная форма

Формула MTL в положительной нормальной форме определяется почти как любая формула MTL с двумя следующими изменениями:

операторы Release и Back введены в логический язык и больше не считаются обозначениями некоторых других формул.
Отрицания можно применять только к буквам.

Любая формула MTL эквивалентна формуле в нормальной форме. Это можно показать простой индукцией по формулам. Например, формула $\neg (\phi {\mathcal {U}}_{S}\psi )$ эквивалентно формуле $(\neg \phi ){\mathcal {R}}_{S}(\neg \psi )$ . Точно так же соединения и дизъюнкции можно рассматривать, используя законы Де Моргана .

Строго говоря, множество формул в положительной нормальной форме не является фрагментом MTL.

См. также

Временная пропозициональная темпоральная логика , еще одно расширение LTL, в котором можно измерить время.

Ссылки

^ Jump up to: ^а ^б Дж. Уакнин и Дж. Уоррелл, «О разрешимости метрической темпоральной логики», 20-й ежегодный симпозиум IEEE по логике в информатике (LICS '05), 2005, стр. 188-197.
^ Уакнин Дж., Уоррелл Дж. (2006) О метрической временной логике и неисправных машинах Тьюринга. В: Ачето Л., Ингольфсдоттир А. (ред.) Основы науки о программном обеспечении и вычислительных структур. FoSSaCS 2006. Конспекты лекций по информатике, том 3921. Springer, Берлин, Гейдельберг.
^ Jump up to: ^а ^б Буйе, Патрисия ; Шевалье, Фабрис; Марки, Николас (2005). «О выраженности ТПТЛ и МТЛ» . В Сундаре Саруккае; Сандип Сен (ред.). FSTTCS 2005: Основы программных технологий и теоретической информатики, Труды . 25-я Международная конференция, Хайдарабад, Индия, 15–18 декабря 2005 г. Конспекты лекций по информатике. Том. 3821. с. 436. дои : 10.1007/11590156_35 . ISBN 978-3-540-32419-5 .
^ Малер, Одед; Никович, Деян; Пнуэли, Амир (2008). «Проверка временных свойств дискретного, временного и непрерывного поведения». Столпы информатики . АКМ. п. 478. ИСБН 978-3-540-78126-4 .
^ Никович, Деян (31 августа 2009 г.). «3» . Проверка временных и гибридных свойств: теория и приложения (Диссертация).
^ Jump up to: ^а ^б ^с ^д Хензингер, штат Техас; Раскин, Дж. Ф.; Шоббенс, П.-Ю. (1998). «Обычные языки реального времени». Автоматы, языки и программирование . Конспекты лекций по информатике. Том. 1443. с. 590. дои : 10.1007/BFb0055086 . ISBN 978-3-540-64781-2 .

[Decidabilty_Of_MITL-1] Jump up to: ^а ^б Дж. Уакнин и Дж. Уоррелл, «О разрешимости метрической темпоральной логики», 20-й ежегодный симпозиум IEEE по логике в информатике (LICS '05), 2005, стр. 188-197.

[MTL_and_Faulty_Turing_Machine-2] Уакнин Дж., Уоррелл Дж. (2006) О метрической временной логике и неисправных машинах Тьюринга. В: Ачето Л., Ингольфсдоттир А. (ред.) Основы науки о программном обеспечении и вычислительных структур. FoSSaCS 2006. Конспекты лекций по информатике, том 3921. Springer, Берлин, Гейдельберг.

[ExpressivenesOfTPTLAndMtl-3] Jump up to: ^а ^б Буйе, Патрисия ; Шевалье, Фабрис; Марки, Николас (2005). «О выраженности ТПТЛ и МТЛ» . В Сундаре Саруккае; Сандип Сен (ред.). FSTTCS 2005: Основы программных технологий и теоретической информатики, Труды . 25-я Международная конференция, Хайдарабад, Индия, 15–18 декабря 2005 г. Конспекты лекций по информатике. Том. 3821. с. 436. дои : 10.1007/11590156_35 . ISBN 978-3-540-32419-5 .

[LTLPlusPast-4] Малер, Одед; Никович, Деян; Пнуэли, Амир (2008). «Проверка временных свойств дискретного, временного и непрерывного поведения». Столпы информатики . АКМ. п. 478. ИСБН 978-3-540-78126-4 .

[Checking_Timed_and_Hybrid_Properties-5] Никович, Деян (31 августа 2009 г.). «3» . Проверка временных и гибридных свойств: теория и приложения (Диссертация).

[RegularRealTime-6] Jump up to: ^а ^б ^с ^д Хензингер, штат Техас; Раскин, Дж. Ф.; Шоббенс, П.-Ю. (1998). «Обычные языки реального времени». Автоматы, языки и программирование . Конспекты лекций по информатике. Том. 1443. с. 590. дои : 10.1007/BFb0055086 . ISBN 978-3-540-64781-2 .

[1]

[2]

[3]

[4]

[5]

[6]