Введение
Техника, используемая в формальной верификации компьютерных систем.
В информатике частичное упорядочение (partial order reduction) — это техника уменьшения размера пространства состояний, подлежащего исследованию алгоритмом проверки моделей или автоматизированного планирования и составления расписаний. Она использует коммутативность одновременно выполняемых переходов, приводящих к одному и тому же состоянию при выполнении в разном порядке. При явном исследовании пространства состояний частичное упорядочение обычно относится к конкретной технике расширения представительного подмножества всех доступных переходов. Эта техника также описывается как проверка моделей с использованием представителей. Существуют различные варианты этого метода, такие как метод упрямых множеств и метод широких множеств.
Упорные наборы
Упорные множества не используют явного отношения независимости. Вместо этого они определяются исключительно через коммутативность над последовательностями действий. Множество является (слабо) упорным в точке s, если выполняются следующие условия. D0: если выполнение последовательности возможно и приводит к состоянию , то выполнение последовательности возможно и приведет к состоянию . D1: либо является состоянием тупика, либо существует такое , что , и выполнение возможно. Эти условия достаточны для сохранения всех состояний тупика, как и C0 и C1 в методе широких множеств. Однако они несколько слабее, и поэтому могут приводить к меньшим множествам. Условия C2 и C3 также могут быть дополнительно ослаблены по сравнению с методом широких множеств, но метод упорных множеств совместим с C2 и C3.
D1 Either is a deadlock, or such that , the execution of is possible. These conditions are sufficient for preserving all deadlocks, just like C0 and C1 are in the ample set method. They are, however, somewhat weaker, and as such may lead to smaller sets. The conditions C2 and C3 can also be further weakened from what they are in the ample set method, but the stubborn set method is compatible with C2 and C3.
Другие
Существуют и другие обозначения для частичного уменьшения порядка. Одним из наиболее часто используемых является алгоритм постоянных множеств / множеств сна. Подробную информацию можно найти в диссертации Патриса Годфроида. В символической верификации моделей частичное сокращение порядка может быть реализовано путем добавления дополнительных ограничений (усиление защитных условий). Дальнейшие применения частичного сокращения порядка включают автоматизированное планирование.