דנה פיסמן

Traditional automata classify words from a given alphabet as either good or bad. In many scenarios, in particular in formal verification, a finer classification is required. Fully-ordered lattice automata (FOLA) associate with every possible word a value from a finite set of values such as { 0, 1, 2, …, k}. In this paper we are interested in learning formal series that can be represented by FOLA. Such a series can be learned by a straight forward extension of the L^∗ algorithm. However, this approach does not take advantage of the special structure of a FOLA. In this paper we investigate FOLAs and provide a Myhill-Nerode characterization for FOLAs, which serves as a basis for providing a specialized algorithm for FOLAs, which we term FOL^∗. We compare the performance of FOL^∗ to that of L^∗ on synthetically generated FOLA. Our experiments show that FOL^∗ outperforms L^∗ in the number of states of the obtained FOLA, the number of issued value queries (the extension of membership queries to the quantitative setting), and the number of issued equivalence queries.