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

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

При явном исследовании пространства состояний частичное понижение порядка обычно относится к особой технике расширения репрезентативного подмножества всех включенных переходов. Этот метод также был описан как проверка модели с представителями ( Пелед, 1993 ). Существуют различные версии этого метода: так называемый метод упорных множеств ( Valmari 1990 ), метод обширных множеств ( Peled 1993 ) и метод постоянных множеств ( Godefroid 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 цикл не допускается , если она содержит состояние , в котором некоторые перехода включены, но никогда не включается в обильном (с) для любого состояния s на цикле.${\ displaystyle \ alpha}$

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

Упрямые наборы [ править ]

Упрямые множества не используют явного отношения независимости. Вместо этого они определяются исключительно через коммутативность последовательностей действий. Множество (слабо) упорное в s, если выполняется следующее.${\ displaystyle T (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 также могут быть дополнительно ослаблены по сравнению с тем, что они есть в методе обильного набора, но метод упорного набора совместим с C2 и C3.

Другое [ править ]

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

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

Ссылки [ править ]

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