![]() |
ИСТИНА |
Войти в систему Регистрация |
ИСТИНА ЦЭМИ РАН |
||
рассмотрена задача формальной верификации реагирующих систем, моделируемых конечными автоматами-преобразователями. Для спецификации их поведения предложен новый вариант темпоральной логики линейного времени LTL-FL (LTL with Formal Languages). Формальные языки (множества конечных слов фиксированных алфавитов) в формулах LTL-FL используются для представления элементарных свойств вычислений, а также для параметризации темпоральных операторов. Установлено, что задача проверки выполнимости формул регулярного фрагмента FL-LTL на конечных автоматах преобразователях разрешима.