This is an old revision of the document!
Table of Contents
Büchi Automata Complementation (Buechic)
Buechic is a tool to learn the complement of a given Büchi automaton. It is based on the learning library ROLL [2]. We have added the support for HOA format in ROLL.
Buechic complements a given Büchi automaton B by learning an FDFA [1] which captures all ultimately periodic words of the complement of B. Therefore, our algorithm relies on the language of B instead of on the structure of B, as happens for the classic complementation techniques.
Source Code and Executable Files
- Buechic source code : the source code is released under GPL license
- Buechic executable file: Buechic jar file to complement Büchi automaton
- Buechi complementation with Universality check : the jar file to complement Büchi automaton with universality checking
How to Use Buechic in Command Line
Buechic can be started using java -jar buechic.jar, which is equal to the following command.
java -jar buechic.jar -h
Running Buechic
The command to run Buechic to learn the Büchi automaton given by aut.hoa is:
java -jar buechic.jar aut.hoa -aut -table -periodic
Data Structures
In Buechic, you can specify the data structures for the learning procedure in the following.
- -table. This argument calls for the use of the observation table.
- -tree. It requires to use the classification tree for the learner.
Learning Algorithms
You can also use three canonical FDFAs to learn the Büchi automata as follows.
- -periodic. Learning the periodic FDFA.
- -syntactic. Learning the syntactic FDFA.
- -recurrent. Learning the recurrent FDFA.
Lazy Equivalence Check
If you want to reuse the counterexample returned by the teacher as much as possible, you can use the lazy equivalence check optimization as follows.
java -jar buechic.jar aut.hoa -aut -table -periodic -lazyeq
How to Use Buechic in JAVA Code
We support HOA format in Buechic. An example Büchi automaton is given as follows.
Prepare a HOA file
HOA: v1 name: "GFa" States: 2 Start: 0 Start: 1 acc-name: Buchi Acceptance: 1 Inf(0) AP: 1 "a" --BODY-- State: [0] 0 {0} 0 1 State: [!0] 1 0 1 --END--
Use the complement teacher
If you want to use Buechic in verification or other areas, you should use our complement teacher as follows.
// initialize a parser to parse input automaton Parser parser = new HOAParser(autfile); FiniteAutomaton aut = parser.parse(); // prepare the data structure for alphabet ValueManager contextValue = new ValueManager(); WordManager contextWord = new WordManager(contextValue); // get an instance of our complement teacher ComplementTeacherFDFA teacher = new ComplementTeacherFDFA(contextWord, aut);
Call a learner and specify the BA construction
// specify FDFA learner, here we use table-based periodic FDFA learner LearnerFDFA learner = new LearnerFDFATablePeriodic(contextWord, teacher); // specify the counterexample translator Translator ceTranslator = new TranslatorFDFAUnder(learner);
Learning loop
System.out.println("Start learning..."); Timer timer = new Timer(); timer.start(); learner.startLearning(); timer.stop(); Statistics.timeLearner += timer.getTimeElapsed(); boolean result = false; while(! result ) { Query<EqResult> query = teacher.answerEquivalenceQuery(learner); // get out of the loop if(query.getQueryAnswer().isEqual == true) { Statistics.setLearnerFDFA(learner); Statistics.hypothesis = hypothesis; break; } // lazy equivalence check is implemented here ceTranslator.setQuery(query); while(ceTranslator.canRefine()) { Query<Boolean> ceQuery = ceTranslator.translate(); timer.start(); learner.refineHypothesis(ceQuery); timer.stop(); Statistics.timeLearner += timer.getTimeElapsed(); // set lazyEqCheck to true if you want to reuse the counterexample if(! lazyEqCheck) break; } } System.out.println("Learning completed...");
Büchi Automata and Log Files
We have compared Buechic with GOAL on the automata from BüchiStore and NCSB-complementation. In the following, you can download the logs files of the experiments.
1. The Büchi Automata from BüchiStore can be found on their webpage and the log files are listed as below.
- double complementation on BüchiStore of GOAL
2. The Büchi Automata from NCSB-complementation and the log files are listed as below.
—-
[1] Dana Angluin, and Dana Fisman. “Learning regular omega languages.” In ALT. Springer International Publishing, 2014: 125-139.
[2] 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.