Efficient Monitoring of Omega-Languages
- Abstract. We present a technique for generating efficient monitors for Omega-regular-languages. We show how Buchi automata can be reduced in size and transformed into special, statistically optimal nondeterministic finite state machines, called binary transition tree finite state machines (BTT-FSMs), which recognize precisely the minimal bad prefixes of the original Omega-regular-language. The presented technique is implemented as part of a larger monitoring framework and is available for download.