В большинстве работ о редукции частичного порядка предполагается, что анализируемая система задана как набор процессов с некоторым оператором композиции. Это имеет большой смысл, поскольку вы не хотите сначала вычислять пространство состояний, а затем уменьшать его с помощью редукции частичного порядка.
Но, предполагая, что у вас уже есть плоское пространство состояний, можете ли вы уменьшить его с помощью редукции частичного порядка? Я думал, что это должно быть возможно с использованием модифицированной DFS. Некоторые свойства можно проверить локально, а условие цикла можно учесть, используя информацию о состояниях в стеке.
Есть ли документ или другая ссылка, где представлен такой алгоритм?
