Метрический интервал временной логики

Фрагмент метрической темпоральной логики

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

Определение

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

Отличие от MTL

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

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

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

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

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

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

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

• между 9 и 10 единицами времени назад P было истинным.
• Непосредственно перед моментом времени t P было ложным.

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

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

Примеры

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

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

Фрагменты

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

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

Открытые и закрытые MITL

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

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

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

Плоский и коплоский MITL

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

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

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

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

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

МИТЛ0,∞и МИТЛ0

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

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

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

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

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

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

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

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

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

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

R. Alur, T. Feder и TA Henzinger. Преимущества расслабленной пунктуальности. Journal of the ACM, 43(1):116–146, 1996. R. Alur и TA Henzinger. Логики и модели реального времени: обзор. In Proc. REX Workshop, Real-time: Theory in Practice, страницы 74–106. LNCS 600, Springer, 1992. TA Henzinger. Речь идет о времени: обзор логик реального времени. In Proc. CONCUR'98, страницы 439–454. LNCS 1466, Springer, 1998.

Ссылки

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