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

При проверке модели Метрическая Интервальная Темпоральная Логика (MITL) является фрагментом Метрической Темпоральной Логики (MTL). Этот фрагмент часто предпочтительнее MTL, поскольку некоторые проблемы, неразрешимые для MTL, становятся разрешимыми для MITL.

Определение

Формула MITL — это формула MTL, в которой каждый набор действительных чисел, используемый в нижнем индексе, представляет собой интервалы, которые не являются одиночными, и чьи границы являются либо натуральными числами, либо бесконечными. ^{[ нужна ссылка ]}

Отличие от МТЛ

MTL может выражать такое утверждение, как предложение S : « P состоялось ровно десять единиц времени назад». В МИТЛ это невозможно. Вместо этого MITL может сказать T : « P удерживалось между 9 и 10 единицами времени назад». Поскольку MITL может выражать T , но не S , в некотором смысле MITL является ограничением MTL, которое допускает только менее точные утверждения.

Проблемы, которых MITL избегает

Одна из причин избегать такого утверждения, как S , заключается в том, что его значение истинности может меняться произвольное количество раз за одну единицу времени. Действительно, значение истинности этого утверждения может меняться столько раз, сколько меняется значение истинности P , а само P может меняться произвольное количество раз в одной единице времени.

Давайте теперь рассмотрим систему, такую как временной автомат или сигнальный автомат , которые хотят знать в каждый момент времени, выполняется S или нет. Эта система должна вспомнить все, что произошло за последние 10 единиц времени. Как видно выше, это означает, что он должен вспомнить сколь угодно большое количество событий. Это не может быть реализовано системой с ограниченной памятью и тактовой частотой.

Ограниченная изменчивость

Одним из основных преимуществ MITL является то, что каждый оператор обладает свойством ограниченной изменчивости. Пример:

Учитывая утверждение T, определенное выше. Каждый раз, когда значение истинности T переключается с ложного на истинное, оно остается истинным как минимум в течение одной единицы времени. Доказательство: В момент времени t , когда T становится истинным, это означает, что:

между 9 и 10 единицами времени назад P было правдой.
незадолго до времени P t было ложным.

Следовательно, P было истинным ровно 9 единиц времени назад. Отсюда следует, что для каждого $t'\in [0,1]$ , во время $t+t'$ , П был правдой $9+t'$ единицы времени назад. С $9+t'\in [9,10]$ , во время $t'$ , T имеет место.

времени хочет знать значение T. Система в каждый момент Такая система должна помнить, что произошло за последние десять единиц времени. Однако благодаря свойству ограниченной изменчивости он должен вспомнить не более 10 единиц времени, когда T станет истинным. И, следовательно, 11 раз, когда T становится ложным. Таким образом, эта система должна запомнить не более 21 события и, следовательно, может быть реализована как синхронизированный или сигнальный автомат .

Примеры

Примеры формул MITL:

$\square \diamond _{(0,1)}p$ утверждает, что письмо $p$ появляется хотя бы один раз в каждом открытом интервале длины 1.
$\triangleright _{\{i\}}p$ где $\triangleright _{\{i\}}p$ — оператор пророчества, определяемый как $\square _{(0,i)}\neg p\land \diamond _{(0,i]}p$ и в котором говорится, что первое появление $p$ в будущем находится в $i$ единица времени.
$p\land \square (p\implies \triangleright _{\{1\}}p)$ заявляет, что $p$ выполняется ровно в каждый интегральный момент времени, а не когда-либо еще.

Фрагменты

Безопасность-MTL _0,∞

Фрагмент Safety-MTL _0,v определяется как подмножество MITL _0,∞ , содержащее только формулы в положительной нормальной форме , где интервал каждого оператора до тех пор, пока не имеет верхнюю границу. Например, формула $\Box (a\implies \Diamond _{(0,1]}b)$ в котором говорится, что каждый $a$ за ним, менее чем через одну единицу времени, следует $b$ , принадлежит этой логике. ^[1]

Открытый и закрытый МИТЛ

Фрагмент Open-MTL содержит формулу в положительной нормальной форме такую, что:

для каждого ${\mathcal {U}}_{I}$ , $I$ открыт, и
для каждого ${\mathcal {R}}_{I}$ , $I$ закрыт.

Фрагмент Closed-MITL содержит отрицание формул Open-MITL .

Квартира и Кофлат MITL

Фрагмент Flat-MTL содержит формулу в положительной нормальной форме такую, что:

для каждого $\phi _{1}{\mathcal {U}}_{I}\phi _{2}$ , если $I$ неограничен, то $\phi _{1}$ это LTL-формула
для каждого $\phi _{1}{\mathcal {R}}_{I}\phi _{2}$ , если $I$ неограничен, то $\phi _{2}$ это LTL-формула

Фрагмент Colat-MITL содержит отрицание формул Flat-MITL .

