SAT-Based Synthesis of Minimal Deterministic Real-Time Automata via 3DRTA Representation
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 samples, 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 efficiently find the minimal DRTA consistent with given samples. 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.