Efficient monitoring of ω-languages

Marcelo D'Amorim, Grigore Rosu

Research output: Contribution to journalConference article

Abstract

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
Volume3576
StatePublished - Oct 19 2005
Event17th International Conference on Computer Aided Verification, CAV 2005 - Edinburgh, Scotland, United Kingdom
Duration: Jul 6 2005Jul 10 2005

    Fingerprint

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this