WikiDer > Частичное сокращение заказа

В Информатика, редукция частичного порядка это метод уменьшения размера пространство состояний быть обысканным проверка модели или же Автоматизированное планирование и составление графиков алгоритм. Он использует коммутативность одновременно выполняемых переходы, которые приводят к одному и тому же состоянию при выполнении в разных порядках.

При явном исследовании пространства состояний частичное понижение порядка обычно относится к специальной технике расширения репрезентативного подмножества всех включенных переходов. Этот метод также был описан как проверка модели с представителями (Пелед 1993). Существуют различные варианты метода, так называемый упрямый набор метода (Валмари 1990), обильный метод набора (Пелед 1993) и метод постоянного набора (Годфроид 1994).

Обильные наборы

Обильные наборы - это пример проверки модели с представителями. Их формулировка опирается на отдельное понятие зависимость. Рассмотрены два перехода независимый только если каждый раз, когда они взаимно включены, они не могут отключить другой, и выполнение обоих приводит к уникальному состоянию независимо от порядка, в котором они выполняются. Переходы, которые не являются независимыми, являются зависимыми. На практике зависимость аппроксимируется с помощью статического анализа.

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

C0 ${ displaystyle {обильно (s) = varnothing} iff {enabled (s) = varnothing}}$

C1 Если переход ${ displaystyle alpha}$ зависит от некоторого переходного отношения в ${ displaystyle ample (s)}$, этот переход не может быть запущен, пока не будет выполнен какой-либо переход в большом наборе.

Условия C0 и C1 достаточны для сохранения всех тупиков в пространстве состояний. Необходимы дополнительные ограничения для сохранения более тонких свойств. Например, чтобы сохранить свойства линейной темпоральной логики, необходимы следующие два условия:

C2 Если ${ displaystyle enabled (s) neq ample (s)}$, каждый переход в обильном наборе невидим

C3 А цикл не допускается, если он содержит состояние, в котором некоторый переход ${ displaystyle alpha}$ включен, но никогда не включается в число (а) для любых состояний цикла.

Этих условий достаточно для обильного набора, но не обязательных условий (Кларк 1999) ошибка harv: цель отсутствует: CITEREFClarke1999 (помощь).

Упрямые наборы

Упрямые множества не используют явного отношения независимости. Вместо этого они определяются исключительно через коммутативность последовательностей действий. Множество ${ displaystyle T (s)}$ является (слабо) упорным в s, если выполняется следующее.

D0 ${ Displaystyle forall a in T (s) forall b_ {1}, ..., b_ {n} notin T (s)}$, если выполнение последовательности ${ displaystyle b_ {1}, ..., b_ {n}, a}$ возможно и приводит к состоянию ${ displaystyle s '}$, то выполнение последовательности ${ displaystyle a, b_ {1}, ..., b_ {n}}$ возможно и приведет к состоянию ${ displaystyle s '}$.

D1 Либо ${ displaystyle s}$ это тупик, или ${ Displaystyle существует в T (s)}$ такой, что ${ displaystyle forall b_ {1}, ..., b_ {n} notin T (s)}$, выполнение ${ displaystyle b_ {1}, ..., b_ {n}, a}$ возможно.

Этих условий достаточно для сохранения всех тупиковые ситуации, точно так же, как C0 и C1 находятся в методе обильного набора. Однако они несколько слабее и поэтому могут давать меньшие наборы. Условия C2 и C3 также могут быть дополнительно ослаблены от того, что они находятся в достаточном методе набора, но упорный метод набора совместит с С2 и С3.

Другие

Существуют и другие обозначения редукции частичного порядка. Одним из наиболее часто используемых является алгоритм постоянной установки / спящего режима. Подробную информацию можно найти в диссертации Патриса Годфруа (Годфроид 1994).

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

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

• Кларк, Эдмунд М .; Грумберг, Орна; Пелед, Дорон А. (1999). Проверка модели. MIT Press.
• Фланаган, Кормак; Годфроид, Патрис (2005). «Динамическая редукция частичного порядка для программного обеспечения для проверки моделей». Труды POPL ’05, 32-й симпозиум ACM. по принципам языков программирования. С. 110–121.
• Годфроид, Патрис (1994). Методы частичного порядка для проверки параллельных систем - подход к проблеме взрыва состояния (PostScript) (Кандидат наук). Университет Льежа, факультет компьютерных наук.
• Хольцманн, Жерар Дж. (1993). Средство проверки спиновой модели: учебник и справочное руководство. Эддисон-Уэсли. ISBN 978-0-321-22862-8.
• Пелед, Дорон А. (1993). «Все от одного, один за всех: проверка моделей с использованием представителей». Труды CAV'93, LNCS 697, Springer 1993. С. 409–423. Дои:10.1007/3-540-56922-7_34.
• Валмари, Антти (1990). «Упрямые наборы для создания сокращенного пространства состояний». Успехи в сетях Петри 1990, LNCS 483, Springer 1991. С. 491–515. Дои:10.1007/3-540-53863-1_36.