Martin Zimmermann

photo

Reactive Systems Group
Universität des Saarlandes
eMail: zimmermann at react.uni-saarland.de

This page is no longer updated. Please visit my new web page at Aalborg University.

About me | News | Teaching | Research | Events | Publications | Presentations | CV

About me

I was a postdoc in the Reactive Systems Group at the Computer Science Department of Saarland University and the principal investigator of the DFG project TriCS, which studies tradeoffs in infinite games. A typical question that we aim to answer is: do strategies that satisfy the specification optimally have to be larger than strategies that just satisfy the specification?

Before coming to Saarbrücken, I was a postdoc at the Institute of Informatics of the University of Warsaw.

I did my PhD in Computer Science under the supervision of Wolfgang Thomas at RWTH Aachen University. Before that, I studied Computer Science, also at RWTH Aachen University. During this time, I was a Fulbright student at DePaul University in Chicago.

News

  • October 1st, 2018: I have moved to the University of Liverpool.
  • August 29th, 2018: New preprint with Daniel Neider and Alexander Weinert combining robustness, quantitative features, and increased expressiveness in linear temporal logics.
  • August 7th, 2018: New preprint on robust monitoring with Corto Mascle, Daniel Neider, Maximilian Schwenger, Paulo Tabuada and Alexander Weinert.
  • June 15th, 2018: The journal version of the paper introducing VLDL has been accepted for publication at TCS.
  • June 15th, 2018: Two papers accepted at CSL 2018: the work with Daniel Neider and Alexander Weinert on computing optimally resilient controllers in a setting with unmodeled disturbances and the work with Sven Schewe and Alexander Weinert on relations between quantitative variants of parity games.
  • June 13th, 2018: Two papers accepted at MFCS 2018: The work with Andreas Krebs, Arne Meier, and Jonni Virtema on team semantics for LTL and the work with Matthew Hague, Roland Meyer and Sebastian Muskalla showing that parity games on higher-order pushdown systems can be turned into safety games on higher-order pushdown systems with only a polynomial blowup.
  • May 9th, 2018: New preprint with Matthew Hague, Roland Meyer and Sebastian Muskalla showing that parity games on higher-order pushdown systems can be turned into safety games on higher-order pushdown systems with only a polynomial blowup. This work was inspired by a result by Wladimir Fridman and me showing how to turn pushdown parity games into finite safety games.
  • April 18th, 2018: New preprint with Sven Schewe and Alexander Weinert on relations between quantitative variants of parity games.
  • January 19th, 2018: I am organizing and co-chairing GandALF 2018 in Saarbrücken. Please consider submitting your papers.
  • January 9th, 2018: Joint work with Swen Jacobs and Leander Tentrup on the distributed synthesis for parametric temporal logics has been accepted to the special issue of Information and Computation dedicated to GandALF 2016.
  • September 26th, 2017: New preprint with Andreas Krebs, Arne Meier, and Jonni Virtema introducing team semantics for LTL to specify hyperproperties.
  • September 15th, 2017: New preprint with Daniel Neider and Alexander Weinert: we show how to compute optimally resilient controllers in a setting with unmodeled disturbances.
  • September 1st, 2017: Together with Swen Jacobs I will teach an advanced course on Reactive Synthesis during the upcoming winter term.
  • August 25th, 2017: The journal version of the paper on playing finitary parity games optimally has been accepted for publication at LMCS.
  • August 25th, 2017: The paper on finite-state strategies in delay games has been accepted for presentation at GandALF 2017.
  • May 2nd, 2017: New preprint on finite-state strategies in delay games. Presents also a very general framework for solving delay games and for determining upper bounds on the necessary lookahead.
  • March 22nd, 2017: My paper on delay games with costs has been accepted for publication at LICS 2017.
  • January 10th, 2017: New preprint demonstrating the usefulness of delay in quantitative games: not only allows it to win more games, but also to improve the quality of strategies in games you win without delay.
  • December 22nd, 2016: Our paper on average-energy games has been accepted for publication at FOSSACS 2017.
  • December 12th, 2016: Joint paper with Bernd Finkbeiner presenting the first-order logic of hyperproperties accepted for publication at STACS 2017.
  • October 26th, 2016: Together with Patricia Bouyer, Piotr Hofman, Nicolas Markey, and Mickael Randour, I proved that average-energy games with only a lower bound on the energy level are decidable. A preprint can be found on the arXiv. Coincidentally, preliminary work with Kim G. Larsen and Simon Laursen on this problem appeared today in the post-proceedings of QAPL 2016.
  • October 17th, 2016: Uploaded a new preprint to the arXiv presenting a first-order logic capturing HyperLTL. Also, models of HyperLTL are rather not well-behaved.
  • October 10th, 2016: Invited to the FSTTCS Workshop AVeRTS.
  • September 16th, 2016: Two papers accepted for presentation at FSTTCS 2016 introducing Visibly Linear Dynamic Logic (joint work with Alexander Weinert) and settling the complexity of delay games with Prompt-LTL winning conditions (joint work with Felix Klein).
  • August 29th, 2016: The full version of the CSR 2015 paper on delay games with WMSO+U winning conditions has been accepted for publication at RAIRO ITA.
  • August 1st, 2016: The full version of the FSTTCS 2014 paper with Hazem Torfah on the complexity of counting models of LTL is accepted for publication at Acta Informatica.
  • July 8th, 2016: Two papers on synthesis for Prompt-LTL specifications have been accepted for publication at GandALF 2016 presenting an approximation algorithm for Prompt-LTL synthesis (with Leander Tentrup and Alexander Weinert) and a study of distributed Prompt-LTL synthesis (with Swen Jacobs and Leander Tentrup).
  • June 12th, 2016: I will present Visibly Linear Dynamic Logic at the Highlights Conference 2016.
  • June 11th, 2016: A paper with Alexander Weinert showing that playing finitary parity games and parity games with costs optimally is harder than just winning them is accepted for publication at CSL 2016.

