Последовательные реагирующие системы, такие как контроллеры, системные драйверы, компьютерные интерпретаторы, работают с двумя потоками данных и преобразуют входные потоки данных (управляющие сигналы, инструкции) в выходные потоки управляющих сигналов (инструкции, данные). Конечные преобразователи широко используются в качестве подходящей формальной модели для подобных систем обработки информации. Поскольку вычисления преобразователей протекают во времени, темпоральная логика, очевидно, может использоваться как простой и выразительный формализм для определения поведения последовательных реагирующих систем. Однако обычные прикладные темпоральные логики (LTL, CTL) плохо подходят для этой цели, поскольку их формулы интерпретируются на омега-языках, тогда как поведение преобразователей представлено бинарными отношениями на бесконечных последовательностях, то есть омега-трансдукциях. Чтобы обеспечить темпоральную логику возможностью учитывать эту общую особенность поведения реагирующих систем, мы ввели новые расширения этой логики. Это расширение характеризуют две отличительные особенности: 1) временные операторы параметризуются наборами потоков (языков), допустимых для ввода, и 2) наборы (языки) ожидаемых выходных потоков используются в качестве базовых предикатов. В предыдущей серии работ мы изучали выразительные возможности и задачу верификации моделей для Reg-LTL и Reg-CTL, которые являются такими расширениями LTL и CTL, где упомянутые выше языки являются регулярными. Мы обнаружили, что такое расширение темпоральной логики увеличивает их выразительную способность, хотя сохраняет разрешимость задачи верификации моделей. Нашим следующим шагом в систематическом изучении выразительных и алгоритмических свойств новых расширений темпоральной логики является анализ проблемы верификации моделей для конечных автоматов-преобразователей относительно формул логики Reg-CTL*. В этой статье мы описываем алгоритм верификации моделей автоматов-преобразователей для форму логики Reg-CTL* и показываем, что эта задача принадлежит классу сложности ExpSpace.