I am a lecturer at the Department of Computer Science at the University of Liverpool working in the Verification Group. The red thread of my research is turning reactive synthesis from a decision problem into an optimization problem by studying quantitative winning conditions, by turning qualitative conditions into quantitative ones, and by developing algorithms to compute optimal winning strategies. This also includes work on quantitative variants of temporal logics, the standard formalism for specifying such winning conditions.
I spent postdocs at the Reactive Systems Group at Saarland University and at the Institute of Informatics of the University of Warsaw. Between 2015 and 2018, I was the principal investigator of the DFG project TriCS, which studied tradeoffs in infinite games. For example, we showed that strategies that satisfy a quantitative specification optimally may have to be larger than strategies that just satisfy the specification.
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

  • March 25th, 2019: Open PhD scholarship associated with the EPSRC-funded project "quantMD" on ontology-based management of many-dimensional quantitative data lead by Boris Konev, Frank Wolter and myself. Please see this advert for details. The topic of the PhD project is rather flexible and covers, in particular, (quantitative) temporal logics. If you are interested, please contact me.
  • July 3rd, 2019: The work with Daniel Neider and Alexander Weinert on combining robustness, quantitative features and increased expressiveness in linear temporal logics has been accepted at GandALF 2019.
  • June 30th, 2019: Joint work with Daniel Neider and Alexander Weinert on synthesizing resilient controllers has been accepted to a special issue of Acta Informatica on synthesis.
  • June 20th, 2019: Joint work with Sven Schewe and Alexander Weinert on quantitative parity games has been accepted to the special issue of LMCS dedicated to CSL 2018.
  • April 9th, 2019: I am a PC member for GandALF 2019 in Bordeaux. Please consider submitting your papers.
  • December 18th, 2018: The Department of Computer Science at the University of Liverpool is offering two fully funded PhD positions. If you are interested in doing a PhD with me, contact me and mention me in your application. Deadline is Friday, March 1st, 2019.
  • December 14th, 2018: Alexander Weinert has sucessfully defended his PhD thesis. Congratulations!
  • October 25th, 2018: The journal version of the paper on finite-state strategies has been accepted for publication in Information and Computation. It presents, amongst the results of the conference version, new results on tradeoffs between delay and memory, obtained in collaboration with Sarah Winter.
  • October 1st, 2018: I 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 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. Joint work with Bernd Finkbeiner.
  • 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

At University of Liverpool

I am the module coordinator for COMP313 Formal Methods. All learning material can be found on VITAL.

At Saarland University

Supervision

Publications

Under Submission

  • The Keys to Decidable HyperLTL Satisfiability: Small Models or Very Simple Formulas pdf
    Joint work with Corto Mascle. arXiv
  • From LTL to rLTL Monitoring: Improved Monitorability through Robust Semantics pdf
    Joint work with Corto Mascle, Daniel Neider, Maximilian Schwenger, Paulo Tabuada and Alexander Weinert. arXiv

Journal Papers

Conference Papers

  • Robust, Expressive, and Quantitative Linear Temporal Logics: Pick any Two for Free pdf
    Joint work with Daniel Neider and Alexander Weinert. arXiv (to appear at GandALF 2019)
  • Synthesizing Optimally Resilient Controllers pdf
    Joint work with Daniel Neider and Alexander Weinert. CSL 2018
  • Parity Games with Weights pdf
    Joint work with Sven Schewe and Alexander Weinert. CSL 2018
  • Team Semantics for the Specification and Verification of Hyperproperties pdf
    Joint work with Andreas Krebs, Arne Meier and Jonni Virtema. MFCS 2018
  • Parity to Safety in Polynomial Time for Pushdown and Collapsible Pushdown Systems pdf
    Joint work with Matthew Hague, Roland Meyer and Sebastian Muskalla. MFCS 2018
  • Finite-state Strategies in Delay Games pdf
    GandALF 2017
  • Games with Costs and Delays pdf
    LICS 2017
  • Bounding Average-energy Games pdf
    Joint work with Patricia Bouyer, Piotr Hofman, Nicolas Markey and Mickael Randour. FoSSaCS 2017
  • The First-Order Logic of Hyperproperties pdf
    Joint work with Bernd Finkbeiner. STACS 2017
  • Prompt Delay pdf
    Joint work with Felix Klein. FSTTCS 2016
  • Visibly Linear Dynamic Logic pdf
    Joint work with Alexander Weinert. FSTTCS 2016
  • Limit your Consumption! Finding Bounds in Average-energy Games pdf
    Joint work with Kim G. Larsen and Simon Laursen. QAPL 2016
  • Distributed PROMPT-LTL Synthesis pdf
    Joint work with Swen Jacobs and Leander Tentrup. GandALF 2016
  • Approximating Optimal Bounds in Prompt-LTL Realizability in Doubly-exponential Time pdf
    Joint work with Leander Tentrup and Alexander Weinert. GandALF 2016
  • Easy to Win, Hard to Master: Optimal Strategies in Parity Games with Costs pdf
    Joint work with Alexander Weinert. CSL 2016
  • Parameterized Linear Temporal Logics Meet Costs: Still not Costlier than LTL pdf
    GandALF 2015
  • What are Strategies in Delay Games? Borel Determinacy for Games with Lookahead pdf
    Joint work with Felix Klein. CSL 2015
  • How much lookahead is needed to win infinite games? pdf
    Joint work with Felix Klein. ICALP 2015
  • Delay Games with WMSO+U Winning Conditions pdf
    CSR 2015
  • The Complexity of Counting Models of Linear-time Temporal Logic pdf
    Joint work with Hazem Torfah. FSTTCS 2014
  • Parametric Linear Dynamic Logic pdf
    Joint work with Peter Faymonville. GandALF 2014
  • Cost-Parity and Cost-Streett Games pdf
    Joint work with Nathanaël Fijalkow. FSTTCS 2012
  • Down the Borel Hierarchy: Solving Muller Games via Safety Games pdf
    Joint work with Daniel Neider and Roman Rabinovich. GandALF 2012
  • Playing Pushdown Parity Games in a Hurry pdf
    Joint work with Wladimir Fridman. GandALF 2012
  • Degrees of Lookahead in Context-free Infinite Games pdf
    Joint work with Wladimir Fridman and Christof Löding. CSL 2011
  • Optimal Bounds in Parametric LTL Games pdf
    GandALF 2011
  • Playing Muller Games in a Hurry pdf
    Joint work with John Fearnley. GandALF 2010
  • Time-optimal Winning Strategies for Poset Games pdf
    CIAA 2009