Teaching

Supervision

Research

The red thread of my research is turning synthesis from a decision problem into an optimization problem by studying quantitative winning conditions, by extending qualitative conditions into quantitative ones, and by developing algorithms to compute optimal winning strategies.

Oftentimes, optimal strategies have substantially larger memory requirements than arbitrary winning strategies. In the project TriCS, I investigate whether such tradeoffs are avoidable or whether playing optimally comes at a price.

Furthermore, I am interested in the theory of asynchronous strategies for infinite games: in a delay game, one of the players may delay her moves to obtain an advantage on her opponent’s moves.

Projects

Events

Publications

Theses

Selected Presentations

  • Finite-state Strategies in Delay Games: Slides
    GandALF 2017, Rome, Italy, September 2017
  • Easy to Win, Hard to Master: Playing Parity Games with Costs Optimally: Slides
    University of Liverpool, Liverpool, United Kingdom, September 2017
  • Games with Costs and Delays: Slides
    LICS 2017, Reykjavik, Iceland, June 2017
  • The First-order Logic of Hyperproperties: Slides
    STACS 2017, Hannover, Germany, March 2017
  • Easy to Win, Hard to Master: Playing Parity Games with Costs Optimally: Slides
    AVeRTS 2016, Chennai, India, December 2016
  • Approximating Optimal Bounds in Prompt-LTL Realizability in Doubly-exponential Time: Slides
    GandALF 2016, Catania, Italy, September 2016
  • Limit Your Consumption! Finding Bounds in Average-energy Games: Slides
    QAPL 2016, Eindhoven, Netherlands, April 2016
  • Approximating Optimal Bounds in Prompt-LTL Realizability in Doubly-exponential Time: Slides
    QAPL 2016, Eindhoven, Netherlands, April 2016
  • Parameterized Linear Temporal Logics Meet Costs: Still not Costlier than LTL: Slides
    GandALF 2015, Genova, Italy, September 2015
  • What are Strategies in Delay Games? Borel Determinacy for Games with Lookahead: Slides
    CSL 2015, Berlin, Germany, September 2015
  • Delay Games with WMSO+U Winning Conditions: Slides
    CSR 2015, Listvyanka, Russia, July 2015
  • The Complexity of Counting Models of Linear-time Temporal Logic: Slides
    AlgoSyn Seminar, RWTH Aachen University, Aachen, Germany, January 2015
  • Cost-Parity and Cost-Streett Games: Slides
    AlgoSyn Seminar, RWTH Aachen University, Aachen, Germany, November 2012
  • Playing Pushdown Parity Games in a Hurry: Slides
    GandALF 2012, Naples, Italy, September 2012
  • Down the Borel Hierarchy: Solving Muller Games via Safety Games: Slides
    Gasics Meeting, Brussels, Belgium, November 2011
  • Degrees of Lookahead in Context-free Infinite Games: Slides
    Gasics Meeting, Mons, Belgium, May 2011
  • Time-optimal Strategies for Infinite Games: Slides
    DIMAP Seminar, University of Warwick, Coventry, United Kingdom, March 2010
  • Parametric LTL Games: Slides
    AlMoTh 2010, Frankfurt am Main, Germany, February 2010
  • Time-optimal Winning Strategies for Poset Games: Slides
    CIAA 2009, Sydney, Australia, July 2009
  • Time-optimal Winning Strategies in Infinite Games: Slides
    Gasics Meeting, Brussels, Belgium, March 2009

Curriculum Vitae

pdf