• A
  • A
  • A
  • АБB
  • АБB
  • АБB
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта

Статья

Using an extension of CTL* for specification and verification of sequential reactive systems

Системная информатика. 2020. Vol. 17. P. 21-32.

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