Regular Omega Language Learning (ROLL)

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.
[[start|{{:home.png?16}}]][[start| Main]]
[[usage|{{:imac.png?16}}]][[usage|How to Use ROLL in Command Line]]
[[how_to_use|{{:pencil.png?16}}]][[how_to_use|How to Use ROLL in JAVA Program]]
[[release|{{:tool.png?16}}]][[release| Tool ]]
[[contact|{{:letter.png?16}}]][[contact| Contact ]]


====== 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
  - the learning algorithms for FDFAs
     * the algorithm in [5] learns three canonical FDFAs using observation tables, which is based on results in [3],
     * the algorithm in [6] learns three canonical FDFAs using classification trees;
  - and the learning algorithms for Büchi automata
     * the algorithm in [4] learns a Büchi automaton by combining L<sup>*</sup> algorithm [1] and results in [2],
     * the algorithm in [6] learns the Büchi automata via learning three canonical FDFAs.
     * the algorithm in [9] 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 [[http://www.brics.dk/automaton/|dk.brics.automaton]] package. We use [[http://www.languageinclusion.org/doku.php?id=tools|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 [[https://github.com/ISCAS-PMC/roll-library| 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.
  * [[https://iscasmc.ios.ac.cn/roll/jupyter|Jupyter notebook for ROLL]].
  * Interactive mode for education purpose.
  * Büchi automata complementation based on learning [7].
  * 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 version of [8]).
  * [[http://adl.github.io/hoaf/|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 Angluin [1], there are a //teacher//, which 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 [1], Angluin introduced the well-known algorithm L<sup>*</sup> which learns from a teacher a regular language represented by a deterministic finite automaton (DFA).


----

[1] Dana Angluin. "Learning regular sets from queries and counterexamples." Information and computation 75.2 (1987): 87-106.


[2]  Hugues Calbrix, Maurice Nivat, and Andreas Podelski. "Ultimately periodic words of rational ω-languages." In MFPS. Springer Berlin Heidelberg, 1993: 554-566.

[3] Oded Maler and Ludwig Staiger. "On syntactic congruences for ω-languages." In STACS. Springer Berlin Heidelberg, 1993: 586-594.

[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, and Dana Fisman. "Learning regular omega languages." In ALT. Springer International Publishing, 2014: 125-139.

[6] 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. {{ :tacas17.pdf |preprint}}

[7] Yong Li, Andrea Turrini, Lijun Zhang and Sven Schewe. "Learning to Complement Büchi Automata." In VMCAI. Springer, Cham, 2018:313-335.

[8] Radu Grosu, Scott A. Smolka. "Monte carlo model checking." In TACAS. Springer-Verlag Berlin, Heidelberg, 2005:271-286.


[9] 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. {{ :LDBA.pdf |preprint}} (Added an algorithm to transform an FDFA to a limit-deterministic Büchi automaton)