rltl2ba Translator from Regular Linear Temporal Logic (RLTL) formulas into Büchi Automata TODO Allow the LET expression to define global identifiers.