Семинар лаборатории теоретической информатики: Антон Гнатенко "Спецификация и верификация конечных автоматов-преобразователей"

10 октября на семинаре лаборатории теоретической информатики состоится доклад Антона Гнатенко "Спецификация и верификация конечных автоматов-преобразователей".

Конечные автоматы, задающие преобразования потоков входных сигналов в последовательности элементарных действий, являются простейшей моделью вычислений, пригодной для описания поведения реагирующих систем. Это поведение проявляется в соответствии между потоком входных сигналов и последовательностью элементарных действий, выполняемых системой. Для формальной спецификации и верификации реагирующих систем такого рода требуются более сложные и выразительные средства спецификации, нежели традиционные темпоральные логики. В докладе будет предложена расширенная темпоральная логика Reg-CTL*, в которой темпоральные операторы параметризованы регулярными выражениями. Мы рассмотрим алгоритмы верификации автоматов-преобразователей относительно формул некоторых фраментов этой логики, а также её выразительные возможности. На правах "work in progress" будет изложена идея алгоритма верифкации относительно произвольных формул Reg-CTL*.

Семинар пройдет с 18:10 до 19:30 в аудитории R207, Покровский бульвар, 11.
Заказ пропуска: dchernyshova@hse.ru