Матрица, связанная с разностью

В проверке моделей , области информатики , матрица границ различий (DBM) — это структура данных, используемая для представления некоторых выпуклых многогранников , называемых зонами . Эту структуру можно использовать для эффективной реализации некоторых геометрических операций над зонами, таких как проверка пустоты, включения, равенства, а также вычисление пересечения и суммы двух зон. Он, например, используется в средстве проверки моделей Uppaal ; где он также распространяется как независимая библиотека.

Точнее, есть понятие канонической DBM; между каноническими DBM и зонами существует взаимно однозначное отношение, и на основе каждого DBM можно эффективно вычислить канонический эквивалент DBM. Таким образом, равенство зон можно проверить, проверив равенство канонических DBM.

Зона

Матрица границ разностей используется для представления некоторых выпуклых многогранников. Эти многогранники называются зоной . Теперь они определены. Формально зона определяется уравнениями вида $x\leq c$, $x\geq c$, $x_{1}\leq x_{2}+c$ и $x_{1}\geq x_{2}+c$, с $x_{1}$ и $x_{2}$ некоторые переменные и $c$ константа.

Зоны изначально назывались регионами . но в настоящее время это название обычно обозначает регион , особый вид зоны. Интуитивно регион можно рассматривать как минимальную непустую зону, в которой ограничены константы, используемые в ограничении.

Данный $n$ переменные, есть ровно $n(n+1)$ возможны различные неизбыточные ограничения, $n$ ограничения, которые используют одну переменную и верхнюю границу, $n$ ограничения, в которых используется одна переменная и нижняя граница, и для каждого из $n^{2}$ упорядоченные пары переменных $(x,y)$, верхняя граница $x-y$. Однако произвольный выпуклый многогранник в $\mathbb {R} ^{n}$ может потребовать сколь угодно большого числа ограничений. Даже когда $n=2$, может существовать сколь угодно большое количество неизбыточных ограничений $(x<iy+c_{i})_{i\in \mathbb {N} }$, для $c_{i}$ некоторые константы. По этой причине ДБМ не могут быть расширены от зон до выпуклых многогранников.

Пример

Как указано во введении, мы рассматриваем зону, определяемую набором утверждений вида $x_{1}\leq c$, $x_{1}\geq c$, $x_{1}\leq x_{2}+c$ и $x_{1}\geq x_{2}+c$, с $x_{1}$ и $x_{2}$ некоторые переменные и $c$ константа. Однако некоторые из этих ограничений либо противоречивы, либо избыточны. Мы сейчас приведем такие примеры.

• ограничения $x_{1}\leq 3$ и $x_{1}\geq 4$ противоречивы. Следовательно, когда найдены два таких ограничения, определенная зона пуста.

  

  Рисунок в ${\textstyle \mathbb {R} ^{2}}$ показывая ${\textstyle x_{1}\leq 3}$, ${\textstyle x_{1}\geq 4}$ которые не пересекаются

• ограничения $x_{1}\leq 3$ и $x_{1}\leq 4$ являются излишними. Второе ограничение подразумевается первым. Следовательно, когда в определении зоны обнаружены два таких ограничения, второе ограничение может быть удалено.

  

  Рисунок в ${\textstyle \mathbb {R} ^{2}}$ показывая ${\textstyle x_{1}\leq 3}$ и ${\textstyle x_{1}\leq 4}$ который содержит первую цифру

Мы также приводим пример, показывающий, как генерировать новые ограничения из существующих ограничений. Для каждой пары часов $x_{1}$ и $x_{2}$, DBM имеет ограничение вида $x_{1}\prec x_{2}+c$, где $\prec$ либо <, либо ≤. Если такое ограничение не может быть найдено, ограничение $x_{1}\prec x_{2}+\infty$ могут быть добавлены к определению зоны без потери общности. Но в некоторых случаях можно найти более точное ограничение. Сейчас будет приведен такой пример.

• ограничения $x_{1}\leq 3$, $x_{2}\geq -3$ подразумевает, что $x_{1}\leq x_{2}+6$. Таким образом, предполагая, что никакие другие ограничения, такие как $x_{1}\leq x_{2}+5$ или $x_{1}<x_{2}+6$ принадлежит определению, ограничению $x_{1}\leq x_{2}+6$ добавляется в определение зоны.

  

  Рисунок в ${\textstyle \mathbb {R} ^{2}}$ показывая ${\textstyle x_{1}\leq 3}$, ${\textstyle x_{2}\geq -3}$ и их пересечения

