Меню
Публикации
2024
2023
2022
2021
2020
2019
2018
2017
2016
2015
2014
2013
2012
2011
2010
2009
2008
2007
2006
2005
2004
2003
2002
2001
Главный редактор
НИКИФОРОВ
Владимир Олегович
д.т.н., профессор
Партнеры
doi: 10.17586/2226-1494-2020-20-3-394-401
УДК 004.832.25
ПОСТРОЕНИЕ ДЕТЕРМИНИРОВАННЫХ КОНЕЧНЫХ АВТОМАТОВ ПО ПРИМЕРАМ ПОВЕДЕНИЯ С ИСПОЛЬЗОВАНИЕМ ПОДХОДА УТОЧНЕНИЯ АБСТРАКЦИИ ПО КОНТРПРИМЕРАМ
Читать статью полностью
Язык статьи - русский
Ссылка для цитирования:
Аннотация
Ссылка для цитирования:
Закирзянов И.Т. Построение детерминированных конечных автоматов по примерам поведения с использованием подхода уточнения абстракции по контрпримерам // Научно-технический вестник информационных техно- логий, механики и оптики. 2020. Т. 20. № 3. С. 394–401. doi: 10.17586/2226-1494-2020-20-3-394-401
Аннотация
Предмет исследования. Рассмотрена задача построения детерминированного конечного автомата минимального размера по примерам поведения. Разработан и реализован комбинированный метод решения данной задачи на основе сведения к задаче выполнимости булевых формул и с использованием подхода уточнения абстракции по контрпримерам. Метод. Предлагается в качестве исходных данных использовать не все примеры поведения сразу, а начинать с какого-то их подмножества, и строить соответствующий автомат, используя метод на основе сведения к задаче выполнимости. Затем построенный автомат проверяется на соответствие всем остальным примерам поведения. Те примеры, на которых поведение автомата расходится с желаемым, являются контрпримерами. Часть контрпримеров добавляется к исходным примерам поведения и процесс повторяется. Основные результаты. Предложенный метод реализован как часть программного комплекса для решения задачи построения детерминированного конечного автомата по примерам поведения на языке Python. Проведено эксперимен- тальное сравнение разработанного метода с методом, основанным на сведении к задаче выполнимости булевых формул, но без использования подхода уточнения абстракции. Практическая значимость. Экспериментальное исследование показало, что разработанный метод целесообразно использовать при условии, что число приме- ров поведения достаточно велико — хотя бы в двести раз превышает количество состояний автомата, — и, как следствие, строящаяся булева формула содержит десятки и сотни миллионов дизъюнктов.
Ключевые слова: построение детерминированного конечного автомата, задача выполнимости, уточнение абстракции по контр- примерам, нарушение симметрии, грамматический вывод, машинное обучение
Благодарности. Исследование выполнено при финансовой поддержке РФФИ в рамках научного проекта № 18-37-00425.
Список литературы
Благодарности. Исследование выполнено при финансовой поддержке РФФИ в рамках научного проекта № 18-37-00425.
Список литературы
-
Wieman R., Aniche M.F., Lobbezoo W., Verwer S., Van Deursen A. An experience report on applying passive learning in a large-scale payment company // Proc. 33rd IEEE International Conference on Software Maintenance and Evolution (ICSME). Shanghai, China. 2017. P. 564–573. doi: 10.1109/ICSME.2017.71
-
Neider D. Applications of Automata Learning in Verification and Synthesis: PhD thesis. Hochschulbibliothek der Rheinisch-Westfälischen Technischen Hochschule Aachen, 2014. 283 p.
-
Biermann A.W., Feldman J.A. On the synthesis of finite-state machines from samples of their behavior // IEEE Transactions on Computers. 1972. V. C-21. N 6. P. 592–597. doi: 10.1109/TC.1972.5009015
-
Coste F., Nicolas J. Regular inference as a graph coloring problem // Proc. 14th International Conference on Machine Learning (ICML), Workshop on Grammatical Inference, Automata Induction, and Language Acquisition. Nashville, Tennessee, USA. 1997.
-
Coste F., Nicolas J. How considering incompatible state mergings may reduce the DFA induction search tree // Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 1998. V. 1433. P. 199–210. doi: 10.1007/BFb0054076
-
Oliveira A.L., Silva J.P.M. Efficient algorithms for the inference of minimum size DFAs // Machine Learning. 2001. V. 44. N 1-2. P. 93–119. doi: 10.1023/A:1010828029885
-
Lang K.J. Faster Algorithms for Finding Minimal Consistent DFAs: Technical Report. NEC Research Institute, 1999. 19 p.
-
Lang K.J., Pearlmutter B.A., Price R.A. Results of the Abbadingo one DFA learning competition and a new evidence-driven state merging algorithm // Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 1998. V. 1433. P. 1–12. doi: 10.1007/BFb0054059
-
Heule M., Verwer S. Exact DFA identification using SAT solvers // Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2010. V. 6339. P. 66–79. doi: 10.1007/978-3-642-15488-1_7
-
Ulyantsev V., Tsarev F. Extended finite-state machine induction using SAT-solver // Proc. 10th International Conference on Machine Learning and Applications and Workshops. Honolulu, Hawaii, USA. 2011. P. 346–349. doi: 10.1109/ICMLA.2011.166
-
Grinchtein O., Leucker M., Piterman N. Inferring network invariants automatically // Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2006. V. 4130. P. 483–497. doi: 10.1007/11814771_40
-
Ulyantsev V., Zakirzyanov I., Shalyto A. BFS-based symmetry breaking predicates for DFA identification // Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2015. V. 8977. P. 611–622. doi: 10.1007/978-3-319-15579-1_48
-
Zakirzyanov I., Morgado A., Ignatiev A., Ulyantsev V., Silva J.M. Efficient symmetry breaking for SAT-based minimum DFA inference // Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2019. V. 11417. P. 159–173. doi: 10.1007/978-3-030-13435-8_12
-
Zakirzyanov I., Shalyto A., Ulyantsev V. Finding all minimum-size DFA consistent with given examples: SAT-based approach // Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2018. V. 10729. P. 117–131. doi: 10.1007/978-3-319-74781-1_9
-
Clarke E.M., Grumberg O., Jha S., Lu Y., Veith H. Counterexample-guided abstraction refinement for symbolic model checking // Journal of the ACM. 2003. V. 50. N 5. P. 752–794. doi: 10.1145/876638.876643
-
Angluin D. Learning regular sets from queries and counterexamples // Information and Computation. 1987. V. 75. N 2. P. 87–106. doi: 10.1016/0890-5401(87)90052-6
-
Handbook of Satisfiability / ed. by A. Biere, M. Heule, H. van Maaren, T.Walsh. IOS Press, 2009. 980 p. (Frontiers in Artificial Intelligence and Applications, V. 185)
-
Gold E.M. Complexity of automaton identification from given data // Information and Control. 1978. V. 37. N 3. P. 302–320. doi: 10.1016/S0019-9958(78)90562-4