AIを含むソフトウェアのための形式検証手法
项目来源
项目主持人
项目受资助机构
项目编号
立项年度
立项时间
研究期限
项目级别
受资助金额
学科
学科代码
基金类别
关键词
参与者
参与机构
1.Active Learning ofSymbolic Mealy Automata
- 关键词:
- Finite automata;Set theory;Active Learning;Active-learning algorithm;Automaton learning;Finite set;Learn+;Mealy automatons;Multiple outputs;Output functions;Symbolic automaton;Under-approximation
- Irie, Kengo;Waga, Masaki;Suenaga, Kohei
- 《22nd International Colloquium on Theoretical Aspects of Computing, ICTAC 2025》
- 2026年
- November 24, 2025 - November 28, 2025
- Marrakesh, Morocco
- 会议
We propose ΛM∗—an active learning algorithm that learns symbolic Mealy automata, which support infinite input alphabets and multiple output characters. Each of these two features has been addressed separately in prior work. Combining these two features poses a challenge in learning the outputs corresponding to potentially infinite sets of input characters at each state. To address this challenge, we introduce the notion of essential input characters, a finite set of input characters that is sufficient to learn the output function of a symbolic Mealy automaton. ΛM∗ maintains an underapproximation of the essential input characters and refines this set during learning. We prove that ΛM∗ terminates under certain assumptions. Moreover, we provide upper and lower bounds for the query complexity. Their similarity suggests the tightness of the bounds. We empirically demonstrate that ΛM∗ is i) efficient regarding the number of queries on practical benchmarks and ii) scalable according to evaluations with randomly generated benchmarks. © The Author(s), under exclusive license to Springer Nature Switzerland AG 2026.
...
