Регион (проверка модели)

В проверке моделей , области информатики , область представляет собой выпуклый многогранник в $\mathbb {R} ^{d}$ для какого-то измерения $d$, а точнее, зону , удовлетворяющую некоторому свойству минимальности. Раздел регионов $\mathbb {R} ^{d}$.

Набор зон зависит от набора $K$ ограничений вида $x\leq c$, $x\geq c$, $x_{1}\leq x_{2}+c$ и $x_{1}\geq x_{2}+c$, с $x_{1}$ и $x_{2}$ некоторые переменные и $c$ константа. Области определены так, что если два вектора ${\vec {x}}$ и ${\vec {x}}'$ принадлежат одному и тому же региону, то они удовлетворяют одним и тем же ограничениям $K$. Более того, когда эти векторы рассматриваются как кортеж часов , оба вектора имеют одинаковый набор возможных вариантов будущего. Интуитивно это означает, что любая временная формула пропозициональной темпоральной логики , или синхронизированный автомат , или сигнальный автомат, использующий только ограничения $K$ не может различить оба вектора.

Набор регионов позволяет создать автомат регионов , представляющий собой ориентированный граф , в котором каждый узел является регионом, а каждое ребро $r\to r'$ убедиться, что $r'$ возможное будущее $r$. Взяв произведение автомата этой области и автомата с таймером ${\mathcal {A}}$ который принимает язык $L$ создает конечный автомат или автомат Бюхи , который принимает несинхронизированное $L$. В частности, это позволяет уменьшить проблему пустоты для ${\mathcal {A}}$ к проблеме пустоты для конечного автомата или автомата Бюхи. Этот метод используется, например, в программном обеспечении UPPAAL .

Определение

Позволять $C=\{x_{1},\dots ,x_{d}\}$ набор часов . Для каждого $x\in \mathbb {N}$ позволять $c_{x}\in \mathbb {N}$. Интуитивно это число представляет собой верхнюю границу значений, до которых часы $x$ можно сравнить. Определение региона по часам $C$ использует эти цифры $c_{x}$х. Теперь даны три эквивалентных определения.

Учитывая назначение часов $\nu$, $[\nu ]$ обозначает регион, в котором $\nu$ принадлежит. Множество регионов обозначается ${\mathcal {R}}$.

Эквивалентность назначения часов

Первое определение позволяет легко проверить, принадлежат ли два назначения одному и тому же региону.

Регион можно определить как класс эквивалентности для некоторого отношения эквивалентности. Два задания на часы $\nu _{1}$ и $\nu _{2}$ эквивалентны, если они удовлетворяют следующим ограничениям:

• $\nu _{1}(x)\sim c$ если только $\nu _{2}(x)\sim c$, для каждого $x\in C$ и $0\leq c\leq c_{x}$ целое число, а ~ является одним из следующих отношений = , < или ≤ .
• $\{\nu _{1}(x)\}\sim \{\nu _{1}(y)\}$ если только $\{\nu _{2}(x)\}\sim \{\nu _{2}(y)\}$, для каждого $x,y\in C$, $\nu _{1}(x)\leq c_{x}$, $\nu _{1}(y)\leq c_{y}$, $\{r\}$ являющийся дробной частью реального $r$, а ~ является одним из следующих отношений = , < или ≤ .

Первый вид ограничений гарантирует, что $\nu _{1}$ и $\nu _{2}$ удовлетворяет тем же ограничениям. Действительно, если $\nu _{1}(x)=0.5$ и $\nu _{2}(x)=1$, то только второе присваивание удовлетворяет $x=1$. С другой стороны, если $\nu _{1}(x)=0.5$ и $\nu _{2}(x)=0.6$, оба присваивания удовлетворяют одному и тому же набору ограничений, поскольку ограничения используют только целочисленные константы.

Второй вид ограничений гарантирует, что будущие два назначения будут удовлетворять одним и тем же ограничениям. Например, пусть $\nu _{1}=\{x\mapsto 0.5,y\mapsto 0.6\}$ и $\nu _{2}=\{x\mapsto 0.5,y\mapsto 0.4\}$. Тогда ограничение $y=1\land x<1$ в конечном итоге удовлетворен будущим $\nu _{1}$ без сброса часов, но не в будущем $\nu _{2}$ без сброса часов.

Явное определение региона

Хотя предыдущее определение позволяет проверить, принадлежат ли два назначения одному и тому же региону, оно не позволяет легко представить регион как структуру данных. Третье определение, приведенное ниже, позволяет дать каноническую кодировку региона.