Theses

Selected Presentations

  • Robust, Expressive, and Quantitative Linear Temporal Logics: Pick any Two for Free pdf
    GandALF 2019, Bordeaux, France, September 2019
  • Synthesizing Optimally Resilient Controllers pdf
    Highlights Conference 2018, Berlin, Germany, September 2018
  • Games Computer Scientists Play pdf
    Introductory Lecture, Saarland University, Saarbrücken, Germany, July 2018
  • Tradeoffs in Infinite Games pdf
    Scientific Colloquium in the Habilitation Process, Saarland University, Saarbrücken, Germany, May 2018
  • Delay Games pdf
    University of Naples “Federico II” , Naples, Italy, March 2018
  • Finite-state Strategies in Delay Games pdf
    GandALF 2017, Rome, Italy, September 2017
  • The First-order Logic of Hyperproperties pdf
    Highlights Conference 2017, London, UK, September 2017
  • Easy to Win, Hard to Master: Playing Parity Games with Costs Optimally pdf
    University of Liverpool, Liverpool, United Kingdom, September 2017
  • Games with Costs and Delays pdf
    LICS 2017, Reykjavik, Iceland, June 2017
  • Logics for Hyperproperties pdf
    Centre Fédéré en Vérification, Brussels, Belgium, May 2017
  • The First-order Logic of Hyperproperties pdf
    Leibniz University Hannover, Hannover, Germany, April 2017
  • The First-order Logic of Hyperproperties pdf
    STACS 2017, Hannover, Germany, March 2017
  • The First-order Logic of Hyperproperties pdf
    RWTH Aachen University, Aachen, Germany, March 2017
  • Easy to Win, Hard to Master: Playing Parity Games with Costs Optimally pdf
    AVeRTS 2016, Chennai, India, December 2016
  • Visibly Linear Dynamic Logic pdf
    FSTTCS 2016, Chennai, India, December 2016
  • Prompt Delay pdf
    FSTTCS 2016, Chennai, India, December 2016
  • Approximating Optimal Bounds in Prompt-LTL Realizability in Doubly-exponential Time pdf
    GandALF 2016, Catania, Italy, September 2016
  • Visibly Linear Dynamic Logic pdf
    Highlights Conference 2016, Brussels, Belgium, September 2016
  • Limit Your Consumption! Finding Bounds in Average-energy Games pdf
    QAPL 2016, Eindhoven, Netherlands, April 2016
  • Approximating Optimal Bounds in Prompt-LTL Realizability in Doubly-exponential Time pdf
    QAPL 2016, Eindhoven, Netherlands, April 2016
  • Parameterized Linear Temporal Logics Meet Costs: Still not Costlier than LTL pdf
    GandALF 2015, Genova, Italy, September 2015
  • Delay Games with WMSO+U Winning Conditions pdf
    Highlights Conference 2015, Prague, Czech Republic, September 2015
  • What are Strategies in Delay Games? Borel Determinacy for Games with Lookahead pdf
    CSL 2015, Berlin, Germany, September 2015
  • How Much Lookahead is Needed to Win Infinite Games? pdf
    Aalborg University, Aalborg, Denmark, August 2015
  • Delay Games with WMSO+U Winning Conditions pdf
    CSR 2015, Listvyanka, Russia, July 2015
  • Parametric Linear Temporal Logics pdf
    Aalborg University, Aalborg, Denmark, March 2015
  • Delay Games with WMSO+U Winning Conditions pdf
    AVACS Workshop 2015, Freiburg, Germany, March 2015
  • How Much Lookahead is Needed to Win Infinite Games? pdf
    Workshop Automata, Concurrency and Timed Systems, Chennai Mathematical Institute, Chennai, India, February 2015
  • Omega-regular and Max-regular Delay Games pdf
    Dagstuhl Seminar Non-Zero-Sum-Games and Control, Schloss Dagstuhl, Wadern, Germany, January 2015
  • The Complexity of Counting Models of Linear-time Temporal Logic pdf
    AlgoSyn Seminar, RWTH Aachen University, Aachen, Germany, January 2015
  • Infinite Games pdf
    Research Training Group SCARE, Oldenburg, Germany, October 2014
  • Optimal Strategy Synthesis for Request-Response Games pdf
    AVACS Workshop 2014, Saarbrücken, Germany, September 2014
  • The Complexity of Counting Models of Linear-time Temporal Logic pdf
    Highlights Conference 2014, Paris, France, September 2014
  • Reducing omega-regular Specifications to Safety Conditions pdf
    AVACS Workshop 2014, Oldenburg, Germany, March 2014
  • Optimal Bounds in Parametric LTL Games pdf
    AVACS Workshop 2013, Freiburg, Germany, October 2013
  • Cost-Parity and Cost-Streett Games pdf
    AlgoSyn Seminar, RWTH Aachen University, Aachen, Germany, November 2012
  • Playing Pushdown Parity Games in a Hurry pdf
    Games Workshop 2012, Naples, Italy, September 2012
  • Playing Pushdown Parity Games in a Hurry pdf
    GandALF 2012, Naples, Italy, September 2012
  • Playing Pushdown Parity Games in a Hurry pdf
    AISS 2012, Dubrovnik, Croatia, June 2012
  • Down the Borel Hierarchy: Solving Muller Games via Safety Games pdf
    LICS 2012, Dubrovnik, Croatia, June 2012
  • Solving Infinite Games with Bounds pdf
    Oberseminar Informatik, RWTH Aachen University, Germany, February 2012
  • Down the Borel Hierarchy: Solving Muller Games via Safety Games pdf
    Gasics Meeting, Brussels, Belgium, November 2011
  • Playing Infinite Games in Finite Time pdf
    AlgoSyn Workshop 2011, Kerkrade, Netherlands, November 2011
  • Degrees of Lookahead in Context-free Infinite Games pdf
    Games Workshop 2011, Paris, France, August 2011
  • Optimal Bounds in Parametric LTL Games pdf
    GandALF 2011, Minori, Italy, June 2011
  • Degrees of Lookahead in Context-free Infinite Games pdf
    Gasics Meeting, Mons, Belgium, May 2011
  • Degrees of Lookahead in Context-free Infinite Games pdf
    AlMoTh 2011, Leipzig, Germany, February 2011
  • Synthesis of Time-optimal Controllers pdf
    Computer Science Day 2010, RWTH Aachen University, Aachen, Germany, December 2010
  • Optimal Bounds in Parametric LTL Games pdf
    Gasics Meeting, Paris, France, November 2010
  • Playing Muller Games in a Hurry pdf
    Games Workshop 2010, Oxford, United Kingdom, September 2010
  • Playing Muller Games in a Hurry pdf
    MoVeP 2010, Aachen, Germany, June 2010
  • Playing Muller Games in a Hurry pdf
    GandALF 2010, Minori, Italy, June 2010
  • Playing Muller Games in a Hurry pdf
    Gasics Meeting, Aalborg, Denmark, May 2010
  • Time-optimal Strategies for Infinite Games pdf
    DIMAP Seminar, University of Warwick, Coventry, United Kingdom, March 2010
  • Parametric LTL Games pdf
    AlMoTh 2010, Frankfurt am Main, Germany, February 2010
  • Parametric LTL Games pdf
    Gasics Meeting, Aachen, Germany, October 2009
  • Prompt and Parametric LTL Games pdf
    Games Workshop 2009, Udine, Italy, September 2009
  • Time-optimal Winning Strategies for Poset Games pdf
    CIAA 2009, Sydney, Australia, July 2009
  • Time-optimal Winning Strategies in Infinite Games pdf
    Gasics Meeting, Brussels, Belgium, March 2009

CV

Last updated: January 2019 pdf

Contact

Email

martin.zimmermann liverpool.ac.uk

Office

George Holt Building, Room 201
Ashton Street
Liverpool

Phone

+44 151 795 8860

Mail

Department of Computer Science
University of Liverpool
Ashton Street
Liverpool L69 3BX
United Kingdom