Learning Deterministic Finite Automata Decompositions from Examples and Demonstrations

Niklas Lauffer, Beyazit Yalcinkaya, Marcell Vazquez-Chanlatte, Ameesh Shah, and Sanjit A. Seshia. Learning Deterministic Finite Automata Decompositions from Examples and Demonstrations. In Proceedings of the IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD), October 2022.

Download

[pdf] 

Abstract

The identification of a deterministic finite automaton (DFA) from labeled examples is a well-studied problem in the literature; however, prior work focuses on the identification of monolithic DFAs. Although monolithic DFAs provide accurate descriptions of systems’ behavior, they lack simplicity and interpretability; moreover, they fail to capture sub-tasks realized by the system and introduce inductive biases away from the inherent decomposition of the overall task. In this paper, we present an algorithm for learning conjunctions of DFAs from labeled examples. Our approach extends an existing SAT-based method to systematically enumerate Pareto-optimal candidate solutions. We highlight the utility of our approach by integrating it with a state-of-the-art algorithm for learning DFAs from demonstrations. Our experiments show that the algorithm learns sub-tasks realized by the labeled examples, and it is scalable in the domains of interest.

BibTeX

@InProceedings{lauffer-fmcad22,
  Author = {Niklas Lauffer and Beyazit Yalcinkaya and Marcell Vazquez-Chanlatte and Ameesh Shah and Sanjit A. Seshia},
  Title = {Learning Deterministic Finite Automata Decompositions from Examples and Demonstrations},
  booktitle = {Proceedings of the IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD)},
  month = "October",
  year = {2022},
  abstract = {The identification of a deterministic finite automaton (DFA) from labeled examples is a well-studied problem in the literature; however, prior work focuses on the identification of monolithic DFAs. Although monolithic DFAs provide accurate descriptions of systems’ behavior, they lack simplicity and interpretability; moreover, they fail to capture sub-tasks realized by the system and introduce inductive biases away from the inherent decomposition of the overall task. In this paper, we present an algorithm for learning conjunctions of DFAs from labeled examples. Our approach extends an existing SAT-based method to systematically enumerate Pareto-optimal candidate solutions. We highlight the utility of our approach by integrating it with a state-of-the-art algorithm for learning DFAs from demonstrations. Our experiments show that the algorithm learns sub-tasks realized by the labeled examples, and it is scalable in the domains of interest.},
}