Нестрогий вариант

Учитывая любой фрагмент L , фрагмент L ^нс — это ограничение L , в котором только нестрогие используются операторы.

MITL _0,∞ и MITL ₀

Для любого фрагмента L фрагмент L _0,∞ является подмножеством L , где нижняя граница каждого интервала равна 0, а верхняя граница равна бесконечности. Аналогично обозначим через L ₀ (соответственно L _∞ ) подмножество L такое, что нижняя граница каждого интервала равна 0 (соответственно верхняя граница каждого интервала равна ∞).

Выразительность над сигналами

В отношении сигналов MITL ₀ столь же выразителен, как и MITL. Это можно доказать, применив следующие правила переписывания к формуле MITL. ^[2]

$\phi {\mathcal {U}}_{(a,b)}\psi$ эквивалентно $\Box _{(0,a]}\phi {\mathcal {U}}\psi \land \Diamond _{(a,b)}\psi$ (построение полузамкнутых и замкнутых интервалов аналогично).
$\Diamond _{(a,b)}\phi$ эквивалентно $\Diamond _{(2a-b,a)}\Box _{(0,b-a)}\Diamond _{(0,b-a)}\phi$ если $2a-b\geq 0$ .
$\Diamond _{(a,b)}\phi$ эквивалентно $\Diamond _{(a,b-a)}\Diamond _{(0,a)}\phi$ если $a<b$ .
$\Diamond _{(a,+\infty )}\phi$ эквивалентно $\Box _{(0,a)}\Diamond \phi$ .

Применение этих правил переписывания экспоненциально увеличивает размер формулы. Действительно, цифры $a$ и $b$ традиционно записываются в двоичном формате, и эти правила следует применять. $O\left({\frac {b}{b-a}}\right)$ раз.

Выразительность в отношении временных слов

В отличие от сигналов, MITL строго более выразителен, чем MITL _0,∞ . Приведенные выше правила переписывания не применяются в случае синхронизированных слов, поскольку для переписывания $\Diamond _{(a,b)}$ предположение должно заключаться в том, что какое-то событие происходит между моментами времени 0 и $a$ , что не обязательно так.

Проблема выполнимости

Проблема определения того, выполнима ли формула MITL для сигнала, находится в PSPACE-complete . ^[3]

Необходимы ссылки

Р. Алур, Т. Федер и Т. А. Хензингер. Преимущества расслабленной пунктуальности. Журнал ACM, 43(1):116–146, 1996.Р. Алур и Т. А. Хензингер. Логика и модели реального времени: обзор. В Proc. Семинар REX, В реальном времени: теория на практике, страницы 74–106. LNCS 600, Спрингер, 1992 г.Т. А. Хенцингер. Речь идет о времени: обзор логики реального времени. В Proc. КОНКУР'98, стр. 439–454. LNCS 1466, Спрингер, 1998 г.

Ссылки

^ Булычев, Петр; Дэвид, Александр; Ларсен, Ким Г.; Гуанъюань, Ли (июнь 2014 г.). «Синтез эффективного регулятора для фрагмента МТЛ _0,∞ ». Акта Информатика . 51 (3–4): 166. doi : 10.1007/s00236-013-0189-z . S2CID 253779696 .
^ Берсани, Марчелло; Росси, Маттео; Сан-Пьетро, Пьерлуиджи (2013). «Инструмент для определения выполнимости метрической темпоральной логики непрерывного времени» (PDF) . 2013 20-й Международный симпозиум по временному представлению и рассуждению . Том. 20. с. 202. дои : 10.1109/TIME.2013.20 . hdl : 11311/964235 . ISBN 978-1-4799-2240-6 .
^ Хензингер, штат Техас; Раскин, Дж. Ф.; Шоббенс, П.-Ю. (1998). «Обычные языки реального времени». Автоматы, языки и программирование . Конспекты лекций по информатике. Том. 1443. с. 591. дои : 10.1007/BFb0055086 . ISBN 978-3-540-64781-2 .

[1] Булычев, Петр; Дэвид, Александр; Ларсен, Ким Г.; Гуанъюань, Ли (июнь 2014 г.). «Синтез эффективного регулятора для фрагмента МТЛ _0,∞ ». Акта Информатика . 51 (3–4): 166. doi : 10.1007/s00236-013-0189-z . S2CID 253779696 .

[2] Берсани, Марчелло; Росси, Маттео; Сан-Пьетро, Пьерлуиджи (2013). «Инструмент для определения выполнимости метрической темпоральной логики непрерывного времени» (PDF) . 2013 20-й Международный симпозиум по временному представлению и рассуждению . Том. 20. с. 202. дои : 10.1109/TIME.2013.20 . hdl : 11311/964235 . ISBN 978-1-4799-2240-6 .

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

[1]

[2]

[3]