Задача выглядит вполне понятной. Есть состояние системы, точка в

, где

состояния контор,

сколько экземляров справок на руках. Есть функции

. Есть начальная точка

. Есть определенное множество финальных точек

. Вопрос: есть ли такая композиция

что образ начальной точки пересекается с

?
Можно строить такой образ в прямом порядке, можно двигаться в обратном, т.е. расширять множество

объединяя со всеми прообразами

, сделав столько итераций, пока не перестанет расти, или не включит начальную точку. Всё выглядит просто. Эффективно реализовать это дело конечно будет сложно.
ps Пока не перестанет расти в пересечении с каким-то ограничивающим множеством, конечно. Ограничивающее множество это сколько справок можно унести без тележки.