ПОСТРОЕНИЕ ДЕТЕРМИНИРОВАННЫХ КОНЕЧНЫХ АВТОМАТОВ ПО ПРИМЕРАМ ПОВЕДЕНИЯ С ИСПОЛЬЗОВАНИЕМ ПОДХОДА УТОЧНЕНИЯ АБСТРАКЦИИ ПО КОНТРПРИМЕРАМ

НАУЧНО-ТЕХНИЧЕСКИИ ВЕСТНИК ИНФОРМАЦИОННЫХ ТЕХНОЛОГИИ, МЕХАНИКИ И ОПТИКИ май-июнь 2020 Том 20 № 3 ISSN 2226-1494 http://ntv.itmo.ru/

SCIENTIFIC AND TECHNICAL JOURNAL OF INFORMATION TECHNOLOGIES, MECHANICS AND OPTICS May-June 2020 Vol. 20 No 3 ISSN 2226-1494 http://ntv.itmo.ru/en/

HHIIIDPMAPDHHhlX ТЕХНОЛОГИЙ, МЕХАНИКИ И ОПТИКИ

УДК 004.832.25 doi: 10.17586/2226-1494-2020-20-3-394-401

ПОСТРОЕНИЕ ДЕТЕРМИНИРОВАННЫХ КОНЕЧНЫХ АВТОМАТОВ ПО ПРИМЕРАМ ПОВЕДЕНИЯ С ИСПОЛЬЗОВАНИЕМ ПОДХОДА УТОЧНЕНИЯ АБСТРАКЦИИ ПО КОНТРПРИМЕРАМ

И.Т. Закирзянов

Университет ИТМО, Санкт-Петербург, 197101, Российская Федерация Адрес для переписки: ilya.zakirzyanov@gmail.com Информация о статье

Поступила в редакцию 23.03.20, принята к печати 28.04.20 Язык статьи — русский

Ссылка для цитирования: Закирзянов И.Т. Построение детерминированных конечных автоматов по примерам поведения с использованием подхода уточнения абстракции по контрпримерам // Научно-технический вестник информационных технологий, механики и оптики. 2020. Т. 20. № 3. С. 394-401. doi: 10.17586/2226-1494-2020-20-3-394-401

Аннотация

Предмет исследования. Рассмотрена задача построения детерминированного конечного автомата минимального размера по примерам поведения. Разработан и реализован комбинированный метод решения данной задачи на основе сведения к задаче выполнимости булевых формул и с использованием подхода уточнения абстракции по контрпримерам. Метод. Предлагается в качестве исходных данных использовать не все примеры поведения сразу, а начинать с какого-то их подмножества, и строить соответствующий автомат, используя метод на основе сведения к задаче выполнимости. Затем построенный автомат проверяется на соответствие всем остальным примерам поведения. Те примеры, на которых поведение автомата расходится с желаемым, являются контрпримерами. Часть контрпримеров добавляется к исходным примерам поведения и процесс повторяется. Основные результаты. Предложенный метод реализован как часть программного комплекса для решения задачи построения детерминированного конечного автомата по примерам поведения на языке Python. Проведено экспериментальное сравнение разработанного метода с методом, основанным на сведении к задаче выполнимости булевых формул, но без использования подхода уточнения абстракции. Практическая значимость. Экспериментальное исследование показало, что разработанный метод целесообразно использовать при условии, что число примеров поведения достаточно велико — хотя бы в двести раз превышает количество состояний автомата, — и, как следствие, строящаяся булева формула содержит десятки и сотни миллионов дизъюнктов. Ключевые слова

построение детерминированного конечного автомата, задача выполнимости, уточнение абстракции по контрпримерам, нарушение симметрии, грамматический вывод, машинное обучение Благодарности

Исследование выполнено при финансовой поддержке РФФИ в рамках научного проекта № 18-37-00425.

doi: 10.17586/2226-1494-2020-20-3-394-401