• ограничения $x_{2}\leq 3$, $x_{1}\leq x_{2}+3$ подразумевает, что $x_{1}\leq 6$. Таким образом, предполагая, что никакие другие ограничения, такие как $x_{1}\leq 5$ или $x_{1}<6$ принадлежит определению, ограничению $x_{1}\leq 6$ добавляется в определение зоны.

  

  Рисунок в ${\textstyle \mathbb {R} ^{2}}$ показывая ${\textstyle x_{1}\leq 3}$, ${\textstyle x_{1}\leq x_{2}+3}$ и их пересечения

• ограничения $x_{1}\leq x_{2}+3$, $x_{2}\leq x_{3}+3$ подразумевает, что $x_{1}\leq x_{3}+6$. Таким образом, предполагая, что никакие другие ограничения, такие как $x_{1}\leq x_{3}+5$ или $x_{1}<x_{3}+6$ принадлежит определению, ограничению $x_{1}\leq x_{3}+6$ добавляется в определение зоны.

На самом деле, два первых случая, приведенных выше, являются частными случаями третьих случаев. Действительно, $x_{1}\leq 3$ и $x_{2}\geq -3$ можно переписать как $x_{1}\leq 0+3$ и $0\leq x_{2}+3$ соответственно. И таким образом, ограничение $x_{1}\leq x_{2}+6$ добавленное в первом примере аналогично ограничению, добавленному в третьем примере.

Определение

Теперь исправим моноид $(M,0,+)$ которое является подмножеством реальной линии. Этот моноид традиционно представляет собой набор целых , рациональных , действительных чисел или их подмножество неотрицательных чисел.

Ограничения

Чтобы определить матрицу границ различий структуры данных , сначала необходимо задать структуру данных для кодирования атомарных ограничений. Кроме того, мы вводим алгебру для атомарных ограничений. Эта алгебра похожа на тропическое полукольцо с двумя модификациями:

• Вместо $\mathbb {R}$.
• Чтобы отличить " $<m$" и " $\leq m$", набор элементов алгебры должен содержать информацию о том, является ли порядок строгим или нет.

Определение ограничений

Набор выполнимых ограничений определяется как набор пар вида:

• $(\leq ,m)$, с $m\in M$, которое представляет ограничение формы $\leq m$,
• $(<,m)$, с $m\in M$, где $m$ не является минимальным элементом $M$, которое представляет ограничение формы $<m$,
• $(<,\infty )$, что означает отсутствие ограничений.

Набор ограничений содержит все выполнимые ограничения, а также следующее невыполнимое ограничение:

• $(<,-\infty )$.

Подмножество $\{q\in \mathbb {Q} \mid q\leq {\sqrt {2}}\}$ не может быть определен с использованием такого рода ограничений. В более общем смысле, некоторые выпуклые многогранники не могут быть определены, если упорядоченный моноид не имеет свойства наименьшей верхней границы , даже если каждое из ограничений в его определении использует не более двух переменных.

Операция над ограничениями

Чтобы сгенерировать одно ограничение из пары ограничений, примененных к одной и той же (паре) переменных, мы формализуем понятие пересечения ограничений и порядка над ограничениями. Аналогично, чтобы определить новые ограничения на основе существующих ограничений, необходимо также определить понятие суммы ограничений.

Порядок ограничений

Теперь мы определим отношение порядка над ограничениями. Этот порядок символизирует отношение включения.

Во-первых, набор $\{<,\leq \}$ рассматривается как упорядоченный набор, где < уступает ≤. Интуитивно этот порядок выбран потому, что набор, определенный формулой $x<c$ строго входит в набор, определяемый $x\leq c$. Затем мы утверждаем, что ограничение $(\prec _{1},m_{1})$ меньше, чем $(\prec _{2},m_{2})$ если либо $m_{1}<m_{2}$ или ( $m_{1}=m_{2}$ и $\prec _{1}$ меньше, чем $\prec _{2}$). То есть порядок ограничений — это лексикографический порядок, применяемый справа налево. Обратите внимание, что этот заказ является общим заказом . Если $M$ имеет свойство наименьшей верхней границы (или свойство наибольшей нижней границы ), то оно также имеется в наборе ограничений.

