ROLL is a library of learning algorithms for ω-regular languages. It consists of all the learning algorithms for the complete class of ω-regular languages available in the literature, namely
ROLL v1.0 is now publicly available on GitHub at this repository. ROLL v1.0 is a major rewrite of the learning algorithms of the previous version used in the TACAS paper. Compared to its previous version, it now supports new features such as:
Before going through other contents on this website, you might need some basic background knowledge in the following.
In the active automata learning setting proposed by Angluin , there is a teacher, who knows the target language L, and a learner, whose task is to learn from the teacher the target language, represented by an automaton. The learner interacts with the teacher by means of two kinds of queries: membership queries and equivalence queries. A membership query MQ[w] asks whether a string w belongs to L while an equivalence query EQ[A] asks whether the hypothesis automaton A recognizes L. The teacher replies with a witness/counterexample if the hypothesis is incorrect otherwise the learner completes its job. The returned counterexample is a word in the symmetric difference of the language of the conjectured automaton and the target language. In , Angluin introduced the well-known algorithm L* which learns from a teacher a regular language represented by a deterministic finite automaton (DFA).
 Dana Angluin. “Learning regular sets from queries and counterexamples.” Information and computation 75.2 (1987): 87-106.
 Hugues Calbrix, Maurice Nivat, and Andreas Podelski. “Ultimately periodic words of rational ω-languages.” In MFPS. Springer Berlin Heidelberg, 1993: 554-566.
 Oded Maler and Ludwig Staiger. “On syntactic congruences for ω-languages.” In STACS. Springer Berlin Heidelberg, 1993: 586-594.
 Azadeh Farzan, Yu-Fang Chen, Edmund M. Clarke, Yih-Kuen Tsay, Bow-Yaw Wang. “Extending automated compositional verification to the full class of omega-regular languages.” In TACAS. Springer Berlin Heidelberg, 2008: 2-17.
 Dana Angluin, and Dana Fisman. “Learning regular omega languages.” In ALT. Springer International Publishing, 2014: 125-139.
 Yong Li, Yu-Fang Chen, Lijun Zhang, and Depeng Liu. “A Novel Learning Algorithm for Büchi Automata based on Family of DFAs and Classification Trees.” In TACAS. Springer Berlin Heidelberg, 2017: 208-226. preprint
 Yong Li, Andrea Turrini, Lijun Zhang and Sven Schewe. “Learning to Complement Büchi Automata.” In VMCAI. Springer, Cham, 2018:313-335.
 Radu Grosu, Scott A. Smolka. “Monte carlo model checking.” In TACAS. Springer-Verlag Berlin, Heidelberg, 2005:271-286.
 Yong Li, Andrea Turrini, Xuechao Sun and Lijun Zhang. “Proving Non-inclusion of Büchi Automata Based on Monte Carlo Sampling.” In ATVA. Springer, 2020: 467-483.
 Yong Li, Yu-Fang Chen, Lijun Zhang, and Depeng Liu. “A Novel Learning Algorithm for Büchi Automata based on Family of DFAs and Classification Trees.” To appear in I&C. preprint (Added an algorithm to transform an FDFA to a limit-deterministic Büchi automaton)