Project Seminar 2019 2020 — различия между версиями
Milovanov (обсуждение | вклад) |
Milovanov (обсуждение | вклад) |
||
Строка 31: | Строка 31: | ||
Конечные автоматы, задающие преобразования потоков входных сигналов в последовательности элементарных действий, являются простейшей моделью вычислений, пригодной для описания поведения реагирующих систем. Это поведение проявляется в соответствии между потоком входных сигналов и последовательностью элементарных действий, выполняемых системой. Для формальной спецификации и верификации реагирующих систем такого рода требуются более сложные и выразительные средства спецификации, нежели традиционные темпоральные логики. В докладе будет предложена расширенная темпоральная логика Reg-CTL*, в которой темпоральные операторы параметризованы регулярными выражениями. Мы рассмотрим алгоритмы верификации автоматов-преобразователей относительно формул некоторых фраментов этой логики, а также её выразительные возможности. На правах "work in progress" будет изложена идея алгоритма верифкации относительно произвольных формул Reg-CTL*. | Конечные автоматы, задающие преобразования потоков входных сигналов в последовательности элементарных действий, являются простейшей моделью вычислений, пригодной для описания поведения реагирующих систем. Это поведение проявляется в соответствии между потоком входных сигналов и последовательностью элементарных действий, выполняемых системой. Для формальной спецификации и верификации реагирующих систем такого рода требуются более сложные и выразительные средства спецификации, нежели традиционные темпоральные логики. В докладе будет предложена расширенная темпоральная логика Reg-CTL*, в которой темпоральные операторы параметризованы регулярными выражениями. Мы рассмотрим алгоритмы верификации автоматов-преобразователей относительно формул некоторых фраментов этой логики, а также её выразительные возможности. На правах "work in progress" будет изложена идея алгоритма верифкации относительно произвольных формул Reg-CTL*. | ||
+ | |||
+ | https://www.semanticscholar.org/paper/Principles-of-model-checking-Baier-Katoen/2bbf4707b8555fd001b1d3248ca0b9815ac9bd46 | ||
====Семинар 6 (17 октября). ==== | ====Семинар 6 (17 октября). ==== |
Версия 19:43, 12 июня 2020
Содержание
- 1 Расписание
- 2 Проведённые семинары
- 2.1 Семинар 1 (12 сентября).
- 2.2 Семинар 2 (19 сентября).
- 2.3 Семинар 3 (26 сентября).
- 2.4 Семинар 4 (3 октября).
- 2.5 Семинар 5 (10 октября).
- 2.6 Семинар 6 (17 октября).
- 2.7 Семинар 7 (31 октября).
- 2.8 Семинар 8 (7 ноября).
- 2.9 Семинар 9 (14 ноября).
- 2.10 Семинар 10 (5 декабря).
- 2.11 Семинар 11 (12 декабря).
- 2.12 Семинар 12 (21 января).
- 2.13 Семинар 13 (28 января).
- 2.14 Семинар 14 (11 февраля).
- 2.15 Семинар 14 (19 февраля).
- 2.16 Семинар 15 (26 февраля).
- 2.17 Семинар 16 (11 марта).
- 2.18 Семинар 17 (25 марта).
- 2.19 Семинар 18 (8 апреля).
- 2.20 Семинар 19 (15 апреля).
- 2.21 Семинар 20 (22 апреля).
- 2.22 Семинар 21 (29 апреля).
- 2.23 Семинар 21 (5 мая).
- 2.24 Семинар 22 (12 мая).
- 2.25 Семинар 23 (19 мая).
- 2.26 Семинар 23 (26 мая).
- 3 Предлагаемые статьи для рассказа на семинаре
- 4 Преподаватели
Расписание
Семинар проходить по четвергам с 18.10 по 19.30
Проведённые семинары
Семинар 1 (12 сентября).
Задача равенства нулю многочлена. Лемма Шварца-Зиппеля. https://eccc.weizmann.ac.il//report/2009/101/
Семинар 2 (19 сентября).
Применение задачи равенства нулю многочлена для решения задачи о паросочетаниях. Дерандомизация задачи о равенстве нулю многочлена для случая небольшого числа ненулевых мономов. https://eccc.weizmann.ac.il//report/2009/101/
Семинар 3 (26 сентября).
Дерандомизация задачи о равенстве нулю многочлена с помощью теорем типа Сильвестра-Галлаи. https://eccc.weizmann.ac.il//report/2009/101/
Семинар 4 (3 октября).
Доклад Антона Гнатенко https://www.semanticscholar.org/paper/Principles-of-model-checking-Baier-Katoen/2bbf4707b8555fd001b1d3248ca0b9815ac9bd46
Семинар 5 (10 октября).
Доклад Антона Гнатенко.
Анонс:
Конечные автоматы, задающие преобразования потоков входных сигналов в последовательности элементарных действий, являются простейшей моделью вычислений, пригодной для описания поведения реагирующих систем. Это поведение проявляется в соответствии между потоком входных сигналов и последовательностью элементарных действий, выполняемых системой. Для формальной спецификации и верификации реагирующих систем такого рода требуются более сложные и выразительные средства спецификации, нежели традиционные темпоральные логики. В докладе будет предложена расширенная темпоральная логика Reg-CTL*, в которой темпоральные операторы параметризованы регулярными выражениями. Мы рассмотрим алгоритмы верификации автоматов-преобразователей относительно формул некоторых фраментов этой логики, а также её выразительные возможности. На правах "work in progress" будет изложена идея алгоритма верифкации относительно произвольных формул Reg-CTL*.
Семинар 6 (17 октября).
Доклад Антона Гнатенко. https://www.labri.fr/perso/igw/Papers/igw-mu.pdf
Семинар 7 (31 октября).
Эффективное решение задачи SAT для КНФ маленькой ширины. http://www.frontiersinai.com/ecai/ecai2004/ecai04/pdf/p0161.pdf
Семинар 8 (7 ноября).
Доклад Андрея Фёдорова.
Семинар 9 (14 ноября).
Доклад Виктора.
Семинар 10 (5 декабря).
О задаче QBF для КНФ маленькой ширины http://www.frontiersinai.com/ecai/ecai2004/ecai04/pdf/p0161.pdf
Семинар 11 (12 декабря).
Доклад Анастасии Чистопольской.
Семинар 12 (21 января).
Введение в Grain-Fine complexity http://people.csail.mit.edu/mip/papers/sat-lbs/paper.pdf
Семинар 13 (28 января).
Введение в Grain-Fine complexity (продолжение) http://people.csail.mit.edu/mip/papers/sat-lbs/paper.pdf
Семинар 14 (11 февраля).
Доклад Азата https://e-maxx.ru/algo/tutte_matrix http://m.mathnet.ru/php/archive.phtml?wshow=paper&jrnid=mp&paperid=170&option_lang=rus
Семинар 14 (19 февраля).
Доклад Павла Захарова
Семинар 15 (26 февраля).
Доклад Антона Гнатенко
Семинар 16 (11 марта).
Доклад Антона Гнатенко.
Семинар 17 (25 марта).
Введение в алгоритмическую статистику. https://www.mccme.ru/free-books/shen/kolmbook.pdf
Семинар 18 (8 апреля).
Доклад Никиты Лукьяненко. https://drive.google.com/file/d/1ePSO5PWdA-qTivHu3hrYfE42SOyzIgUV/view?usp=sharing
Семинар 19 (15 апреля).
Доклад Никиты Лукьяненко. https://drive.google.com/file/d/1ePSO5PWdA-qTivHu3hrYfE42SOyzIgUV/view?usp=sharing
Семинар 20 (22 апреля).
Доклад Никиты Лукьяненко. https://cstheory.stackexchange.com/questions/44382/a-game-on-several-graphs/46571#46571
Семинар 21 (29 апреля).
Доклад Андрея Фёдорова. https://www.cs.cornell.edu/courses/cs4820/2014sp/notes/maxcoverage.pdf
Семинар 21 (5 мая).
Доклад Антона Гнатенко.
Семинар 22 (12 мая).
Доклад Антона Гнатенко.
Семинар 23 (19 мая).
Доклад Максима Голядкина.
Семинар 23 (26 мая).
Доклад Азата. https://arxiv.org/pdf/1602.08254.pdf
Предлагаемые статьи для рассказа на семинаре
1) Nitin Saxena, Progress on Polynomial Identity Testing https://eccc.weizmann.ac.il/report/2009/101/
2) Лекции Стэндфордского университета о PIT и совершенных паросочетаниях. https://cs.stanford.edu/~mpkim/notes/lec5.pdf
Преподаватели
Милованов Алексей, almas239@gmail.com