Пересечение ограничений

Пересечение двух ограничений, обозначаемых как $(\prec _{1},m_{1})\sqcap (\prec _{2},m_{2})$, тогда просто определяется как минимум из этих двух ограничений. Если $M$ имеет свойство наибольшей нижней границы, то также определено пересечение бесконечного числа ограничений.

Сумма ограничений

Даны две переменные $x_{1}$ и $x_{2}$ к которому применяются ограничения $(\prec _{1},m_{1})$ и $(\prec _{2},m_{2})$, теперь мы объясним, как сгенерировать ограничение, удовлетворяющее $x_{1}+x_{2}$. Это ограничение называется суммой двух вышеупомянутых ограничений и обозначается как $(\prec _{1},m_{1})+(\prec _{2},m_{2})$ и определяется как $(\min(\prec _{1},\prec _{2}),m_{1}+m_{2})$.

Ограничения как алгебра

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

• Обе операции ассоциативны и коммутативны ,
• Сумма является дистрибутивной по пересечению, то есть для любых трех ограничений $((\prec _{1},m_{1})\sqcap (\prec _{2},m_{2}))+(\prec _{3},m_{3})$ равно $((\prec _{1},m_{1})+(\prec _{3},m_{3}))\sqcap ((\prec _{2},m_{2})+(\prec _{3},m_{3}))$,
• Операция пересечения идемпотентна,
• Ограничение $(<,\infty )$ является идентификатором операции пересечения,
• Ограничение $(\leq ,0)$ является тождеством операции суммирования,

Кроме того, над выполнимыми ограничениями справедливы следующие алгебраические свойства:

• Ограничение $(<,\infty )$ является нулем для операции суммирования,
• Отсюда следует, что множество выполнимых ограничений представляет собой идемпотентное полукольцо с $(<,\infty )$ как ноль и $(\leq ,0)$ как единство.
• Если 0 является минимальным элементом $M$, затем $(\leq ,0)$ является нулем для ограничений пересечения выполнимых ограничений.

При невыполнимых ограничениях обе операции имеют один и тот же нуль, что $(<,-\infty )$. Таким образом, набор ограничений даже не образует полукольца, поскольку единица пересечения отлична от нуля суммы.

СУБД

Учитывая набор $n$ переменные, $x_{1},\dots ,x_{n}$, DBM представляет собой матрицу со столбцом и строками, индексированными $0,x_{1},\dots ,x_{n}$ и записи являются ограничениями. Интуитивно, для столбца $C$ и ряд $R$, значение $m$ на позиции $(C,R)$ представляет $C\prec R+m$. Таким образом, зона, определяемая матрицей $D((\prec _{C,R},m_{C,R}))_{C,R\in \{0,x_{1},\dots ,x_{n}}\}$, обозначенный ${\mathcal {R}}(D)$, является $\{(x_{1},\dots ,x_{n})\in \mathbb {R} \mid \bigwedge _{C,R\in \{0,x_{1},\dots ,x_{n}\}}C\prec _{C,R}R+m_{C,R}\}$.

Обратите внимание, что $C\prec R+m$ эквивалентно $C-R\prec m$, таким образом, запись $(\prec ,m)$ по сути, по-прежнему является верхней границей. Однако заметим, что, поскольку мы рассматриваем моноид $M$, для некоторых значений $C$ и $R$ настоящий $C-R$ фактически не принадлежит моноиду.

Прежде чем ввести определение канонической DBM, нам необходимо определить и обсудить отношение порядка к этим матрицам.

Закажите эти матрицы

Матрица $D$ считается меньшим, чем матрица $D'$ если каждая из его записей меньше. Обратите внимание, что этот заказ не является полным. Учитывая два DBM $D$ и $D'$, если $D$ меньше или равно $D'$, затем ${\mathcal {R}}(D)\subseteq {\mathcal {R}}(D')$.

Наибольшая нижняя граница двух матриц $D$ и $D'$, обозначенный $D\sqcap D'$, имеет в качестве $(a,b)$ введите значение $(\prec _{a,b},m_{a,b})\sqcap (\prec '_{a,b},m'_{a,b})$. Обратите внимание, что поскольку $\sqcap$ – операция «суммы» полукольца ограничений, операция $\sqcap$ представляет собой «сумму» двух DBM, где набор DBM рассматривается как модуль .

