Polynomielle Systeme über Semiringen: Grundlagen, Algorithmen, Anwendungen

• Antragsteller: Professor Dr. Javier Esparza
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2011 bis 2014
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 192404487

• Erstellungsjahr: 2015

Zusammenfassung der Projektergebnisse

Das Newton-Verfahren ist eines der ältesten und bekanntesten, aber zugleich auch erfolgreichsten Verfahren, um Nullstellen nichtlinearer Funktionen über den reellen oder komplexen Zahlen in mehreren Veränderlichen zu approximieren oder in Spezialfällen sogar zu bestimmen. In Vorarbeiten hatten die Antragsteller bereits gezeigt, dass das Newton-Verfahren auch zur Lösung von nichtlinearen Fixpunktgleichungen, genauer polynomieller (auch: algebraischer) Gleichungssystem, über allgemeineren algebraischen Strukturen, sogenannten (w-stetigen) Semiringen, angewendet werden kann und damit neue Anwendungsbereiche wie formale Sprachen und die Verifikation von Programmen erschlossen. Im Rahmen dieses Projekts sollten die Anwendungsbereiche weiter untersucht werden. Hierzu sollte eine entsprechende Implementierung entwickelt werden. Des Weiteren sollte das Konvergenzverhalten des Newton-Verfahrens fur Semiringe im Allgemeinen und für konkrete Klassen von Semiringen im Besonderen weiter untersucht werden. Bezüglich dieser Aufgabenstellung haben wir folgende Fortschritte erzielt: • Implementierung: Entwicklung von FPsolve, einem generischen Löser für algebraische Systeme über Semiringen mit verschiedenen Techniken zur Minimierung Symbolischer Lösungen. • Provenance: Sowohl neue theoretische Ergebnisse als auch Anwendungen der in FPsolve verwendeten Techniken im Bereich der Provenance-Berechnung für Datalog-Anfragen. • Konvergenzgeschwindigkeit: Verallgemeinerung und Verschärfung des Konvergenzresultats von kommutativen idempotenten auf allgemeine kommutative Semiringe. • Theorie: Darstellung des Newton-Verfahrens ohne Differenzen für allgemeine Semiringe, womit eine der größten Hürden der Vorarbeiten behoben wurde. • Anwendung natürliche Sprachverarbeitung: Techniken zur Beschleunigung des Parsens natürlicher Sprache. • Anwendung Programmanalyse: Mehrparameteranalyse der Komplexität des Verifikationsproblems für nebenläufige Programme mit Prozeduren. • Theorie und Anwendung: Lösen von linearen Gleichungssystemen über Semiringen auf Grafikkarten im Spezialfall von Paritätsspielen. • Theorie: Neue Algorithmen für die Lüosung von algebraischen Systemen über Semiringen für spezielle Semiring-Klassen.

Projektbezogene Publikationen (Auswahl)

• “Complexity of pattern-based verification for multithreaded programs”. In: Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011. 2011, pp. 499– 510
  Javier Esparza and Pierre Ganty
  
• “Solving Fixed-Point Equations by Derivation Tree Analysis”. In: Algebra and Coalgebra in Computer Science - 4th International Conference, CALCO 2011, Winchester, UK, August 30 - September 2, 2011. Proceedings. 2011, pp. 19–35
  Javier Esparza and Michael Luttenberger
  
• “Convergence of Newton’s Method over Commutative Semirings”. In: Language and Automata Theory and Applications - 7th International Conference, LATA 2013, Bilbao, Spain, April 2-5, 2013. Proceedings. 2013, pp. 407–418
  Michael Luttenberger and Maximilian Schlund
  
• “Putting Newton into Practice: A Solver for Polynomial Equations over Semirings”. In: Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings. 2013, pp. 727–734
  Maximilian Schlund, Michal Terepeta, and Michael Luttenberger
  
• “Solving Parity Games on the GPU”. In: Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15-18, 2013. Proceedings. 2013, pp. 455–459
  Philipp Hoffmann and Michael Luttenberger
  
• “A Brief History of Strahler Numbers”. In: Language and Automata Theory and Applications - 8th International Conference, LATA 2014, Madrid, Spain, March 10-14, 2014. Proceedings. 2014, pp. 1–13
  Javier Esparza, Michael Luttenberger, and Maximilian Schlund
  
• “Fast and Accurate Unlexicalized Parsing via Structural Annotations”. In: Proceedings of the 14th Conference of the European Chapter of the Association for Computational Linguistics, EACL 2014, April 26-30, 2014, Gothenburg, Sweden. 2014, pp. 164–168
  Maximilian Schlund, Michael Luttenberger, and Javier Esparza
  
• “FPsolve: A Generic Solver for Fixpoint Equations over Semirings”. In: Implementation and Application of Automata - 19th International Conference, CIAA 2014, Giessen, Germany, July 30 - August 2, 2014. Proceedings. 2014, pp. 1–15
  Javier Esparza, Michael Luttenberger, and Maximilian Schlund
  
• “Pattern-Based Verification for Multithreaded Programs”. In: ACM Trans. Program. Lang. Syst. 36.3 (2014), p. 9
  Javier Esparza, Pierre Ganty, and Tomás Poch
  
• “Regular Expressions for Provenance”. In: 6th Workshop on the Theory and Practice of Provenance, TaPP’14, Cologne, Germany, June 12-13, 2014
  Michael Luttenberger and Maximilian Schlund
  
• “Finite Automata for the Sub- and Superword Closure of CFLs: Descriptional and Computational Complexity”. In: Language and Automata Theory and Applications - 9th International Conference, LATA 2015. 2015, pp. 473– 485
  Georg Bachmeier, Michael Luttenberger, and Maximilian Schlund
  
• Convergence of Newton’s Method over Commutative Semirings. Information and Computation Volume 246, February 2016, Pages 43-61
  Michael Luttenberger and Maximilian Schlund