Регион можно явно определить как зону , используя набор $S$ уравнений и неравенств, удовлетворяющих следующим ограничениям:

• для каждого $x\in C$, $S$ содержит либо:
  • $x=c$ для некоторого целого числа $0\leq c\leq c_{x}$
  • $x\in (c,c+1)$ для некоторого целого числа $0\leq c<c_{x}$,
  • $x>c_{x}$,
• при этом для каждой пары часов $x,y\in C$, где $S$ содержит ограничения вида $x\in (c,c+1)$ и $y\in (c',c'+1)$, затем $S$ содержит (не)равенство вида $\{x\}\sim \{y\}$ с $\sim$ быть либо = , < или ≤ .

С тех пор, как $c$ и $c'$ фиксированы, последнее ограничение эквивалентно $x\sim y+c-c'$.

Это определение позволяет кодировать регион как структуру данных. Достаточно для каждых часов указать, к какому интервалу они принадлежат, и вспомнить порядок дробной части часов, принадлежащих открытому интервалу длины 1. Отсюда следует, что размер этой структуры равен $O\left(\sum \log(c_{k})+|C|\log(|C|)\right)$ с $|C|$ количество часов.

Временная бисимуляция

Дадим теперь третье определение регионов. Хотя это определение более абстрактно, оно также является причиной использования регионов при проверке модели. Интуитивно это определение гласит, что два назначения часов принадлежат одной и той же области, если различия между ними таковы, что ни один синхронизированный автомат не может их заметить. Учитывая любой пробег $r$ начиная с назначения часов $\nu$, для любого другого задания $\nu '$ в этом же регионе есть пробег $r'$, проходя через одни и те же места, читая одни и те же буквы, с той лишь разницей, что время ожидания между двумя последовательными переходами может быть разным, и, следовательно, последовательные изменения часов различны.

Теперь дано формальное определение. Учитывая набор часов $C$, два задания, два задания на часы $\nu _{1}$ и $\nu _{2}$ принадлежит одной и той же области, если для каждого таймерного автомата ${\mathcal {A}}$ в котором охранники никогда не сверяют часы $x$ до числа, большего, чем $c_{x}$, учитывая любое местоположение $\ell$ из ${\mathcal {A}}$ существует синхронизированная бисимуляция между расширенными состояниями $(\ell ,\nu _{1})$ и $(\ell ,\nu _{2})$. Точнее, эта бисимуляция сохраняет буквы и местоположения, но не точное назначение часов.

Работа по регионам

Некоторые операции теперь определены над регионами: сброс некоторых часов и пропуск времени.

Сброс часов

