Uni-Logo
English       Login
Rechnerarchitektur
        Startseite         |         Institut für Informatik         |         Technische Fakultät
 

LIRA

| Beteiligte Mitarbeiter | Beschreibung | Publikationen |


Beteiligte Mitarbeiter

ehemalige Mitarbeiter Lehrstuhl für Rechnerarchitektur
Jochen Eisinger, Dr. Entwickler
Lehrstuhl für Rechnerarchitektur
Bernd Becker, Prof. Dr. Kontakt


Beschreibung

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. Man kann diese Logik mit Hilfe von Automaten entscheiden, die alle erfüllenden Belegungen darstellen. Da die binäre Darstellung reeller Zahlen unendlich lang ist, werden Automaten über unendlichen sogenannten ω-Wörtern verwendet. Die Bibliothek LIRA dient zur effizienten Darstellung und Manipulation solcher Automaten.

LIRA wird nicht mehr weiterentwickelt. Weitere Details sind unter http://lira.gforge.avacs.org/ zu finden.



Publikationen
Jochen Eisinger, Felix Klaedtke
Don't care words with an application to the automata-based approach for real addition
18th International Conference on Computer Aided Verification. LNCS 4144. pp 67-80. Springer-Verlag, 2006
Bernd Becker, Christian Dax, Jochen Eisinger, Felix Klaedtke
LIRA: Handling Constraints of Linear Arithmetics over the Integers and the Reals
19th International Conference on Computer Aided Verification. LNCS 4590. pp 312-315. Springer-Verlag, 2007
Christian Dax, Jochen Eisinger, Felix Klaedtke
Mechanizing the Powerset Construction for Restricted Classes of ω-Automata
5th International Symposium on Automated Technology for Verification and Analysis. LNCS 4762. pp 223-236. Springer-Verlag, 2007