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.
Tue 13 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
11:00 - 12:30 | |||
11:00 30mTalk | Multi-variable Quantification of BDDs in External Memory using Nested Sweeping VMCAI 2026 | ||
11:30 30mTalk | Producing Shorter Congruence Closure Proofs in a State-of-the-Art SMT Solver VMCAI 2026 Bruno Andreotti Universidade Federal de Minas Gerais, Haniel Barbosa Universidade Federal de Minas Gerais | ||
12:00 30mTalk | SAT-Based Synthesis of Minimal Deterministic Real-Time Automata via 3DRTA Representation VMCAI 2026 Junjie Meng School of Computer Science and Technology, Tongji University, Jie An Institute of Software Chinese Academy of Sciences, Yong Li Institute of Software, Chinese Academy of Sciences, Andrea Turrini Institute of Software, Chinese Academy of Sciences, Miaomiao Zhang School of Computer Science and Technology, Tongji University | ||