Convert LTL Rabin omega automata to HOA data types
https://www.isa-afp.org/browser_info/current/AFP/LTL_to_DRA/DTS.html
-
convert arbitrary states and atomic propositions to nat -
define mapping from transition sets to markers -
convert transition letters to HOA labels -
convert Rabin acceptance to HOA representation -
define conversion between runs -
proof acceptance equivalence