DETERMINISTIC FINITE AUTOMATA LEARNING USING COUNTEREXAMPLE GUIDED ABSTRACTION REFINEMENT

I.T. Zakirzyanov

ITMO University, Saint Petersburg, 197101, Russian Federation Corresponding author: ilya.zakirzyanov@gmail.com Article info

Received 23.03.20, accepted 28.04.20 Article in Russian

For citation: Zakirzyanov I.T. Deterministic finite automata learning using counterexample guided abstraction refinement. Scientific and Technical Journal of Information Technologies, Mechanics and Optics, 2020, vol. 20, no. 3, pp. 394-401 (in Russian). doi: 10.17586/2226-1494-2020-20-3-394-401

Abstract

Subject of Research. The paper studies minimum-sized deterministic finite automata inferring problem. A hybrid method is developed and implemented reducing the given problem to Boolean satisfiability (SAT) technique and at the same

time applying a counterexample guided abstraction refinement approach. Method. It is proposed to use not all given behavior examples as training data but start with some subset of them and build a consistent automaton, using SAT-based automata inferring method. Then the built automaton is checked against the complete set of behavior examples. The examples not consistent with the automaton are counterexamples. Some subset of counterexamples is added to the current training data and the process is being repeated. Main Results. The proposed method is implemented as a part of deterministic finite automata inferring tool in Python language. Experimental comparison of the developed method and the SAT-based method without abstraction refinement is carried out. Practical Relevance. Experimental research has shown that the developed method is reasonable for application if the number of behavior examples is large enough, at least, two hundred times exceeds the number of the automaton states, and, therefore, the Boolean formula being created contains tens and hundreds of millions of clauses. Keywords

deterministic finite automata inference, Boolean satisfiability, counterexample guided abstraction refinement, symmetry

breaking, grammatical inference, machine learning

Acknowledgements

The reported study was funded by the RFBR according to the research project No. 18-37-00425.

Введение

Задача построения детерминированного конечного автомата (ДКА) минимального размера по примерам поведения является классической задачей такой области машинного обучения как грамматический вывод. Исследования, посвященные решению данной задачи, проводятся в течение нескольких последних десятилетий. Существует множество прикладных задач, сводящихся к задаче построения ДКА, например, [1, 2]. Первая фундаментальная работа по построению ДКА минимального размера появилась в 70-х годах прошлого века [3]. Следующие важные работы в данной области проводились в 90-х годах: сведение к задаче раскраски графа [4]; использование подходов программирования в ограничениях [5, 6]; подходы на основе алгоритма слияния состояний [7, 8]. В последние годы были предложены подходы, основанные на сведении к задачам выполнимости:

— булевых формул (Boolean Satisfiability problem, SAT)

— формул в теориях (Satisfiability Modulo Theories,

SMT) [2].

Если предложенные ранее алгоритмы являются эвристическими (неточными), то подходы, основанные на сведении к SAT и SMT, позволяют решать поставленную задачу точно. Ими гарантируется, что если в результате работы алгоритма найден некоторый ДКА, то он минимального размера. Недостатком данных методов изначально являлось их время работы и применимость для задач, где размер автомата представляется хотя бы двузначным числом. В последние годы автором данного исследования и его коллегами были предложены различные подходы к нарушению симметрии и другие способы сокращения пространства поиска, что привело к значительному расширению применимости методов, основанных на сведении к SAT [12-14]. Однако, несмотря на разработанные улучшения, эффективность данных методов сильно падает как при увеличении размера искомого автомата, так и при увеличении размера входных данных — примеров поведения. Данная работа посвящена разработке метода, позволяющего эффективно решать задачу построения ДКА при наличии большого количества примеров поведения.

Предлагается новый комбинированный метод, объединяющий подход, основанный на сведении к SAT, с подходом уточнения абстракции по контрпримерам [15]. Использование подхода уточнения абстракции позволяет среди всех примеров поведения рассматривать только значимые, игнорируя те, которые дублируют уже имеющуюся информацию. Таким образом, автомат, построенный комбинированным методом, будет соответствовать всем примерам поведения, но для его построения будет использоваться только их часть.

