Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
ramseysimsub [2019/04/30 04:34] rmayr [References] |
ramseysimsub [2023/07/05 20:42] (current) |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | ====== Buchi Automata: Ramsey-based Approach Using Simulation Subsumption ====== | + | ====== Buchi Automata ====== |
| - | Our tool is called RABIT (Ramsey-based Buchi automata Inclusion Testing). | + | Here are some current tools for checking language inclusion of nondeterministic Buchi automata. |
| - | It implements a generalized version of the Ramsey-based method for Buchi automata | + | |
| - | inclusion checking with additional subsumption techniques using backward and forward | + | |
| - | simulation preorder. The latest version of the tool additionally uses generalized automata | + | |
| - | minimization techniques using good approximations of multipebble simulations and trace | + | |
| - | inclusions (see the POPL 2013 paper listed below). | + | |
| - | - [[tools|Most recent version of the RABIT tool.]] | + | * [[http://goal.im.ntu.edu.tw|GOAL tool.]] There are many other methods for checking Buchi automata inclusion/equivalence, e.g., Safra-based constructions, Muller-Schupp constructions, Safra-Pieteman construction, and Slice-based constructions. The GOAL tool implements many of these. On most instances RABIT performs better than GOAL, and thus it can solve much larger instances. |
| - | - [[http://languageinclusion.org/CONCUR2011|Slightly older tools and experiments of CONCUR 2011.]] | + | * [[https://github.com/Mazzocchi/FORKLIFT | FORKLIFT.]] It uses a subsumption-based technique, different from the Ramsey-based method. See [[https://doi.org/10.1007/978-3-031-13188-2_6 | CAV'22 paper]] and [[https://arxiv.org/abs/2207.13549 | the full version of the paper]] and [[https://github.com/parof/buchi-automata-benchmark | some benchmarks]]. The older [[https://github.com/parof/bait | BAIT tool]] by same authors uses similar methods, see [[https://doi.org/10.4230/LIPIcs.CONCUR.2021.3 | CONCUR 2021 paper]]. |
| - | - [[http://languageinclusion.org/CAV2010|Very old experiments of CAV 2010]] | + | * [[tools | RABIT (Ramsey-based Buchi automata Inclusion Testing).]] It implements a generalized version of the Ramsey-based method for Buchi automata inclusion checking with additional subsumption techniques using backward and forward simulation preorder. Newer versions of the tool additionally use generalized automata minimization techniques using good approximations of multipebble simulations and trace inclusions (see the LMCS 2019 on the RABIT tool page). |
| - | There are many other methods for checking Buchi automata inclusion/equivalence, | + | Note: Subsumption-based techniques and simulation-based techniques are very different from each other. Thus the performance of the above tools can vary a lot between different (classes of) instances. I.e., instances that are hard for one tool may be easy for another, and vice-versa. So you might want to try out different tools, to see what works best for your particular automata. |
| - | e.g., Safra-based constructions, Muller-Schupp constructions, Safra-Pieteman construction, | + | |
| - | and Slice-based constructions. These are implemented in the | + | |
| - | [[http://goal.im.ntu.edu.tw|GOAL tool.]] | + | |
| - | However, our experiments indicate that RABIT performs much better and can solve much larger | + | |
| - | instances than the methods implemented in GOAL. | + | |
| - | + | ||
| - | ====== People ====== | + | |
| - | + | ||
| - | {{:parosh-abdulla.jpg?nolink|Parosh Aziz Abdulla}}{{:yufang-chen.jpg?nolink|Yu-Fang Chen}}{{:lorenzo-clemente.jpg?nolink|Lorenzo Clemente}} | + | |
| - | + | ||
| - | {{:lukas-holik.jpg?nolink|Lukas Holik}}{{:chihduo-hong.jpg?nolink|Chih-Duo Hong}}{{:richard-mayr.jpg?nolink|Richard Mayr}}{{:tomas-vojnar.jpg?nolink|Tomas Vojnar}} | + | |
| - | + | ||
| - | ====== References ====== | + | |
| - | *[[https://lmcs.episciences.org/5189 | Richard Mayr, Lorenzo Clemente. Efficient reduction of nondeterministic automata with application to language inclusion testing. Logical Methods in Computer Science 15(1). 2019.]] | + | |
| - | *[[http://www.inf.ed.ac.uk/publications/report/1414.html | Richard Mayr, Lorenzo Clemente. Advanced Automata Minimization. POPL 2013. Extended Technical Report EDI-INF-RR-1414.]] | + | |
| - | *[[http://homepages.inf.ed.ac.uk/rmayr/tr-absim.pdf | Richard Mayr, Parosh Aziz Abdulla, Yu-Fang Chen, Lorenzo Clemente, Lukás Holik, Chih-Duo Hong and Tomas Vojnar. Advanced Ramsey-based Buchi Automata Inclusion Testing. CONCUR 2011, volume 6901 in LNCS. 2011.]] | + | |
| - | * [[http://www.fit.vutbr.cz/units/UITS/pubs/tr.php?id=9207 | Parosh Aziz Abdulla, Yu-Fang Chen, Lorenzo Clemente, Lukás Holík, Chih-Duo Hong, Richard Mayr, Tomás Vojnar: Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing. CAV 2010: 132-147]] | + | |