В проверке модели , поле информатики , А разница связана матрица (DBM) представляет собой структура данных используются для представления некоторых выпуклых многогранников , называемых зонами . Эта структура может использоваться для эффективного выполнения некоторых геометрических операций над зонами, таких как проверка пустоты, включения, равенства и вычисление пересечения и суммы двух зон. Например, он используется в программе проверки моделей Uppaal ; где он также распространяется как независимая библиотека. [1]
Точнее, есть понятие канонической DBM; существует взаимно однозначное отношение между каноническими DBM и зонами, и из каждой DBM может быть эффективно вычислен канонический эквивалент DBM. Таким образом, равенство зон можно проверить, проверив равенство канонических DBM.
Зона
Матрица разностных границ используется для представления выпуклых многогранников. Эти многогранники называются зонными . Теперь они определены. Формально зона определяется уравнениями вида, , а также , с участием а также некоторые переменные и константа.
Зоны первоначально назвать область , [2] , но в настоящее время это название , как правило , обозначают область , особый вид зоны. Интуитивно регион можно рассматривать как минимальные непустые зоны, в которых константы, используемые в ограничении, ограничены.
Дано переменных, ровно возможны различные не избыточные ограничения, ограничения, использующие одну переменную и верхнюю границу, ограничений, которые используют одну переменную и нижнюю границу, и для каждого из упорядоченные пары переменных , верхняя граница . Однако произвольный выпуклый многогранник вможет потребовать сколь угодно большого количества ограничений. Даже когда, может быть произвольно большое количество неизбыточных ограничений , для некоторые константы. Это причина, по которой DBM не могут быть расширены из зон в выпуклые многогранники.
Пример
Как указано во введении, мы рассматриваем зону, определяемую набором операторов вида , , а также , с участием а также некоторые переменные и константа. Однако некоторые из этих ограничений либо противоречивы, либо избыточны. Приведем теперь такие примеры.
- ограничения а также противоречивы. Следовательно, когда обнаруживаются два таких ограничения, определенная зона становится пустой.
- ограничения а также избыточны. Второе ограничение подразумевается первым. Следовательно, когда в определении зоны обнаруживаются два таких ограничения, второе ограничение может быть удалено.
Мы также приводим пример, показывающий, как создавать новые ограничения из существующих ограничений. Для каждой пары часов а также , DBM имеет ограничение в виде , где либо <, либо ≤. Если такое ограничение не может быть найдено, ограничениеможет быть добавлен к определению зоны без потери общности. Но в некоторых случаях можно найти более точное ограничение. Сейчас будет приведен такой пример.
- ограничения , подразумевает, что . Таким образом, если предположить, что нет других ограничений, таких как или же принадлежит определению, ограничение добавляется к определению зоны.
- ограничения , подразумевает, что . Таким образом, если предположить, что нет других ограничений, таких как или же принадлежит определению, ограничение добавляется к определению зоны.
- ограничения , подразумевает, что . Таким образом, если предположить, что нет других ограничений, таких как или же принадлежит определению, ограничение добавляется к определению зоны.
Фактически, два первых случая выше являются частными случаями третьего случая. Действительно, а также можно переписать как а также соответственно. Таким образом, ограничение добавленное в первом примере аналогично ограничению, добавленному в третьем примере.
Определение
Теперь исправим моноид который является подмножеством реальной линии. Это Моноид традиционно множество целых чисел , рациональных , вещественных чисел , или их подмножество неотрицательных чисел.
Ограничения
Чтобы определить матрицу привязки различий структур данных , сначала необходимо предоставить структуру данных для кодирования атомарных ограничений. Кроме того, мы вводим алгебру атомарных связей. Эта алгебра похожа на тропическое полукольцо с двумя модификациями:
- Вместо можно использовать произвольный упорядоченный моноид.
- Чтобы различать "" а также ""набор элементов алгебры должен содержать информацию о том, строгий порядок или нет.
Определение ограничений
Набор выполнимых ограничений определяется как набор пар вида:
- , с участием , который представляет собой ограничение вида ,
- , с участием , где не является минимальным элементом , который представляет собой ограничение вида ,
- , что означает отсутствие ограничения.
Набор ограничений содержит все выполнимые ограничения, а также следующее невыполнимое ограничение:
- .
Подмножество не может быть определен с использованием такого рода ограничений. В более общем смысле, некоторые выпуклые многогранники не могут быть определены, если упорядоченный моноид не имеет свойства наименьшей верхней границы , даже если каждое из ограничений в его определении использует не более двух переменных.
Работа с ограничениями
Чтобы сгенерировать одно ограничение из пары ограничений, применяемых к одной (паре) переменной, мы формализуем понятие пересечения ограничений и порядка над ограничениями. Точно так же, чтобы определить новые ограничения из существующих ограничений, также должно быть определено понятие суммы ограничений.
Порядок ограничений
Теперь мы определим отношение порядка над ограничениями. Этот порядок символизирует отношение включения.
Во-первых, набор рассматривается как упорядоченный набор, где <уступает ≤. Интуитивно этот порядок выбран, потому что набор, определяемый строго входит в набор, определяемый . Затем мы утверждаем, что ограничение меньше чем если либо или же ( а также меньше чем ). То есть порядок ограничений - это лексикографический порядок, применяемый справа налево. Обратите внимание, что это общий заказ . Еслиимеет свойство наименьшей верхней границы (или свойство наибольшей нижней границы ), то набор ограничений также имеет его.
Пересечение ограничений
Пересечение двух ограничений, обозначенное как , тогда просто определяется как минимум из этих двух ограничений. Если имеет свойство наибольшей-нижней границы, то также определяется пересечение бесконечного числа ограничений.
Сумма ограничений
Учитывая две переменные а также к которым применяются ограничения а также , теперь мы объясним, как сгенерировать ограничение, которому удовлетворяет . Это ограничение называется суммой двух вышеупомянутых ограничений и обозначается как и определяется как .
Ограничения как алгебра
Вот список алгебраических свойств, которым удовлетворяет набор ограничений.
- Обе операции ассоциативны и коммутативны ,
- Сумма распределительна по пересечению, то есть для любых трех ограничений равно ,
- Операция пересечения идемпотентна,
- Ограничение тождество операции пересечения,
- Ограничение тождество для операции суммы,
Кроме того, над выполнимыми ограничениями верны следующие алгебраические свойства:
- Ограничение является нулем для операции суммирования,
- Отсюда следует, что множество выполнимых ограничений представляет собой идемпотентное полукольцо с как ноль и как единство.
- Если 0 - минимальный элемент , тогда является нулем для ограничений пересечения над выполнимыми ограничениями.
При невыполнимых ограничениях обе операции имеют один и тот же ноль, который равен . Таким образом, набор ограничений даже не образует полукольца, потому что идентичность пересечения отлична от нуля суммы.
DBM
Учитывая набор переменные, , DBM - это матрица со столбцом и строками, проиндексированными и записи являются ограничениями. Интуитивно для столбца и ряд , Значение на позиции представляет . Таким образом, зона, определяемая матрицей, обозначаемый , является .
Обратите внимание, что эквивалентно , поэтому запись по сути все еще является верхней границей. Заметим, однако, что, поскольку мы рассматриваем моноид, для некоторых значений а также реальность фактически не принадлежит моноиду.
Прежде чем вводить определение канонической DBM, нам нужно определить и обсудить отношение порядка для этих матриц.
Заказ на этих матрицах
Матрица считается меньше матрицы если каждая из его записей меньше. Обратите внимание, что этот заказ не является полным. Учитывая два DBM а также , если меньше или равно , тогда .
Точная нижняя грань двух матриц а также , обозначаемый , имеет в качестве введите значение . Обратите внимание, что поскольку - операция «сумма» полукольца ограничений, операция представляет собой «сумму» двух DBM, где набор DBM рассматривается как модуль .
Аналогично случаю ограничений, рассмотренному выше в разделе «Операции с ограничениями», наибольшая нижняя граница бесконечного числа матриц определяется правильно, как только удовлетворяет свойству наибольшей нижней границы.
Определено пересечение матриц / зон. Операция объединения не определена, и действительно, объединение зоны не является зоной в целом.
Для произвольного набора матриц, которые все определяют одну и ту же зону , также определяет . Отсюда следует, что до тех пор, покаимеет свойство наибольшей-нижней границы, каждая зона, которая определяется по крайней мере матрицей, имеет уникальную минимальную матрицу, определяющую ее. Эта матрица называется канонической DBM.
Первое определение канонической DBM
Мы переформулируем определение канонической разностной матрицы границ . Это DBM, в которой никакая меньшая матрица не определяет один и тот же набор. Ниже объясняется, как проверить, является ли матрица DBM, и как в противном случае вычислить DBM из произвольной матрицы, чтобы обе матрицы представляли один и тот же набор. Но сначала приведем несколько примеров.
Примеры матриц
Сначала рассмотрим случай, когда есть одиночные часы .
Настоящая линия
Сначала дадим каноническую DBM для . Затем мы представляем еще одну DBM, которая кодирует набор. Это позволяет находить ограничения, которым должна удовлетворять любая DBM.
Каноническая DBM множества вещественных . Он представляет собой ограничения, , а также . Все эти ограничения выполняются независимо от значения, присвоенного. В оставшейся части обсуждения мы не будем подробно описывать ограничения, связанные с записями вида, поскольку эти ограничения систематически соблюдаются.
DBM также кодирует набор реальных. Он содержит ограничения а также которые выполняются независимо от значения . Это показывает, что в канонической DBM, диагональный вход никогда не превышает , поскольку матрица, полученная из путем замены диагонального входа на определяет тот же набор и меньше, чем .
Пустой набор
Теперь мы рассмотрим множество матриц, каждая из которых кодирует пустое множество. Сначала дадим канонический DBM для пустого множества. Затем мы объясняем, почему каждый из DBM кодирует пустой набор. Это позволяет находить ограничения, которым должна удовлетворять любая DBM.
Каноническая DBM пустого множества по одной переменной равна . Действительно, он представляет собой множество, удовлетворяющее ограничению, , а также . Эти ограничения невыполнимы.
DBM также кодирует пустой набор. Действительно, он содержит ограничениечто неудовлетворительно. В более общем плане это показывает, что запись не может быть если все записи не .
DBM также кодирует пустой набор. Действительно, он содержит ограничениечто неудовлетворительно. В более общем плане это показывает, что запись в диагональной линии не может быть меньше, чем если это не .
DBM также кодирует пустой набор. Действительно, он содержит ограничения а также которые противоречивы. В более общем плане это показывает, что для каждого, если , тогда а также оба равны ≤.
DBM также кодирует пустой набор. Действительно, он содержит ограничения а также которые противоречивы. В более общем плане это показывает, что для каждого, , пока не является .
Строгие ограничения
Примеры, приведенные в этом разделе, аналогичны примерам, приведенным в разделе «Примеры» выше. На этот раз они представлены как DBM.
DBM представляет набор, удовлетворяющий ограничениям а также . Как упоминалось в разделе «Примеры», оба этих ограничения подразумевают, что. Это означает, что DBMкодирует ту же зону. Собственно, это DBM этой зоны. Это показывает, что в любой DBM, для каждого , ограничение меньше, чем ограничение .
Как объяснялось в разделе «Пример», константа 0 может рассматриваться как любая переменная, что приводит к более общему правилу: в любой DBM , для каждого , ограничение меньше, чем ограничение .
Три определения канонической DBM
Как объяснялось во введении к разделу « Матрица границ разницы» , канонический DBM - это DBM, строки и столбцы которого индексируются, записи которого являются ограничениями. Кроме того, он обладает одним из следующих эквивалентных свойств.
- не существует DBM меньшего размера, определяющего ту же зону,
- для каждого , ограничение меньше, чем ограничение
- учитывая ориентированный граф с краями и стрелы помеченный , кратчайший путь от любого края к любому краю это стрела . Этот граф называется потенциальным графом DBM.
Последнее определение можно напрямую использовать для вычисления канонического DBM, связанного с DBM. Достаточно применить алгоритм Флойда – Уоршалла к графу и сопоставить каждую запись кратчайший путь от к в графике. Если этот алгоритм обнаруживает цикл отрицательной длины, это означает, что ограничения невыполнимы, и, следовательно, зона пуста.
Операции по зонам
Как было сказано во введении, основной интерес DBM заключается в том, что они позволяют легко и эффективно выполнять операции с зонами.
Напомним сначала операции, которые были рассмотрены выше:
- тестирование на включение зоны в зоне выполняется путем проверки того, что каноническая DBM меньше или равен каноническому BDM ,
- DBM для пересечения набора зон - это наибольшая нижняя граница DBM этих зон,
- проверка на пустоту зоны заключается в проверке того, состоит ли каноническая DBM зоны только из ,
- проверка того, является ли зона всем пространством, заключается в проверке того, состоит ли DBM зоны только из .
Теперь опишем операции, которые не рассматривались выше. Первые описанные ниже операции имеют четкий геометрический смысл. Последние становятся более естественными для часовых оценок.
Сумма зон
Сумма Минковского двух зон, определенных двумя DBM а также , определяется DBM чей запись . Обратите внимание, что поскольку - операция «произведение» полукольца ограничений, операция над DBM на самом деле не является работой модуля DBM.
В частности, следует, что для перевода зоны по направлению , достаточно добавить DBM в DBM .
Проекция компонента на фиксированное значение
Позволять константа.
Учитывая вектор , а индекс , проекция -й компонент к это вектор . На языке часов для, это соответствует сбросу -ые часы.
Проектирование -й компонент зоны к состоит просто из множества векторов с их -й компонент к . Это реализовано в DBM путем настройки компонентов к и компоненты к
Будущее и прошлое зоны
Будем называть будущее зонойи мимо зоны. Учитывая точку, будущее определяется как , и прошлое определяется как .
Имена «будущее» и «прошлое» происходят от понятия часов . Если набор часам присваиваются значения , и т. д., то в их будущем набор заданий, которые у них будут, - это будущее .
Учитывая зону , будущееявляются объединением будущего каждой точки зоны. Определение прошлого зоны аналогично. Таким образом, будущее зоны можно определить как, и, следовательно, может быть легко реализован как сумма DBM. Однако есть даже более простой алгоритм, который можно применить к DBM. Достаточно изменить каждую запись к . Точно так же прошлое зоны можно вычислить, установив каждую запись к .
Смотрите также
- Регион (проверка модели) - минимальная по включению зона, удовлетворяющая некоторым свойствам
Рекомендации
- ^ http://people.cs.aau.dk/~adavid/UDBM/index.html
- ^ Дилл, Дэвид L (1990). «Временные предположения и проверка параллельных систем с конечным числом состояний». Конспект лекций по информатике . 407 : 197–212. DOI : 10.1007 / 3-540-52148-8_17 . ISBN 978-3-540-52148-8.
- Матрицы разностных привязок Лекция № 20 по расширенной проверке моделей Йуст-Питер Катоен
- Перон, Матиас; Halbwachs, Николас (2008). «Абстрактная область, расширяющая матрицы разностной связи с ограничениями неравенства» (PDF) . Конспект лекций по информатике . 4349 : 268–282. DOI : 10.1007 / 978-3-540-69738-1_20 . ISBN 978-3-540-69735-0.