Постановка задачи

Детерминированным конечным автоматом D называется кортеж (D, 2, 5, d1, D+, D- ), где D — конечное множество состояний; 2 — алфавит; 5: D х 2 ^ D — функция перехода; d1 — стартовое состояние; D+ — множество допускающих (принимающих) состояний; D- = D\\D+ — множество не допускающих (отвергающих) состояний. Изначально автомат D находится в стартовом состоянии d^ В качестве входных данных автомату передается строка (слово) s £ 2*. Автомат считывает символы строки s по одному, и при считывании очередного символа ct переходит из текущего состояния d в состояние 5(d, c). Процесс продолжается до тех пор, пока автомат не считает все символы строки s. Если после этого автомат оказался в допускающем состоянии, то говорят, что автомат D допускает (принимает) слово s. Иначе говоря, автомат D не допускает (отвергает) слово s. Можно индуктивно определить функцию перехода 8: D х 2* ^ D следующим образом: 5(d1, е) = d1 (е — пустая строка); для s = s&c верно, что 5(d1, е) = 5^(d1, s&), c).

В данной работе рассматривается задача пассивного построения минимального ДКА по имеющимся примерам поведения — множеству строк, которые были приняты или отвергнуты некоторым неизвестным ДКА И = (U, 2, р., щ, U+, U-). Альтернативой является задача активного построения минимального ДКА [2, 16], когда алгоритм построения может делать некоторые запросы к оракулу, который имеет информацию о неизвестном ДКА.

Для простоты будем считать, что примеры поведения представлены двумя множествами слов над алфавитом 2: S+ — множество слов, допущенных неизвестным автоматом И; S_ — множество слов, отвергнутых неизвестным автоматом 1L. Примеры поведения можно представить в виде расширенного префиксного дерева (Augmented Prefix Tree Acceptor, APTA) T = (T, 2, т, th T+, T-). Все элементы кортежа соответствуют тем, что даны в определении ДКА с единственным отличием, что T+ U T- ф T. Иными словами, в расширенном префиксном дереве Т присутствуют как принимающие и отвергающие состояния, так и неопределенные. Помимо этого, расширенное префиксное дерево обладает всеми свойствами обычных префиксных деревьев: для двух примеров поведения ^ = ssj и sj = ss2 их общий префикс s соответствует уникальной последовательности состояний в APTA.

Таким образом,

Т= Ut(Íi;S).

Будем считать, что |T| = N. Пример расширенного префиксного дерева представлен на рис. 1.

Задача построения ДКА минимального размера заключается в поиске такого ДКА D = (D, 2, 5, dj, D+, D ), что |D| — минимально, и для любой строки s € S+ верно, что 5(d:, s) € D+, а для любой строки s& € S_ верно, что 5(dj, s&) € D-. Будем считать, что |D| = M.

Задача выполнимости булевых формул

Пусть X = (xj, ..., xn} — конечное множество булевых переменных. Литералом называется либо переменная x¡, либо ее отрицание —x¡. Дизъюнктом называется дизъюнкция нескольких (возможно одного) литералов, например (xj V —x2 V x4 V—x6). Также дизъюнкт можно представить в виде множества литералов, подразумевая, что они связаны дизъюнкцией — (xj, —xj, x4, —x6}. Булева формула, представленная в конъюнктивно-нормальной форме (КНФ), является конъюнкцией некоторых дизъюнктов, например (xj V x3) Л (—xj V —x3 V x^) Л (x6) . Иначе булеву формулу в КНФ можно представить как множество дизъюнктов — {{xj, x3}, {—x2, —x3, x5}, (x6}}. В данной работе принято, что любая булева формула представлена в

