В модели проверки , поле информатики , область является выпуклым многогранником в для некоторого измерения , а точнее зона , удовлетворяющая некоторому свойству минимальности. Разделение регионов.
Набор зон зависит от набора ограничений формы , , а также , с участием а также некоторые переменные и константа. Области определены так, что если два вектора а также принадлежат к одному региону, то они удовлетворяют одним и тем же ограничениям . Более того, когда эти векторы рассматриваются как кортеж часов , оба вектора имеют одинаковый набор возможных вариантов будущего. Интуитивно это означает, что любая временная пропозициональная темпоральная логическая формула, или синхронизированный автомат, или сигнальный автомат, использующие только ограничения не может различить оба вектора.
Набор регионов позволяет создать автомат региона , который представляет собой ориентированный граф, в котором каждый узел является регионом, а каждое ребро гарантировать, что возможное будущее . Взяв произведение автомата этой области и синхронизированного автомата который принимает язык создает конечный автомат или автомат Бюхи, который принимает бессрочно . В частности, это позволяет уменьшить проблему пустоты дляк проблеме пустоты для конечного автомата или автомата Бюхи. Этот метод используется, например, в программном обеспечении UPPAAL . [1]
Определение
Позволять набор часов . Для каждого позволять . Интуитивно это число представляет собой верхнюю границу значений, до которых часыможно сравнить. Определение региона на часах использует эти числа с. Даны три эквивалентных определения.
Учитывая назначение часов , обозначает область, в которой принадлежит. Множество регионов обозначено.
Эквивалентность присвоения часов
Первое определение позволяет легко проверить, принадлежат ли два назначения к одному и тому же региону.
Область может быть определена как класс эквивалентности для некоторого отношения эквивалентности. Назначение двух часов а также эквивалентны, если они удовлетворяют следующим ограничениям: [2] :
- если только , для каждого а также целое число, а ~ является одним из следующих соотношений = , < или ≤ .
- если только , для каждого , , , являясь дробной частью реального, а ~ является одним из следующих соотношений = , < или ≤ .
Первый вид ограничений гарантирует, что а также удовлетворяет тем же ограничениям. Действительно, если а также , то только второе присвоение удовлетворяет . С другой стороны, если а также , оба присваивания удовлетворяют одному и тому же набору ограничений, поскольку ограничения используют только интегральные константы.
Второй вид ограничений гарантирует, что будущее двух назначений будет удовлетворять одним и тем же ограничениям. Например, пусть а также . Тогда ограничение в конце концов удовлетворен будущим без сброса часов, но не к будущему без сброса часов.
Явное определение региона
Хотя предыдущее определение позволяет проверить, принадлежат ли два назначения одному и тому же региону, оно не позволяет легко представить регион как структуру данных. Третье определение, приведенное ниже, позволяет дать каноническую кодировку региона.
Регион можно явно определить как зону , используя набор уравнений и неравенств, удовлетворяющих следующим ограничениям:
- для каждого , содержит либо:
- для некоторого целого числа
- для некоторого целого числа ,
- ,
- кроме того, для каждой пары часов , где содержит ограничения вида а также , тогда содержит (не) равенство вида с участием быть либо = , < или ≤ .
С каких пор а также фиксированы, последнее ограничение эквивалентно .
Это определение позволяет кодировать регион как структуру данных. Для каждых часов достаточно указать, к какому интервалу они принадлежат, и вспомнить порядок дробной части часов, принадлежащих открытому интервалу длины 1. Отсюда следует, что размер этой структуры равен с участием количество часов.
Синхронизированная бисимуляция
Дадим теперь третье определение регионов. Хотя это определение является более абстрактным, оно также является причиной того, что регионы используются при проверке модели. Интуитивно это определение гласит, что два назначения часов принадлежат одной и той же области, если различия между ними таковы, что никакой синхронизированный автомат не может их заметить. Учитывая любой пробег начиная с задания часов , для любого другого задания в том же районе есть пробег , проходя через одни и те же места, читая одни и те же буквы, с той лишь разницей, что время ожидания между двумя последовательными переходами может быть разным, и, следовательно, последовательные изменения часов будут разными.
Теперь дано формальное определение. Учитывая набор часов, два задания два задания часов а также принадлежит к одному региону, если для каждого синхронизированного автомата в котором охранники никогда не сравнивают часы на число больше, чем , учитывая любое местоположение из , между расширенными состояниями существует синхронизированная бисимуляция а также . Точнее, эта бисимуляция сохраняет буквы и местоположения, но не точное назначение часов. [1] : 7
Работа по регионам
Некоторые операции теперь определены по регионам: сброс некоторых часов и пропуск времени.
Сброс часов
Учитывая регион определяется набором (не) уравнений , и набор часов , регион, подобный в котором часы перезапущены теперь определяется. Эта область обозначается, это определяется следующими ограничениями:
- каждое ограничение не содержащий часов ,
- ограничения для .
Набор заданий, определяемый это именно набор заданий для .
Время-преемник
Учитывая регион , области, которые могут быть достигнуты без сброса часов, называются временными преемниками . Даны два эквивалентных определения.
Определение
Часовой регион является временным преемником другого часового региона если для каждого задания , существует некоторая положительная реальная такой, что .
Обратите внимание, что это не означает, что . Например, регион определяется набором ограничений имеет временного преемника определяется набором ограничений . Действительно, для каждого, достаточно взять . Однако настоящего такой, что или даже такой, что ; действительно, определяет треугольник, в то время как определяет сегмент.
Вычислимое определение
Второе определение, данное теперь, позволяет явно вычислить набор временного преемника региона, заданный его набором ограничений.
Учитывая регион определяется как набор ограничений , определим его набор времен-преемников. Для этого требуются следующие переменные. Позволять набор ограничений формы . Позволять набор часов такой, что содержит ограничение . Позволять набор часов такие, что нет ограничений вида в .
Если пустой, является своим временным преемником. Если, тогда является единственным временным преемником . В противном случае существует наименьший преемник по времени не равно . Наименьший по времени преемник, если не пусто, содержит:
- ограничения
- ,
- , а также
- для каждого такой, что не принадлежит , ограничение .
Если пусто, наименьший по времени преемник определяется следующими ограничениями:
- ограничения не использовать часы ,
- ограничение , для каждого ограничения в , с участием .
Характеристики
Есть не больше регионы, где это количество часов. [2] : 203
Региональный автомат
Учитывая синхронизированный автомат , его региональный автомат является конечным автоматом или автоматом Бюхи, который принимает безвременные . Этот автомат похож на, где часы заменены регионом. Интуитивно региональный автомат построен как продукти графа региона. Этот граф региона определяется первым.
График региона
Область графика является укоренились ориентированный граф , который моделирует множество возможных оценок тактовой частоты во время пробега приурочено-autoamton. Это определяется следующим образом:
- его узлы - регионы,
- его корень - начальная область , определяемый набором ограничений ,
- набор ребер , для наследник .
Региональный автомат
Позволять приуроченная автомат . За каждые часы, позволять наибольшее количество такой, что существует охранник вида в . Область автомат из, обозначаемый является конечным автоматом или автоматом Бюхи, который по существу является продуктом и графа региона, определенного выше. То есть каждое состояние автомата региона представляет собой пару, содержащую местоположениеи регион. Поскольку назначение двух часов, принадлежащих одной и той же области, удовлетворяет одной и той же защите, каждая область содержит достаточно информации, чтобы решить, какие переходы могут быть выполнены.
Формально автомат региона определяется следующим образом:
- его алфавит ,
- его набор состояний ,
- его набор состояний с участием начальный регион,
- его набор принимающих состояний ,
- его переходное отношение содержит , для , так что а также является временным преемником .
Учитывая любой пробег из , последовательность обозначается , это пробег и принимает тогда и только тогда, когда принимает [2] : 207 . Следует, что. В частности, принимает синхронизированное слово тогда и только тогда, когда принимает слово. Кроме того, приемный пробег можно вычислить из принимающего прогона .
Рекомендации
- ^ a b Бенгтссон, Йохан; Йи, Ван Л. (2003). «Временные автоматы: семантика, алгоритмы и инструменты» . Лекции о параллелизме и сетях Петри . Конспект лекций по информатике. 3098 : 87–124. DOI : 10.1007 / 978-3-540-27755-2_3 . ISBN 978-3-540-22261-3.
- ^ а б в Алур, Раджив; Дилл, Дэвид Л. (25 апреля 1994 г.). «Теория временных автоматов» (PDF) . Теоретическая информатика . 126 (2): 183–235. DOI : 10.1016 / 0304-3975 (94) 90010-8 .