Efficient monitoring of ω-languages

Marcelo D'Amorim, Grigore Roşu

Research output: Contribution to journalConference articlepeer-review


We present a technique for generating efficient monitors for ω-regular-languages. We show how Büchi 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 ω-regular-language. The presented technique is implemented as part of a larger monitoring framework and is available for download.

Original languageEnglish (US)
Pages (from-to)364-378
Number of pages15
JournalLecture Notes in Computer Science
StatePublished - 2005
Event17th International Conference on Computer Aided Verification, CAV 2005 - Edinburgh, Scotland, United Kingdom
Duration: Jul 6 2005Jul 10 2005

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Efficient monitoring of ω-languages'. Together they form a unique fingerprint.

Cite this