КНФ. Выполняющей подстановкой v = (v1; ..., vn) для некоторой булевой формулы ф называется такой булев вектор, что для всех i при подстановке значения vi вместо переменной xi в формуле ф, получается тождественно истинное выражение. Задача выполнимости булевых формул заключается в определении — существует ли выполняющая подстановка v для данной формулы ф [17]. Формула ф передается одному из существующих программных средств для решения SAT, которое выносит вердикт: SAT (satisfiable) — если подстановка v существует; UNSAT (unsatisfiable) — иначе. Большинство современных программных средств возвращают также саму подстановку v в случае вердикта SAT.

Подход к построению минимального ДКА по заданным примерам поведения при помощи сведения к задаче SAT

Среди множества других подходов к решению задачи построения ДКА минимального размера по заданным примерам поведения следует выделить подход, основанный на сведении к SAT. Данный подход в отличие от других является точным — гарантируется, что найденный автомат будет минимально возможным. На рис. 2 представлен наиболее успешный вариант данного подхода. По примерам поведения строится расширенное префиксное дерево Т. Затем неким (обычно эвристическим) алгоритмом ищется нижняя оценка l на размер искомого ДКА. После этого, начиная с нижней оценки l, для каждого возможного числа состояний некоторый алгоритм определяет, существует ли ДКА D такого размера, соответствующий префиксному дереву Т. Таким образом гарантируется минимальность найденного автомата D.

Задача поиска ДКА фиксированного размера является NP-полной [18], а значит, может быть сведена к задаче SAT. Такое сведение было предложено в [9]. Далее приводится данное сведение в кратком изложении.

Необходимо решить следующую задачу: для расширенного префиксного дерева Т = (T, 2, т, t1, T+, T-) определить, существует ли ДКА D = (D, 2, 5, d1, D+, D ) такой, что |D| = M. Для решения поставленной задачи авторы [9] предложили задать соответствие между имеющимся префиксным деревом Т и искомым автоматом D.

Рис. 1. Расширенное префиксное дерево для Е = {а; Ь}, 5+ = {а; аааа; ЬЬ} и = {аа; ЬаЬ}, где вершины: с двойной сплошной границей — принимающие (2, 4, 7); с прерывистой внешней границей — отвергающие (5, 9); с одинарной границей — неопределенные (1, 3, 6, 8)

Рис. 2. Точный алгоритм поиска минимального детерминированного конечного автомата по примерам поведения

Для того чтобы закодировать данную задачу на языке SAT, нужно определить три набора булевых переменных:

Все приведенные выше наборы дизъюнктов можно объединить в одну формулу и передать программному средству для решения задачи SAT. Если программное средство найдет выполняющую подстановку, то автомат размера M, соответствующий имеющимся примерам поведения, представленным в виде расширенного префиксного дерева Т, существует. Этот автомат можно построить, воспользовавшись переменными yi ¡j и z.

Представленное выше кодирование содержит 0(M3 + Ж х M2) дизъюнктов и O(M2 + Ж х M) переменных. Учитывая, что обычно Ж » M (Ж ~ 103-104; M ~ 10 - 100), то можно заключить, что сведение содержит 0(Ж х M2) дизъюнктов. Данный подход сам по себе не показывает выдающихся результатов, но в совокупности с идеями, кратко представленными в следующем разделе, его применимость значительно возрастает.

Подходы к сокращению пространства поиска в задаче построения ДКА минимального размера по заданным примерам поведения

В статье [9] авторы предложили дополнительно использовать структуру данных, названную как граф совместимости (consistency graph). Несмотря на то, что для данной структуры данных больше подходит название граф несовместимости, далее будет использоваться оригинальное название. Основная идея состоит в том, что, имея расширенное префиксное дерево Т = (T, 2, т, t1, T+, T-), можно построить граф Q = (V, E) такой, что V = T, а E определяется следующим образом. Две вершины в графе соединены ребром тогда и только тогда, когда слияние данных вершин в префиксном дереве в одну и последующее избавление от недетерминированности путем слияния потомков, в которые есть переход по одному и тому же символу, приводят к ситуации, когда объединяются принимающее и отвергающее состояния.

