The rtl2ba tool translates formulas of the linear-time temporal logic RTL into Büchi automata. The prominent linear-time logic LTL and the linear-time cores of the IEEE standardized logics SVA, and PSL are fragments of RTL. The output of rtl2ba can be used in the symblic model checker NuSMV. For further information see the README.TXT file in the package.
These details are provided for information only. No information here is legal advice and should not be used as such.