Частичное уменьшение порядка

Метод, используемый при формальной проверке компьютерных систем

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

В явном исследовании пространства состояний частичная редукция порядка обычно относится к конкретной технике расширения представительного подмножества всех разрешенных переходов. Эта техника также описывается как проверка модели с представителями. ^[1] Существуют различные версии метода, так называемый метод упрямого множества, ^[2] метод обильного множества, ^[1] и метод постоянного множества. ^[3]

Обширные наборы

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

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

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

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

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

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

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

Эти условия достаточны для обширного набора, но не являются необходимыми условиями. ^[4]

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

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

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

Другие

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

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

Цитаты

1. (Пелед 1993)
2. (Вальмари 1990)
3. (Годфруа 1994)
4. (Кларк, Грумберг и Пелед 1999)

Ссылки

• Кларк, Эдмунд М.; Грумберг , Орна ; Пелед, Дорон А. (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). «Упрямые множества для генерации сокращенного пространства состояний». Advances in Petri Nets 1990, LNCS 483, Springer 1991. стр. 491–515. doi :10.1007/3-540-53863-1_36.