Иными словами, если две вершины являются смежными в графе совместимости, то они не могут соответствовать одному и тому же состоянию в ДКА. Это свойство можно выразить с помощью дизъюнктов вида (-xv i v-xw i) для v, w в [N]; (v, w) в E; i в [M]. Такие дизъюнкты не являются обязательными, но они сильно сокращают пространство поиска программного средства для решения задачи SAT. Минусом использования графа совместимости является то, что в общем случае необходимо добавить 0(N2 х M) дизъюнктов, что сильно увеличивает размер формулы.

Помимо этого, было предложено несколько подходов к нарушению симметрии в данной задаче. Лучше всего себя зарекомендовали предикаты нарушения симметрии на основе алгоритма обхода в ширину (Breadth-First Search, BFS), предложенные в [12-14]. Основная идея заключается в том, чтобы путем добавления новых ограничений в сведение зафиксировать нумерацию искомого ДКА в порядке его обхода в ширину. Такие ограничения позволяют запретить программному средству рассматривать M! изоморфных автоматов, оставив по одному представителю для каждого класса эквивалентности по изоморфизму. Последняя модификация данных предикатов может быть выражена через 0(M2 х L) дизъюнктов. Подробное описание предикатов нарушения симметрии можно найти в оригинальной работе [12].

В [13] можно найти некоторые другие идеи по сокращению пространства поиска, которые не относятся непосредственно к настоящей работе, но могут быть полезны для ознакомления.

Метод уточнения абстракции по контрпримерам

Главной проблемой методов решения задачи построения минимального ДКА по примерам поведения при помощи сведения к SAT является размер получающейся формулы. Ранее в [12-14] были предложены как более компактные способы кодирования поставленной задачи на языке SAT, так и различные подходы к сокращению пространства поиска. Тем не менее, подход, основанный на сведении к задаче выполнимости, все еще мало применим в случае, когда префиксное дерево большое. Следует заметить, что префиксное дерево увеличивается в размере как при увеличении числа примеров поведения, так и при увеличении их длины. В данном разделе описан новый подход к решению задачи построения минимального ДКА, позволяющий решить вышеуказанную проблему.

В случае, когда стоит задача построить некоторую модель, при этом имея доступ к проверяющей системе, часто применяется метод уточнения абстракции по контрпримерам (Counterexample-Guided Abstraction Refinement, CEGAR). Суть данного метода можно описать следующим образом. На начальном шаге генерируется некоторая, возможно случайная модель. Затем на каждом следующем шаге данная модель проходит

проверку некоторой проверяющей системы. Если проверка проходит успешно, то искомая модель найдена. Иначе система возвращает один или несколько контрпримеров, которые затем используются для улучшения модели. Процесс повторяется, пока не будет найдена модель, проходящая проверку системы. Данный подход больше похож на метод активного построения модели, в то время как в данной работе рассматривается задача пассивного построения —все примеры поведения известны заранее и никакой дополнительной информации в ходе построения автомата быть получено не может. Однако далее приводится описание того, как метод уточнения абстракции можно применить для построения ДКА.

Для начального шага выбирается некоторое подмножество примеров поведения (возможно пустое), по которому строится расширенное префиксное дерево Т, выбирается нижняя оценка на размер искомого ДКА, а затем используется сведение к SAT, описанное ранее. Если программное средство не смогло найти автомат текущего размера, то текущий размер увеличивается на один и процесс повторяется. Если же какой-то автомат, соответствующий дереву Т , найден, то оставшиеся неиспользуемые пока примеры поведения проверяются на соответствие текущему ДКА. Множество слов, которые не соответствуют автомату, образуют множество контрпримеров. После этого выбирается некоторое подмножество (или все множество) контрпримеров, которые добавляются в дерево Т и процесс повторяется (рис. 3). Таким образом, вместо построения слишком большой формулы, описывающей все имеющиеся примеры поведения, формула итеративно достраивается и описывает только часть примеров, что должно сократить время на решение SAT.

