Differences

This shows you the differences between two versions of the page.

--- start [2018/11/13 15:36] – liyong
+++ start [2020/12/16 15:03] (current) – [New Features in ROLL v1.0] liyong
@@ Line 9: / Line 9: @@
-ROLL is a Library of learning algorithms for ω-regular languages. It consists of all complete class of ω-regular languages learning algorithms available in the literature, namely
+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 algorithm for FDFAs
+  - 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 algorithm for Büchi automata
+  - 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 algorithm in [10] 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
@@ Line 22: / Line 22: @@
 ===== 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 large rewrite of the previous version used in the TACAS paper.
+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]].
+  * [[https://iscasmc.ios.ac.cn/roll/jupyter|Jupyter notebook for ROLL]] (You can **play with ROLL online** !!!).
-  * Interactive mode for education purpose.
+  * Interactive mode for educational 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]).
+  * PAC-learning for Büchi automata based on Monte-Carlo word sampling (our improved version [9] 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 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 [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).
 ----
@@ Line 50: / Line 60: @@
 [8] Radu Grosu, Scott A. Smolka. "Monte carlo model checking." In TACAS. Springer-Verlag Berlin, Heidelberg, 2005:271-286.
+[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.
-[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)
+[10] 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. {{ :iandc.pdf |preprint}} (Added an algorithm to transform an FDFA to a limit-deterministic Büchi automaton)