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

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

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

Широкие наборы

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

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

С0 ${ample(s)=\varnothing }\iff {enabled(s)=\varnothing }$

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

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

C2 Если $enabled(s)\neq ample(s)$, каждый переход в обширном множестве невидим.

C3 Цикл не допускается , если он содержит состояние, в котором некоторый переход $\alpha$ включен, но никогда не включается в ampl(s) для каких-либо состояний цикла.

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

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

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

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

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

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

Другие

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

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

Ссылки

• Кларк, Эдмунд М .; Грумберг, Орна ; Пелед, Дорон А. (1999). Проверка модели . МТИ Пресс.
• Фланаган, Кормак; Годфруа, Патрис (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 .