Учитывая регион $\alpha$ определяется набором (в) уравнений $S$и набор часов $C'\subseteq C$, регион, аналогичный $\alpha$ в котором часы $C'$ перезапускаются теперь определены. Этот регион обозначается $\alpha [C'\mapsto 0]$, он определяется следующими ограничениями:

• каждое ограничение $S$ не содержит часов $x$,
• ограничения $x=0$ для $x\in C'$.

Набор заданий, определенный $\alpha [C'\mapsto 0]$ это именно набор заданий $\nu [C'\mapsto 0]$ для $\nu \in \alpha$.

Время-преемник

Учитывая регион $\alpha$области, в которые можно попасть без перестановки часов, называются временными преемниками $\alpha$. Теперь даны два эквивалентных определения.

Определение

Регион часов $\alpha '$ является временным преемником другого региона часов $\alpha$ если для каждого задания $\nu \in \alpha$, существует некоторое положительное реальное $t_{\nu ,\alpha '}>0$ такой, что $\nu +t_{\nu ,\alpha '}\in \alpha '$.

Обратите внимание, что это не означает, что $\alpha +t_{\nu ,\alpha '}=\alpha '$. Например, регион $\alpha$ определяется набором ограничений $\{0<x<1,0<y<1,x<y\}$ имеет преемника по времени $\alpha '$ определяется набором ограничений $\{0<x<1,y=1\}$. Действительно, для каждого $\nu \in \alpha$, достаточно взять $t_{\nu ,\alpha '}=1-\nu (y)$. Однако не существует реального $t$ такой, что $\alpha +t=\alpha '$ или даже такое, что $\alpha +t\subseteq \alpha '$; действительно, $\alpha$ определяет треугольник, в то время как $\alpha '$ определяет сегмент.

Вычислимое определение

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

Учитывая регион $\alpha$ определяется как набор ограничений $S$, давайте определим его набор временных преемников. Для этого необходимы следующие переменные. Позволять $T\subseteq S$ набор ограничений $S$ формы $x_{i}=c_{i}$. Позволять $Y\subseteq C$ набор часов $y$ такой, что $S$ содержит ограничение $y>c_{y}$. Позволять $Z\subseteq C\setminus Y$ набор часов $\{z\}$ такие, что не существует ограничений вида $\{x\}<\{z\}$ в $S$.

Если $T$ пусто, $\alpha$ является своим преемником по времени. Если $Y=C$, затем $\alpha$ является единственным временным преемником $\alpha$. В противном случае существует наименьший преемник по времени $\alpha$ не равен $\alpha$. Наименьший преемник по времени, если $T$ непусто, содержит:

• ограничения $S\setminus T$
• $x_{i}>c_{i}$,
• $\{x_{i}\}=\{x_{j}\}$, и
• для каждого $y$ такой, что $y>c_{y}$ не принадлежит $S$, ограничение $x_{i}<y$.

Если $T$ пусто, наименьший временной преемник определяется следующими ограничениями:

• ограничения $S$ не пользуясь часами $Z$,
• ограничение $z=c+1$, для каждого ограничения $c<z<c+1$ в $S$, с $z\in Z$.

Характеристики

Есть максимум $|C|!2^{|C|}\prod _{x\in C}(2c_{x}+2)$ регионы, где $|C|$ это количество часов.

Регион-автомат

Учитывая временной автомат ${\mathcal {A}}$, его региональный автомат является конечным автоматом или автоматом Бюхи , который принимает несинхронизированный $L$. Этот автомат похож на ${\mathcal {A}}$, где часы заменены регионом. Интуитивно, региональный автомат представляется как продукт ${\mathcal {A}}$ и графа региона. Этот граф региона определяется первым.

Граф регионов

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

• его узлы являются регионами,
• его корень - начальная область $\alpha _{0}$, определяемый набором ограничений $\{x=0\mid x\in C\}$,
• множество ребер $(\alpha ,\alpha '[C'\mapsto 0])$, для $\alpha '$ преемник времени $\alpha$.

Регион-автомат

Позволять ${\mathcal {A}}=\langle \Sigma ,L,L_{0},C,F,E\rangle$ автомат с таймером . За каждые часы $x\in C$, позволять $c_{x}$ самое большое число $c$ такая, что существует защита вида $x\sim c$ в ${\mathcal {A}}$. Районный автомат ​ ${\mathcal {A}}$, обозначенный $R({\mathcal {A}})$ является конечным автоматом или автоматом Бюхи, который по существу является произведением ${\mathcal {A}}$ и графа региона, определенного выше. То есть каждое состояние автомата региона представляет собой пару, содержащую местоположение ${\mathcal {A}}$ и регион. Поскольку назначение двух тактовых импульсов, принадлежащих одному и тому же региону, удовлетворяет одному и тому же охраннику, каждый регион содержит достаточно информации, чтобы решить, какие переходы можно предпринять.

Формально регион-автомат определяется следующим образом:

• его алфавит $\Sigma$,
• его набор состояний $L\times {\mathcal {R}}$,
• его набор состояний $L_{0}\times \{\alpha _{0}\}$ с $\alpha _{0}$ начальный регион,
• его набор принимающих состояний равен $F\times {\mathcal {R}}$,
• его переходное отношение $\delta$ содержит $((\ell ,\alpha ),a,(\ell ',\alpha '[C'\mapsto 0]))$, для $(\ell ,a,g,C',\ell ')\in E$, такой, что $\gamma \models \alpha '$ и $\alpha '$ является временным преемником $\alpha$.

Учитывая любой пробег $r=(\ell _{0},\nu _{0}){\xrightarrow[{t_{1}}]{\sigma _{1}}}(\ell _{1},\nu _{1})\dots$ из ${\mathcal {A}}$, последовательность $(\ell _{0},[\nu _{0}]){\xrightarrow {\sigma _{1}}}(\ell _{1},[\nu _{1}])\dots$ обозначается $[r]$, это пробег $R({\mathcal {A}})$ и принимает тогда и только тогда, когда $r$ принимает . Отсюда следует, что $L(R({\mathcal {A}}))=\operatorname {Untime} (L({\mathcal {A}}))$. В частности, ${\mathcal {A}}$ принимает синхронизированное слово тогда и только тогда, когда $R({\mathcal {A}})$ принимает слово. Кроме того, приемочный пробег ${\mathcal {A}}$ может быть вычислено из принимающей серии $R({\mathcal {A}})$.