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

Formal languages
Regular Languages
Finite automata
State Machine
Monitoring
Prefix
Automata
Monitor
Binary
Language
Framework

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Efficient monitoring of ω-languages. / D'Amorim, Marcelo; Rosu, Grigore.

In: Lecture Notes in Computer Science, Vol. 3576, 19.10.2005, p. 364-378.

Research output: Contribution to journalConference article

D'Amorim, Marcelo ; Rosu, Grigore. / Efficient monitoring of ω-languages. In: Lecture Notes in Computer Science. 2005 ; Vol. 3576. pp. 364-378.
@article{23d9c2779d8c437d96bc77c6f566c220,
title = "Efficient monitoring of ω-languages",
abstract = "We present a technique for generating efficient monitors for ω-regular-languages. We show how B{\"u}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.",
author = "Marcelo D'Amorim and Grigore Rosu",
year = "2005",
month = "10",
day = "19",
language = "English (US)",
volume = "3576",
pages = "364--378",
journal = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
issn = "0302-9743",
publisher = "Springer Verlag",

}

TY - JOUR

T1 - Efficient monitoring of ω-languages

AU - D'Amorim, Marcelo

AU - Rosu, Grigore

PY - 2005/10/19

Y1 - 2005/10/19

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=26444539487&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=26444539487&partnerID=8YFLogxK

M3 - Conference article

AN - SCOPUS:26444539487

VL - 3576

SP - 364

EP - 378

JO - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SN - 0302-9743

ER -