Аналогично случаю ограничений, рассмотренному выше в разделе «Действие с ограничениями», наибольшая нижняя граница бесконечного числа матриц правильно определена, как только $M$ удовлетворяет свойству наибольшей нижней границы.

Определяется пересечение матриц/зон. Операция объединения не определена, и действительно, объединение зоны не является зоной вообще.

Для произвольного набора ${\mathcal {D}}$ матриц, которые все определяют одну и ту же зону $Z$, $\sqcap _{D\in {\mathcal {D}}}D$ также определяет $Z$. Отсюда следует, что, пока $M$ имеет свойство наибольшей нижней границы: каждая зона, определяемая хотя бы матрицей, имеет уникальную определяющую ее минимальную матрицу. Эта матрица называется канонической DBM $Z$.

Первое определение канонической DBM

Мы переформулируем определение канонической разностной связанной матрицы . Это DBM, в котором никакая меньшая матрица не определяет тот же набор. Ниже объясняется, как проверить, является ли матрица DBM, и как вычислить DBM из произвольной матрицы, чтобы обе матрицы представляли один и тот же набор. Но сначала приведем несколько примеров.

Примеры матриц

Сначала рассмотрим случай, когда имеются одни часы. $x_{1}$.

Настоящая линия

Сначала мы даем каноническую DBM для $\mathbb {R}$. Затем мы вводим еще одну DBM, которая кодирует набор $\mathbb {R}$. Это позволяет найти ограничения, которым должна удовлетворять любая DBM.

Каноническая DBM множества вещественных есть $\left({\begin{array}{ll}(\leq ,0)&(<,\infty )\\(<,\infty )&(\leq ,0)\end{array}}\right)$. Он представляет собой ограничения $0\leq 0+0$, $x_{1}\leq 0+\infty$, $0\leq x_{1}+\infty$ и $0\leq 0+0$. Все эти ограничения выполняются независимо от значения, присвоенного $x_{1}$. В оставшейся части обсуждения мы не будем явно описывать ограничения, обусловленные записями вида $(<,\infty )$, поскольку эти ограничения систематически выполняются.

ДБМ $\left({\begin{array}{ll}(<,\infty )&(<,\infty )\\(<,\infty )&(<,\infty )\end{array}}\right)$ также кодирует множество вещественных чисел. Он содержит ограничения $0<0+\infty$ и $x_{1}<x_{1}+\infty$ которые удовлетворяются независимо от значения $x_{1}$. Это показывает, что в канонической DBM $D$, диагональный вход никогда не превышает $(\leq ,0)$, поскольку матрица, полученная из $D$ заменив диагональную запись на $(\leq ,0)$ определяет тот же набор и меньше, чем $D$.

Пустой набор

Теперь мы рассмотрим множество матриц, каждая из которых кодирует пустой набор. Сначала мы даем каноническую DBM для пустого множества. Затем мы объясним, почему каждый из DBM кодирует пустой набор. Это позволяет найти ограничения, которым должна удовлетворять любая DBM.

Каноническая DBM пустого множества по одной переменной есть $\left({\begin{array}{ll}(<,-\infty )&(<,-\infty )\\(<,-\infty )&(<,-\infty )\end{array}}\right)$. Действительно, оно представляет собой множество, удовлетворяющее ограничению $0<0-\infty$, $0<x_{1}-\infty$, $x_{1}<0-\infty$ и $x_{1}<x_{1}-\infty$. Эти ограничения невыполнимы.

ДБМ $\left({\begin{array}{ll}(<,\infty )&(<,-\infty )\\(<,\infty )&(<,\infty )\end{array}}\right)$ также кодирует пустой набор. Действительно, оно содержит ограничение $x_{1}<0-\infty$ что неудовлетворительно. В более общем плане это показывает, что ни одна запись не может быть $(<,-\infty )$ если все записи не $(<,-\infty )$.

ДБМ $\left({\begin{array}{ll}(<,\infty )&(<,\infty )\\(<,\infty )&(<,-1)\end{array}}\right)$ также кодирует пустой набор. Действительно, оно содержит ограничение $x_{1}<x_{1}-1$ что неудовлетворительно. В более общем плане это показывает, что запись в диагональной линии не может быть меньше, чем $(\leq ,0)$ если это не $(<,-\infty )$.

