5ⁿ → 4n+1: сколько на самом деле дают редукции в explicit-state model checking

Проверка модели полным перебором упирается в комбинаторный взрыв, и практически вся инженерия в этой области — не про сам поиск, а про то, как его избежать. Две классические техники — редукция по симметрии и редукция частичных порядков — описаны в литературе десятилетиями, но их эффект обычно приводится либо асимптотически, либо на одном показательном примере.

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

Три результата, ради которых стоит читать дальше: Читать далее