Experimental Materials for "Büchi Automata as Specifications for Reactive Systems"

This document includes links to the experimental tools employed in "Büchi Automata as Specifications for Reactive Systems." For details of the tools and file formats, please see Appendix B in the dissertation.

• Rank: the Rank-based Büchi Universality and Containment Solver. Based on the mh tool from Laurent Doyen and Jean-François Raskin.
• Ramsey: the Ramsey-based Büchi Containment Solver. Based on the sct/scp tool from Amir Ben-Amram and Chin Soon Lee.
• dk: a tool for the generation of Tabakov-Vardi random automata. Written by Deian Tabakov.
• sctp: a general Büchi automata manipulation tool, used to convert between various file formats. Based on the reference size-change termination analysis tool from Neil D. Jones, Amir Ben-Amram, and Chin-Soon Lee.
• Subsumption NuSMV: a version of NuSMV that, when used to check the universality of NFA, allows the use of subsumption. Based on NuSMV 2.5.0. For more recent versions and documentation, please visit the main NuSMV site.