Шаблон:Current Seminars

Материал из Кафедра математической кибернетики
Перейти к: навигация, поиск

Доклады на спецсеминарах

Дискретная математика и математическая кибернетика
Дискретные функции и сложность алгоритмов
Дискретный анализ
20 октября 2017 г. О максимальной длине цепи в единичном n-мерном кубе. По статье Евдокимова А.А. Вершинин А., 618/1 гр.


Теория управляющих систем и математические модели СБИС и Некоторые вопросы теории управляющих систем
20 октября 2017 г. О динамической активности схем из функциональных элементов. Шуплецов М.С.
27 октября 2017 г. Доклад по статье "Dynamic Programming Algorithms for Large-Scale Equivalence Checking and Functional Correction". Аннотация доклада Автайкина Мария


Сложность решения дискретных задач
13 октября 2017 г. NP-полнота некоторых задач о раскраске графов без заданных порожденных подграфов: о раскраске в 4 цвета графа без порожденных цепей с 8 вершинами; о предраскраскраске в 4 цвета графа без порожденных цепей с 7 вершинами. Доклад по статье: Broesma H., Golovach P.A., Paulusma D., Song J. Updating the complexity status of coloring graphs without a fixed induced linear forest. Сакович М., 418 гр.


Теоретические проблемы программирования
19 октября 2017 г. (четверг, ауд. 614) Horn fragments of temporal logics & complex event processing.

We discuss the use of various temporal knowledge representation formalisms for ontology-mediated query answering over temporal data. In particular, we consider ontology and query languages based on the linear temporal logic LTL, the multi-dimensional Halpern-Shoham interval temporal logic HS, as well as the metric temporal logic MTL. Our main focus is on the data complexity of answering temporal ontology-mediated queries and their rewritability into standard first-order and datalog queries.

M.V. Zakharyaschev
29 сентября 2017 г. Верификация преобразований исходных кодов программ посредством проверки эквивалентности.

Доклад по статье K.C. Shashidhar, Maurice Bruynooghe, Francky Catthoor, Gerda Janssens "Verification of Source Code Transformations by Program Equivalence Checking"

Как правило, когда алгоритмы для обработки цифровых сигналов адаптируются для работы в энергоэффективных и эффективно функционирующих встроенных системах, применяется комбинация ручных и автоматических преобразований. Это порождает сложную задачу верификации. Задача верификации упрощается при конвертирования кода в DSA-форму (dynamic single assignment form). Данная статья описывает метод доказательства эквивалентности двух программ в DSA-форме, в которых индексация элементов массивов и условия завершения циклов являются (кусочно заданными) аффинными выражениями. Для таких программ может быть использовано геометрическое моделирование и сразу для наборов элементов может быть показано, что результат вычислений обеих программ представляет собой одну и ту же функцию от входных данных.

М.М. Аббас
22 сентября 2017 г. Рещение задачи минимизации для одного вида детерминированных временных автоматов.

Доклад по статье Aleksandr Tvardovskii, Nina Yevtushenko "On minimization of Timed Finite State Machines"

В этой статье показано, что для одной разновидности конечных временных автоматов с ограничениями на сроки обработки входного сигнала, задержкой выходного сигнала и тайм-аутом задача минимизации автоматов по числу состояний может быть сведена к аналогичной задаче для конечных детерминированных синхронных автоматов Мили.


Е.М. Винарский