Применение методов решения задачи удовлетворения ограничениям для построения управляющих конечных автоматов по сценариям работы Владимир Ульянцев Научный. - презентация

1 Применение методов решения задачи удовлетворения ограничениям для построения управляющих конечных автоматов по сценариям работы Владимир Ульянцев Научный руководитель: Федор Царев I всероссийский конгресс молодых ученых НИУ ИТМО 11 апреля 2012

2 2 Управляющие автоматы и сценарии работы программы Управляющий автомат: – входные события – входные переменные – выходные воздействия Сценарий работы – последовательность троек – e – входное событие – f – охранное условие – Булева формула, зависящая от входных переменных – A – последовательность выходных воздействий Приведенный управляющий автомат: – Удовлетворяет – Не удовлетворяет 2

3 3 Пример управляющего автомата Часы с будильником Четыре события – H – кнопка H нажата – M – кнопка M нажата – A – кнопка A нажата – T – происходит каждый момент времени Две входные переменные Семь выходных воздействий

4 Требования, предъявляемые к автоматной программе Непротиворечивость – не должно быть двух переходов, исходящих из одного состояния автомата и одновременно выполнимых при некоторой комбинации события и входных переменных Полнота – любой комбинации события и входных переменных должен соответствовать переход в каждом состоянии 4

5 5 Постановка задачи Рассматриваются автоматные программы с единственным объектом управления Входные данные: – Набор сценариев работы программы (Sc) – Число состояний управляющего автомата (C) Необходимо найти управляющий автомат, состоящий из C состояний и удовлетворяющий всем сценариям работы

6 Предлагаемый метод Ulyantsev V., Tsarev F. Extended Finite-State Machine Induction using SAT-Solver / Proceedings of the Tenth International Conference on Machine Learning and Applications, ICMLA 2011, Honolulu, HI, USA, December IEEE Computer Society, Vol. 2. P. 346–349 – Не гарантируется полнота Выразить требование полноты в виде ограничений на целочисленные переменные (constraint satisfaction problem, CSP) 6

7 7 Основная идея Каждому сценарию работы соответствует «линейный» автомат «Раскраска» сценариев – Каждому «состоянию» каждого сценария работы необходимо поставить в соответствие состояние искомого управляющего автомата – Состояния управляющего автомата будем различать цветами 77

8 8 Этапы работы алгоритма 8 Построение дерева сценариев Построение графа совместимости Построение булевой КНФ-формулы – Набор ограничений на целочисленные переменные Запуск сторонней программы, находящей решение Построение искомого управляющего автомата

9 9 Предварительные вычисления Для каждой пары охранных условий, встречающихся в заданных сценариях: – Равны ли как булевы формулы – Имеют ли общую выполняющую подстановку Асимптотическая оценка: – O(n 2 2 2m ) где n – общий размер сценариев, m – наибольшее число переменных, встречающихся в охранном условии (на практике m не превышает пяти)

10 10 1. Построение дерева сценариев Аналогично построению бора Алгоритм прерывается, если найдено противоречие 10

11 11 2. Построение графа совместимости Вершины совпадают с вершинами дерева Вершины соединены ребром, если существует последовательность, различающая их Для каждой вершины, начиная с листьев, строится множество несовместимых с ней вершин Используется динамическое программирование 11

12 12 3. Используемые переменные Целочисленные переменные: – x v – цвет, в который покрашена вершина v (1x vC) – y i,e,f – номер состояния, в которое ведет переход из состояния i, помеченный событием e и охранным условием f (1y i,e,fC) 12

13 13 3. Построение ограничений для требования непротиворечивости Типы ограничений: – x v x u – цвета несовместимых вершин должны быть различны – (x v = i) (y i,e,f = x u ) – цвета вершин дерева не должны противоречить переходам автомата 13

14 3. Построение ограничений для требования полноты При условии непротиворечивости можно выразить условие полноты Сумма выполняющих подстановок S равна 2 m, где m – число переменных, используемых в переходах данного состояния и события 14

15 15 4. Использование программного средства, решающего задачу удовлетворения ограничениям Использовался пакет choco для нахождения выполняющей подстановки Пакет для языка Java, предназначенный, в том числе, для нахождения оптимальных расписаний 15

16 16 5. Построение управляющего автомата по выполняющей подстановке (1) Раскраска дерева сценариев Цвет вершины соответствует значениям x v 16

17 17 5. Построение управляющего автомата по выполняющей подстановке (2) Вершины одинаковых цветов сливаются 17

18 18 Экспериментальные исследования Управляющий автомат для часов с будильником : – 38 сценариев работы суммарной длины один сценарий Наборы случайных сценариев работы : – Генерируется случайный полный по переменным автомат – Сценарии – случайные пути в автомате – Найдены наборы сценариев, на которых проявляется преимущество разработанного метода 18

19 19 Результаты Разработан и реализован метод построения управляющих автоматов, основанный на сведении задачи к задаче удовлетворения ограничениям Экспериментальные исследования продемонстрировали существование задач, для которых метод находит качественно лучшее решение 19

20 Спасибо за внимание! 20