User Tools

Site Tools


start

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

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 -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  -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...");		

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.

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.

start.txt · Last modified: 2017/04/29 00:32 by wanderduck