|
ИСТИНА |
Войти в систему Регистрация |
Интеллектуальная Система Тематического Исследования НАукометрических данных |
||
On the model checking of sequential reactive systemsдоклад на конференции
- Авторы: Zakharov V., Kozlova D.
- Международная Конференция (Семинар (workshop)) : 25th International Workshop on Concurrency, Specification and Programming (CS&P 2016)
- Даты проведения конференции: 28-30 сентября 2016
- Дата доклада: 30 сентября 2016
- Тип доклада: Устный
- Докладчик: не указан
- Место проведения: Росток, Germany
-
Аннотация доклада:
рассмотрена задача формальной верификации реагирующих систем, моделируемых конечными автоматами-преобразователями. Для спецификации их поведения предложен новый вариант темпоральной логики линейного времени LTL-FL (LTL with Formal Languages). Формальные языки (множества конечных слов фиксированных алфавитов) в формулах LTL-FL используются для представления элементарных свойств вычислений, а также для параметризации темпоральных операторов. Установлено, что задача проверки выполнимости формул регулярного фрагмента FL-LTL на конечных автоматах преобразователях разрешима.
- Доклад на конференции выполнен в рамках проекта (проектов):
- Добавил в систему: Захаров Владимир Анатольевич