Forschung

Automaten-basierte Verifikation

In der Logik der ersten Stufe über gemischter ganzzahliger und reellwertiger Addition, d.h. über der Struktur (ℝ, ℤ, +, <), lassen sich einige Klassen interessanter Systeme beschreiben. Darunter fallen sogenannte lineare hybride Automaten, also Systeme die sowohl aus digitalen als auch aus analogen Komponenten bestehen. Die Analyse solcher Systeme erfordert eine effiziente Entscheidungsprozedur für die Logik, in der die Systeme modelliert sind.

Wir entscheiden diese Logik mit Hilfe von Automaten, indem wir Automaten konstruieren, die alle erfüllenden Belegungen darstellen. Da die binäre Darstellung reeller Zahlen unendlich lang ist, verwenden wir Automaten über unendlichen sogenannten ω-Wörtern. Man kann zeigen, dass schwache deterministische Büchi Automaten ausreichen, um solche Teilmengen von ℝⁿ zu beschreiben, die in der Logik über (ℝ, ℤ, +, <) beschreibbar sind.

zur Homepage der FOL(ℝ, ℤ, +, <) Bibliothek