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 language | English (US) |
|---|---|
| Pages (from-to) | 364-378 |
| Number of pages | 15 |
| Journal | Lecture Notes in Computer Science |
| Volume | 3576 |
| DOIs | |
| State | Published - 2005 |
| Event | 17th International Conference on Computer Aided Verification, CAV 2005 - Edinburgh, Scotland, United Kingdom Duration: Jul 6 2005 → Jul 10 2005 |
ASJC Scopus subject areas
- Theoretical Computer Science
- General Computer Science
Fingerprint
Dive into the research topics of 'Efficient monitoring of ω-languages'. Together they form a unique fingerprint.Cite this
- APA
- Standard
- Harvard
- Vancouver
- Author
- BIBTEX
- RIS