Table of Contents
Tools
RABIT and Reduce v2.5.1 (updated 25.9.2024)
RABIT stands for Ramsey-based Buchi automata inclusion testing. It can check language inclusion between Buchi automata, and thus also language equivalence and language universality. Since version 2.0, the main techniques used to prove inclusion are generalized simulation relations (see our POPL 2013 and LMCS 2019 papers listed below), and the Ramsey method is mainly used to find counterexamples in cases where inclusion does not hold.
RABIT has been extended to handle finite-word automata (NFA) as well. It can check language inclusion between NFA, and thus also language equivalence and language universality.
Reduce is a tool for minimizing Buchi automata (default) and NFAs (with option -finite).
The tools share some code, and are implemented in JAVA, compatible with Sun's JRE with version ≥ 1.7
Complete package containing RABIT v2.5.1 and Reduce v2.5.1 source code, executable and examples.
Earlier versions: RABIT 2.5.0, 2.4.5 2.3, 2.2, 2.1 and 2.0
An earlier version: RABIT v1.1 (now obsolete)
The tool is implemented in JAVA and is compatible with Sun's JRE with version ≥ 1.6.
The BA format
The input of the RABIT and Reduce tools is in the BA format, which is also supported by the GOAL tool. A BA file stores a classic alphabet-based finite automaton (with transition labels, not predicates). The automaton can either be interpreted as a Buchi automaton, or as an NFA. The format of a BA file is as follows.
(initial state) ... transitions ... (accepting states)
A BA file consists of three parts in the following order: the initial state, the transitions, and the accepting states (all in separate lines). If the initial state is omitted, the source state of the first transition is assumed to be the initial state. If the accepting states are omitted, it is assumed that all states are accepting. States are described by their names, which can be any string that does not contain any of the special characters “,” “-” “>”. A transition is of the form “label,source state→destination state.” The label can be any string not containing a special character. The following is the content of an example BA file:
[1] a,[1]->[2] b,[2]->[1] c,[1]->[3] [2] [3]
This BA file describes a Büchi automaton that has [1] as the initial state, [2] and [3] as accepting states, a transition from [1] to [2] over the symbol a, and a transition from [2] to [1] over the symbol b, and a transition from [1] to [3] over the symbol c. The brackets [] are part of the state names and do not have any semantic meaning (and they could be omitted). Here you can find examples of BA files.