Differences
This shows you the differences between two versions of the page.
Both sides previous revisionPrevious revision | |||
tools [2020/05/31 19:09] – [Earlier versions: RABIT v2.3 v2.2 v2.1 and 2.0] rmayr | tools [2025/05/28 08:45] (current) – external edit 127.0.0.1 | ||
---|---|---|---|
Line 1: | Line 1: | ||
======Tools====== | ======Tools====== | ||
- | ====RABIT and Reduce v2.5==== | + | ====RABIT and Reduce v2.5.1 (updated 25.9.2024)==== |
RABIT stands for Ramsey-based Buchi automata inclusion testing. | 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. | 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 paper listed below), and the Ramsey method is mainly used to find counterexamples in cases where inclusion does not hold. | + | Since version 2.0, the main techniques used to prove inclusion are generalized simulation relations (see our POPL 2013 and LMCS 2019 papers |
RABIT has been extended to handle finite-word automata (NFA) as well. | RABIT has been extended to handle finite-word automata (NFA) as well. | ||
Line 13: | Line 13: | ||
The tools share some code, and are implemented in JAVA, compatible with Sun's JRE with version **≥ 1.7** | The tools share some code, and are implemented in JAVA, compatible with Sun's JRE with version **≥ 1.7** | ||
- | {{:rabit250.tar.gz|Complete package containing RABIT v2.5.0 and Reduce v2.5.0 source code, executable and examples.}} | + | {{:rabit251.tar.gz|Complete package containing RABIT v2.5.1 and Reduce v2.5.1 source code, executable and examples.}} |
- | ====Earlier versions: RABIT v2.4.5 v2.3 v2.2 v2.1 and 2.0 ==== | + | ====Earlier versions: RABIT 2.5.0, 2.4.5 2.3, 2.2, 2.1 and 2.0 ==== |
+ | {{: | ||
{{: | {{: | ||
{{: | {{: |