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

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

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

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

Определение

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

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

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

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

Область может быть определена как класс эквивалентности для некоторого отношения эквивалентности. Назначение двух часов ${\displaystyle \nu _{1}}$ и ${\displaystyle \nu _{2}}$ эквивалентны, если они удовлетворяют следующим ограничениям:^[2]:

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

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

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

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

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

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

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

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

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

Бисимуляция по времени

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

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

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

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

Сброс часов

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

• каждое ограничение ${\displaystyle S}$ не содержащий часов ${\displaystyle x}$,
• ограничения ${\displaystyle x=0}$ за ${\displaystyle x\in C'}$.

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

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

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

Определение

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

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

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

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

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

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

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

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

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

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

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

Региональный автомат

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

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

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

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

Региональный автомат

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

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

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

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

Рекомендации

1. Бенгтссон, Йохан; Йи, Ван Л. (2003). «Временные автоматы: семантика, алгоритмы и инструменты». Лекции о параллелизме и сетях Петри. 3098: 87–124. Дои:10.1007/978-3-540-27755-2_3.
2. Алур, Раджив; Дилл, Дэвид Л. (25 апреля 1994 г.). «Теория временных автоматов» (PDF). Теоретическая информатика. 126 (2): 183–235. Дои:10.1016/0304-3975(94)90010-8.