Links und Funktionen
Sprachumschaltung

Navigationspfad
Sie sind hier: Startseite / Lehre / WS 2018/19 / Oberseminar / Sabine Bauer: Decidable inequalities over infinite trees; Jakob Zanker: Automatisches Finden von Faltungscodierern mit SAT-Solvern


Inhaltsbereich

Sabine Bauer: Decidable inequalities over infinite trees; Jakob Zanker: Automatisches Finden von Faltungscodierern mit SAT-Solvern

Oberseminarvortrag von Sabine Bauer über Decidable inequalities over infinite trees; sowie Jakob Zanker über Automatisches Finden von Faltungscodierern mit SAT-Solvern
Wann 14:30 16:00 09.11.2018
von bis
Wo Raum L109, Oettingenstr. 67
Termin übernehmen vCal
iCal

Es spricht Sabine Bauer über:
Decidable inequalities over infinite trees

Abstract:
I will practice my talk at LPAR-22. The paper that Steffen and me will
publish there has the title "Decidable inequalities over infinite
trees" and the following abstract:

Linear tree constraints are given by pointwise linear inequalities
between infinite trees labeled with nonnegative rational numbers.
Satisfiablity of such constraints is at least as hard as solving the
Skolem-Mahler-Lech Problem. We provide an interesting subcase, for
which we prove that satisfiablity is decidable. Our decision procedure
is based on intricate arguments using automata and combinatorics of
words. Our subcase allows to construct an inference mechanism for
resource bounds of object oriented Java-like programs: actual resource
bounds can be read off from solutions of tree constraints. So far,
only the case of degenerated tree constraints (i.e. lists) was known
to be decidable which, however, is insufficient to generally solve the
given resource analysis problem. The present paper therefore provides
a generalisation to trees of higher degree in order to cover the
entire range of constraints encountered by resource analysis.


sowie Jakob Zanker über:
Automatisches Finden von Faltungscodierern mit SAT-Solvern

Abstract:
Für die Konstruktion von Faltungscodes gibt es bislang kein
systematisches Verfahren. Geeignete Schaltpläne für Faltungscodierer
wurden in den 80er Jahren durch exhaustive Suche vor allem von der
NASA gefunden. In dieser Arbeit wird ein Verfahren vorgestellt, mit
welchem sich automati- siert Schaltpläne für Faltungscodes finden
lassen. Hierzu wird das ursprüngliche Suchproblem in ein
Erfüllbarkeitsproblem für aussagenlogische Formeln transformiert.
Das vorgestellte Verfahren wurde in JAVA implementiert und getestet.
Die Ergebnisse und Grenzen des Verfahrens werden diskutiert.

Artikelaktionen


Funktionsleiste