ДБМ $\left({\begin{array}{ll}(<,\infty )&(<,1)\\(\leq ,-1)&(<,\infty )\end{array}}\right)$ также кодирует пустой набор. Действительно, он содержит ограничения $0<x_{1}+1$ и $x_{1}\leq -1$ которые противоречивы. В более общем плане это показывает, что для каждого $C,R\in \{0,x_{1},\dots ,x_{n}\}$, если $m_{C,R}=-m_{R,C}$, затем $\prec _{R,C}$ и $\prec _{C,R}$ оба равны ≤.

ДБМ $\left({\begin{array}{ll}(<,\infty )&(\leq ,1)\\(\leq ,-2)&(<,\infty )\end{array}}\right)$ также кодирует пустой набор. Действительно, он содержит ограничения $0\leq x_{1}+1$ и $x_{1}\leq -2$ которые противоречивы. В более общем плане это показывает, что для каждого $C,R\in \{0,x_{1},\dots ,x_{n}\}$, $-m_{C,R}\leq m_{R,C}$, пока не $m_{C,R}$ является $-\infty$.

Строгие ограничения

Примеры, приведенные в этом разделе, аналогичны примерам, приведенным в разделе «Примеры» выше. На этот раз они указаны как DBM.

ДБМ $\left({\begin{array}{lll}(\leq ,0)&(<,\infty )&(<,\infty )\\(<,\infty )&(\leq ,0)&(\leq ,3)\\(\leq ,3)&(<,\infty )&(\leq ,0)\end{array}}\right)$ представляет набор, удовлетворяющий ограничениям $x_{2}\leq 3$ и $x_{1}\leq x_{2}+3$. Как упоминалось в разделе «Примеры», оба этих ограничения подразумевают, что $x_{1}\leq 6$. Это означает, что ДБМ $\left({\begin{array}{lll}(\leq ,0)&(\leq ,6)&(<,\infty )\\(<,\infty )&(\leq ,0)&(\leq ,3)\\(\leq ,3)&(<,\infty )&(\leq ,0)\end{array}}\right)$ кодирует одну и ту же зону. Собственно, это ДБМ этой зоны. Это показывает, что в любой DBM $((\prec _{C,R},m_{C,R}))_{c,r\in \{0,x_{1},\dots ,x_{n}\}}$, для каждого $1\leq i,j\leq n$, ограничение $(\prec _{x_{i},0},m_{x_{i},0})$ меньше ограничения $(\prec _{x_{j},0},m_{x_{j},0})+(\prec _{x_{i},x_{j}},m_{x_{i},x_{j}})$.

Как поясняется в разделе «Примеры», константу 0 можно рассматривать как любую переменную, что приводит к более общему правилу: в любой DBM $((\prec _{C,R},m_{C,R}))_{c,r\in \{0,x_{1},\dots ,x_{n}\}}$, для каждого $a,b,c\in \{0,x_{1},\dots ,x_{n}\}$, ограничение $(\prec _{a,b},m_{a,b})$ меньше ограничения $(\prec _{c,b},m_{c,b})+(\prec _{a,c},m_{a,c})$.

Три определения канонического DBM

Как объяснялось во введении к разделу «Матрица границ различий» , каноническая DBM — это DBM, строки и столбцы которой индексируются $(0,x_{1},\dots ,x_{n})$, чьи записи являются ограничениями. Кроме того, оно следует одному из следующих эквивалентных свойств.

• нет меньших DBM, определяющих одну и ту же зону,
• для каждого $a,b,c\in \{0,x_{1},\dots ,x_{n}\}$, ограничение $(\prec _{a,b},m_{a,b})$ меньше ограничения $(\prec _{c,b},m_{c,b})+(\prec _{a,c},m_{a,c})$
• учитывая ориентированный граф $G$ с краями $\{0,x_{1},\dots ,x_{n}\}$ и стрелки $(a,b)$ помечены $(\prec _{a,b},m_{a,b})$, кратчайший путь от любого ребра $a$ до любого края $b$ это стрелка $(a,b)$. Этот граф называется потенциальным графом ДБМ.

Последнее определение можно напрямую использовать для вычисления канонического DBM, связанного с DBM. Достаточно применить алгоритм Флойда – Уоршалла и сопоставить его с каждой записью. к графу $(a,b)$ кратчайший путь из $a$ к $b$ в графике. Если этот алгоритм обнаруживает цикл отрицательной длины, это означает, что ограничения невыполнимы и, следовательно, зона пуста.

