Oliver Friedmann Ph.D. Student

Lehrstuhl für Theoretische Informatik
Institut für Informatik
Ludwig-Maximilians-Universität München
Oettingenstraße 67
D-80538 München

E-Mail:     O l i v e r . F r i e d m a n n [at] googlemail com

Mathematical Logics, Modal and Temporal Logics, Applications of Game Theory in Logics, Automata Theory, Complexity Theory, Programming Language Design, Distributed OOP systems.

• O. Friedmann: The Stevens-Stirling-Algorithm For Solving Parity Games Locally Requires Exponential Time; accepted for publication in IJFCS, 2009 [Preprint]
  
  
• O. Friedmann, M. Lange: A Solver for Modal Fixpoint Logics; accepted for publication in M4M-6, 2009 [Preprint, Slides]
  
  
• O. Friedmann, M. Lange: Solving Parity Games in Practice; accepted for publication in ATVA, 2009 [Preprint, Slides]
  
  
• O. Friedmann: An Exponential Lower Bound for the Parity Game Strategy Improvement Algorithm as We Know it; accepted for publication in LICS, 2009; winner of the Kleene Award [Preprint, Slides]

• O. Friedmann, M. Lange, M. Latte: An Effective Calculus of Infinite Proofs for the Full Computation Tree Logic [Preprint]
  
  
• O. Friedmann: Recursive Solving of Parity Games requires Exponential Time [Preprint]
  

• O. Friedmann: Parity Game Strategy Improvement SAT Benchmarks (see below for more details); used in the crafted category of the SAT competition, 2009
  

• MLSolver
  The MLSolver library is a collection of algorithms for solving the satisfiability and validity problems for modal fixpoint logics. It also defines a standard specification format for transition systems, a macro language for defining families of formulas and provides a collection of benchmark problems. Co-developer is Martin Lange.
  
  
• PGSolver
  The PGSolver library is a collection of algorithms for solving parity games that appear somewhere in the literature, as well as some new heuristics etc. It also defines a standard specification format for parity games as well as winning regions and strategies, and provides a collection of benchmark games. Co-developer is Martin Lange.
  
  
• SAT Benchmarks stemming from an analysis of parity games
  These benchmarks originate from my research investigating the structure of parity games that are found to be tough to solve for the standard strategy improvement algorithm. All following downloads are distributed under the BSD license.
  The generator is written in OCaml. You will therefore need an OCaml compiler to produce an executable. Additionally you can download precompiled binary executables for 32-bit Windows and Linux. Finally there is a pregenerated package of benchmarks that can be obtained as well.
  If you want to generate difficult sat-instances using the generator by yourself, I suggest to combine the command line arguments "-pp -ce -ci -n X -i Y", where X should be a natural number greater than 5 and lower than 10 (the higher, the harder...) and Y should also be a natural number near X.
  • Ocaml-Sources: stratimprsat.ml
  • Win32-Binary: stratimprsat_win32.exe
  • Linux32-Binary: stratimprsat_linux32
  • Pregenerated benchmarks: pregenerated_instances.zip

• Oliver Friedmann
  A Proof System for CTL*_μ [PDF, Talk]
  Diploma Thesis, University of Munich, 2008
  Supervised by Prof. Dr. Martin Hofmann and Prof. Dr. Martin Lange
  The prototype implementation that was available before is now subsumed by the publicly available MLSolver and PGSolver platforms.
  
  
• Oliver Friedmann
  A Proof System for the Modal μ-Calculus [PDF, Talk]
  Project Thesis, University of Munich, 2006
  Supervised by Prof. Dr. Martin Lange and Prof. Dr. Martin Hofmann
  The prototype implementation that was available before is now subsumed by the publicly available MLSolver and PGSolver platforms.

• Winter term 2007 / 2008
  Übungen zu Einführung in die Informatik
  Betreuung des Programmierpraktikums
  
  
• Summer term 2007
  Übungen zu Informatik 2
  
  
• Winter term 2006 / 2007
  Übungen zu Informatik 1
  

• Summer term 2005
  Extension of the XChange core engine and contributions to XCerpt in the context of the Rewerse project under the supervision of Dr. Paula-Lavinia Pătrânjan.

• December 2004
  Common memory manager without shared memory, Manipulation of the class hierarchy and Memory allocation within foreign processes (all in German) in Toolbox Magazine 6 / 04, pages 93 - 96
  
  
• September 2003
  Transparency for Delphi's components (in German) in Toolbox Magazine 5 / 03, pages 78 - 81