5ⁿ → 4n+1: сколько на самом деле дают редукции в explicit‑state model checking
5ⁿ → 4n+1: сколько на самом деле дают редукции в explicit‑state model checking Проверка модели полным перебором упирается в комбинаторный взрыв, и практически вся инженерия здесь — не про сам поиск, а про то, как его избежать. Редукция по симметрии и редукция частичных порядков описаны в литературе десятилетиями, но их эффект обычно приводят асимптотически или на одном показательном примере. В статье — измерение на работающей реализации: во сколько раз каждая редукция сокращает пространство состояний, сколько она стоит в пересчёте на состояние, на каких спецификациях не даёт ничего, и экспериментальная проверка того, что четыре условия ample‑множества действительно необходимы. Три результата, ради которых стоит читать дальше: Читать далее. 👉 Frontender's notes