Efficient Monitoring of Omega-Languages

From FSL
Jump to: navigation, search

Marcelo d'Amorim and Grigore Rosu
CAV'05, LNCS 3576, pp 364 - 378. 2005.
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.
PDF, LNCS, CAV'05, DBLP, BIB

Personal tools
Namespaces

Variants
Actions
Navigation