Trustworthy Intelligent Systems

Regular Omega Language Learning (ROLL)

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

  1. the learning algorithms for FDFAs
    • the algorithm by Angluin and Fisman1 learns three canonical FDFAs using observation tables, which is based on results by Maler and Staiger2,
    • the algorithm by Li et al.3 learns three canonical FDFAs using classification trees;
  2. and the learning algorithms for Büchi automata
    • the algorithm by Farzan et al.4 learns a Büchi automaton by combining L* algorithm5 and results by Calbrix et al.6,
    • the algorithm by Li et al.3 learns the Büchi automata via learning three canonical FDFAs.
    • the algorithm by Li et al.7 learns the limit-deterministic Büchi automata via learning three canonical FDFAs.

The ROLL library is implemented in JAVA. Its DFA operations are delegated to the dk.brics.automaton package. We use the RABIT tool to check the equivalence of two Büchi automata.

New Features in ROLL v1.0

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:

  • Learning algorithm for limit-deterministic Büchi automata.
  • Jupyter notebook for ROLL (You can play with ROLL online!!!).
  • Interactive mode for educational purpose.
  • Büchi automata complementation based on learning8.
  • Büchi automata inclusion testing based on word sampling and learning.
  • PAC-learning for Büchi automata based on Monte-Carlo word sampling (our improved version9 of the algorithm by Grosu and Smolka10).
  • Hanoi omega-automata format.

Before going through other contents on this website, you might need some basic background knowledge in the following.

Active Automata Learning Background Knowledge

In the active automata learning setting proposed by Angluin5, 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 her seminal paper5, Angluin introduced the well-known algorithm L* which learns from a teacher a regular language represented by a deterministic finite automaton (DFA).

Material for ROLL

  1. Dana Angluin, and Dana Fisman. “Learning regular omega languages.” In ALT. Springer International Publishing, 2014: 125-139. ↩

  2. Oded Maler and Ludwig Staiger. “On syntactic congruences for ω-languages.” In STACS. Springer Berlin Heidelberg, 1993: 586-594. ↩

  3. 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 ↩ ↩2

  4. 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. ↩

  5. Dana Angluin. “Learning regular sets from queries and counterexamples.” Information and computation 75.2 (1987): 87-106. ↩ ↩2 ↩3

  6. Hugues Calbrix, Maurice Nivat, and Andreas Podelski. “Ultimately periodic words of rational ω-languages.” In MFPS. Springer Berlin Heidelberg, 1993: 554-566. ↩

  7. 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) ↩

  8. Yong Li, Andrea Turrini, Lijun Zhang and Sven Schewe. “Learning to Complement Büchi Automata.” In VMCAI. Springer, Cham, 2018:313-335. ↩

  9. 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. ↩

  10. Radu Grosu, Scott A. Smolka. “Monte Carlo model checking.” In TACAS. Springer-Verlag Berlin, Heidelberg, 2005:271-286. ↩