Другим важным достоинством предлагаемого метода является то, что большинство современных программных средств для решения задачи выполнимости могут работать в так называемом итеративном режиме. В стандартном режиме после вынесения вердикта SAT или UNSAT программное средство прекращает работу. В итеративном же режиме, если формула выполнима и вердикт SAT, то программное средство сохраняет свое состояние и ожидает новых ограничений. Можно закодировать новые свойства, используя уже имеющиеся булевы переменные и добавляя новые, и передать получившуюся формулу программному средству. После этого программное средство продолжит решение задачи с того момента, где остановилось. Такой подход позволяет не делать программному средству одну и ту же работу несколько раз. Заметим, что при добавлении новых примеров поведения и расширении префиксного дерева Т никакие старые дизъюнкты не убираются, только добавляются новые, что делает возможным использование программных средств для решения SAT в итеративном режиме.

Важным вопросом является то, сколько контрпримеров добавлять на каждом шаге. Добавление слишком маленького числа контрпримеров может привести к тому, что накладные расходы на построение префиксного дерева, построение и передачу новых дизъюнктов программному средству для решения SAT будут преРис. 3. Комбинированный алгоритм построения минимального детерминированного конечного автомата по примерам поведения с использованием подхода уточнения абстракции по контрпримерам

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

Экспериментальные результаты

Предложенный в предыдущем разделе комбинированный метод построения ДКА минимального размера на основе сведения к SAT и с использованием подхода уточнения абстракции по контрпримерам был реализован на языке Python как модуль программного комплекса DFA-Inductor-py. Эксперименты проводились на персональном компьютере с процессором QuadCore Intel Core i7-8550U @ 4 ГГц, 16 ГБ оперативной памяти и операционной системой ArchLinux 5.5.6. Для проведения экспериментов было сгенерировано 100 тестовых экземпляров с помощью алгоритма, разработанного автором ранее и описанного в [14]. Параметры для генерации автоматов были выбраны следующим образом:

- размеры автоматов, которые нужно построить, —

Mе [15; 25];

— количество примеров поведения S=S+ U S_ е {50 х N;

В экспериментах проводилось сравнение разработанного комбинированного метода с предложенным в [13] методом, основанным только на сведении к SAT.

Результаты показали, что при относительно небольшом количестве примеров поведения (S е {50 х N;

Таким образом, можно сделать вывод, что использование разработанного метода целесообразно, когда количество примеров поведения велико, и метод, основанный только на сведении к SAT, не применим ввиду слишком большой формулы.

Заключение

В данной работе предложен новый комбинированный алгоритм построения детерминированного конечного автомата минимального размера по примерам поведения, основанный на сведении к задаче выполнимости булевых формул и с использованием подхода уточнения абстракции по контрпримерам. Экспериментальное исследование показало, что разработанный метод эффективен при условии, что число примеров поведения достаточно велико — хотя бы в двести раз превышает количество состояний, — и, как следствие, строящаяся булева формула содержит десятки и сотни миллионов дизъюнктов. Использование

комбинированного метода позволяет сократить количество используемых примеров поведения без потери точности.

Для дальнейшего исследования остается вопрос об эффективности предложенного метода в других

частных, но важных случаях задачи построения минимального детерминированного конечного автомата. Например, когда автомат имеет какую-то особенную структуру, или среди примеров поведения много таких, которые покрывают только одну часть автомата.

Литература

References

Авторы

Закирзянов Илья Тимурович — аспирант, программист, Университет ИТМО, Санкт-Петербург, 197101, Российская Федерация, Scopus ID: 56613352900, ORCID ID: 0000-0002-3460-3489, ilya.zakirzyanov@gmail.com

Ilya T. Zakirzyanov—Postgraduate, Software Engineer, ITMO University, Saint Petersburg, 197101, Russian Federation, Scopus ID: 56613352900, ORCID ID: 0000-0002-3460-3489, ilya.zakirzyanov@gmail.com