Passive Learning of Symbolic Automata over Monotonic Algebras
For researchers in automata theory and software verification, this work provides a passive learning algorithm for symbolic automata, which is an incremental extension of existing methods.
The paper tackles passive learning of symbolic automata over monotonic algebras, providing an algorithm (SAI) that efficiently identifies such automata in the limit from a sample. The algorithm extends RPNI with a splitting operation and admits polynomial size characteristic samples.
Symbolic automata extend classical finite-state automata to handle large or infinite alphabets by labeling transitions by predicates coming from a boolean algebra. Many results from automata theory have been lifted to this model, and it has proved its usefulness for example in multiple software verification applications. Here, we tackle the passive learning problem of identification in the limit, i.e. learning a model from a sample without access to an oracle to query. We provide an algorithm, SAI, that efficiently identifies in the limit symbolic automata over any monotonic algebra where predicates labeling transitions are of the form a <= x < b. The algorithm extends the RPNI framework for passive learning of finite-state automata to symbolic automata thanks to a new splitting operation inspired by RTI, a passive learning algorithm for deterministic real-time automata, a subclass of timed automata. The learning algorithm combines merging of states and splitting of states allowing to infer the predicates on transitions in a top-down fashion. We prove that SAI admits polynomial size characteristic samples.