Операции над зонами

Как говорилось во введении, основной интерес DBM заключается в том, что они позволяют легко и эффективно выполнять операции над зонами.

Сначала напомним операции, рассмотренные выше:

• тестирование на включение зоны $Z_{1}$ в зоне $Z_{2}$ делается путем проверки того, является ли каноническая DBM $Z_{1}$ меньше или равно DBM $Z_{2}$,
• DBM для пересечения набора зон представляет собой максимальную нижнюю границу DBM этих зон,
• проверка на пустоту зоны заключается в проверке того, состоит ли каноническая ДБМ зоны только из $(<,-\infty )$,
• проверка того, является ли зона всем пространством, заключается в проверке того, состоит ли ДБМ зоны только из $(<,\infty )$.

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

Сумма зон

двух Сумма Минковского зон, определяемая двумя DBM. $D$ и $D'$, определяется DBM $D+D'$ чей $(a,b)$ запись $D_{a,b}+D'_{a,b}$. Обратите внимание, что поскольку $+$ – операция «произведения» полукольца ограничений, операция $+$ над DBM на самом деле не является операцией модуля DBM .

В частности, отсюда следует, что для перевода зоны $Z$ по направлению $v$, достаточно добавить DBM $\{v\}$ в DBM $Z$.

Проекция компонента на фиксированное значение

Позволять $d\in M$ константа.

Учитывая вектор ${\vec {x}}=(x_{1},\dots ,x_{n})$и индекс $1\leq i\leq n$, проекция $i$-й компонент ${\vec {x}}$ к $d$ вектор $(x_{1},\dots ,x_{i-1},d,x_{i+1},\dots ,x_{n})$. На языке часов, для $d=0$, это соответствует сбросу $i$-ые часы.

Проектирование $i$-я компонента зоны $Z$ к $d$ состоит просто из набора векторов $Z$ со своими $i$-й компонент $d$. Это реализовано в DBM путем установки компонентов $(x_{i},a)$ к $(\leq ,d)+D(0,a)$ и компоненты $(a,x_{i})$ к $(\leq ,-d)+D(0,a)$

Будущее и прошлое зоны

Назовем будущее зоной $F=\{(t,\dots ,t)\mid t\in \mathbb {R} _{\geq 0}\}$ и прошлая зона $P=\{(-t,\dots ,-t)\mid t\in \mathbb {R} _{\geq 0}\}$. Учитывая точку ${\vec {x}}=(x_{1},\dots ,x_{n})\in \mathbb {R} ^{n}$, будущее ${\vec {x}}$ определяется как $\{(x_{1}+t,\dots ,x_{n}+t)\mid t\in \mathbb {R} _{\geq 0}\}=F+\{{\vec {x}}\}$и прошлое ${\vec {x}}$ определяется как $P+\{{\vec {x}}\}$.

Названия будущее и прошлое происходят от понятия часов . Если набор из $n$ часы присваиваются значениям $x_{1}$, $x_{2}$и т. д., тогда в их будущем набор заданий, которые они получат, будет будущим ${\vec {x}}$.

Учитывая зону $Z$, будущее $Z$ являются объединением будущего каждой точки зоны. Определение прошлого зоны аналогично. Таким образом, будущее зоны можно определить как $F+Z$и, следовательно, может быть легко реализован как сумма DBM. Однако существует еще более простой алгоритм, применимый к DBM. Достаточно изменить каждую запись $(x_{i},0)$ к $(<,\infty )$. Аналогично, прошлое зоны можно вычислить, установив все записи $(0,x_{i})$ к $(<,\infty )$.

См. также

• Регион (проверка модели) – минимальная при включении зона, удовлетворяющая некоторым свойствам.

Ссылки

• Матрицы, связанные с разностями. Лекция № 20 «Продвинутая проверка моделей» Йост-Питер Катоен
• Перон, Матиас; Хальбвакс, Николас (2008). «Абстрактная область, расширяющая матрицы, связанные с разностью, с ограничениями неравенства» (PDF) . Верификация, проверка модели и абстрактная интерпретация . Конспекты лекций по информатике. Том. 4349. стр. 268–282. дои : 10.1007/978-3-540-69738-1_20 . ISBN  978-3-540-69735-0 .