Real-time automata (RTAs) can be viewed as a subclass of timed automata with only one clock that resets at each transition. In this paper, we propose a novel framework for learning deterministic RTAs (DRTAs) with minimal number of states from samples. Inspired by recent advances in learning deterministic finite automata, we introduce 3-valued Deterministic Real-Time Automata (3DRTAs) as an intermediate representation for the given sample set, thereby eliminating the redundancies present in existing approaches. Then, we solve the minimal DRTA learning problem from 3DRTAs by a reduction to a Boolean Satisfiability (SAT) problem. This then allows us to leverage state-of-the-art SAT solvers to find a minimal DRTA consistent with the given samples efficiently. More importantly, small DRTAs not only offer compact representation but also better interpretability of real-world systems. Experimental results demonstrate that our 3DRTA-based framework yields minimal DRTAs with significantly fewer states compared to those of existing methods. The proposed technique also opens new possibilities for scalable real-time automata learning in complex real-time domains.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

SAT-Based Synthesis of Minimal Deterministic Real-Time Automata via 3DRTA Representation

  • Junjie Meng,
  • Jie An,
  • Yong Li,
  • Andrea Turrini,
  • Miaomiao Zhang

摘要

Real-time automata (RTAs) can be viewed as a subclass of timed automata with only one clock that resets at each transition. In this paper, we propose a novel framework for learning deterministic RTAs (DRTAs) with minimal number of states from samples. Inspired by recent advances in learning deterministic finite automata, we introduce 3-valued Deterministic Real-Time Automata (3DRTAs) as an intermediate representation for the given sample set, thereby eliminating the redundancies present in existing approaches. Then, we solve the minimal DRTA learning problem from 3DRTAs by a reduction to a Boolean Satisfiability (SAT) problem. This then allows us to leverage state-of-the-art SAT solvers to find a minimal DRTA consistent with the given samples efficiently. More importantly, small DRTAs not only offer compact representation but also better interpretability of real-world systems. Experimental results demonstrate that our 3DRTA-based framework yields minimal DRTAs with significantly fewer states compared to those of existing methods. The proposed technique also opens new possibilities for scalable real-time automata learning in complex real-time domains.