LIRA
| Beteiligte Mitarbeiter | Beschreibung | Publikationen
|
| ehemalige Mitarbeiter Lehrstuhl für Rechnerarchitektur | |
| Jochen Eisinger, Dr. | Entwickler |
| Lehrstuhl für Rechnerarchitektur | |
| Bernd Becker, Prof. Dr. | Kontakt |
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.
|
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 |