Я хотел бы спросить, существуют ли алгоритмы (также уже реализованные) для проверки пустоты знакопеременного автомата, в частности слабого знакопеременного автомата.
Существует реализация под названием ALASKA: http://www.antichains.be/alaska/ - вы также найдете ссылки на соответствующие теоретические статьи на этой странице.