Локальный тест на включение в задаче о достижимости для вполне структурированных систем переходов

Рассматривается процедура построения дерева достижимости для систем с бесконечным числом состояний в символьном представлении. Показано, что вариант процедуры с локальным тестом на включение является разрешающей процедурой в задаче о покрываемости для вполне структурированных систем переходов.