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

I was 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

  • August 1st, 2021: I have moved to Aalborg University.
  • June 29th, 2021: Two papers accepted for presentation at MFCS 2021: Joint work with Marie Fortin, Louwe B. Kuijer, and Patrick Totzke on satisfiability for hyperlogics and with Shibashis Guha, Ismaël Jecker, and Karoliina Lehtinen on good-for-games pushdown automata.
  • June 21st, 2021: Highlights of Logic, Games and Automata: Satya Prakash Nayak will present adaptive strategies for rLTL Games, Marie Fortin will present complexity results for satisfiability of hyperlogics and I will present succinctness results for good-for-games pushdown automata.
  • May 11th, 2021: New preprint with Marie Fortin, Louwe B. Kuijer, and Patrick Totzke settling the complexity of satisfiability for HyperLTL and HyperCTL*. Spoiler: Both are highly undecidable.
  • May 7th, 2021: New preprint with Shibashis Guha, Ismaël Jecker, and Karoliina Lehtinen continuing the investigation of good-for-games pushdown automata presenting, among other expressiveness and succinctness results, the first separation between deterministic and good-for-games automata on finite words.
  • March 19th, 2021: I will organize the 2022 edition of the MOVEP summer school. More information to follow.
  • February 22nd, 2021: Satya Prakash Nayak will present a poster on the synthesis of adaptive controllers from Robust LTL at HSCC 2021. The results were obtained as part of his Master's thesis prepared under the supervision of Daniel Neider and me.
  • October 23rd, 2020: New preprint showing that the minimal lookahead necessary to win an ω-regular delay game can be approximated in exponential time, the first improvement over the trivial exact algorithm with doubly-exponential running time.
  • August 6th, 2020: Joint work with Aniello Murano and Sasha Rubin on optimal strategies in quantiative Büchi games accepted for publication at GandALF 2020.
  • July 7th, 2020: Joint work with Daniel Neider and Patrick Totzke studying resilient strategies in pushdown safety games accepted at MFCS 2020.
  • April 16th, 2020: Joint work with Karoliina Lehtinen introduing good-for-games pushdown automata accepted at LICS 2020.
  • February 18th, 2020: The Department of Computer Science of the University of Liverpool offers four fully funded PhD positions. If you are interested in doing a PhD under my supervision, please contact me (martin.zimmermann liverpool.ac.uk). Application deadline is April 1st, 2020.
  • January 14th,2020: New preprint with Karoliina Lehtinen introduing good-for-games pushdown automata, which recognize a new class of contextfree languages for which solving games is decidable.
  • January 2nd, 2020: Our work on monitoring of robust LTL got accepted for presentation at HSCC 2020. Joint work with Corto Mascle, Daniel Neider, Maximilian Schwenger, Paulo Tabuada and Alexander Weinert.
  • December 11th, 2019: New preprint on resilient strategies in pushdown safety games with Daniel Neider and Patrick Totzke generalizing previous work on resilient strategies in games on finite arenas.
  • November 11th, 2019: Joint work with Swen Jacobs and Mouhammad Sakr on cutoff results for parameterized systems and quantitaive specifications has been acccepted at VMCAI 2020.
  • October 3rd, 2019: Joint work with Corto Mascle on fragments of HyperLTL with deciable satisfiability has been accepted at CSL 2020.
  • 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.
  • 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.
  • 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 CANVAS.

At Saarland University

Supervision

Events

Publications

Under Submission

  • From LTL to rLTL Monitoring: Improved Monitorability through Robust Semantics (journal version) pdf
    Joint work with Corto Mascle, Daniel Neider, Maximilian Schwenger, Paulo Tabuada and Alexander Weinert. arXiv
  • Good-for-games ω-Pushdown Automata (journal version) pdf
    Joint work with Karoliina Lehtinen. arXiv
  • Approximating the Minimal Lookahead Needed to Win Infinite Games pdf
    arXiv
  • Robust, Expressive, and Quantitative Linear Temporal Logics: Pick any Two for Free (journal version) pdf
    Joint work with Daniel Neider and Alexander Weinert. arXiv

Journal Papers

Conference Papers

  • HyperLTL Satisfiability is \(\Sigma_1^1\)-complete, HyperCTL* Satisfiability is \(\Sigma_1^2\)-completepdf
    Joint work with Marie Fortin, Louwe B. Kuijer, and Patrick Totzke. Accepted for publication at MFCS 2021 (arXiv)
  • A Bit of Nondeterminism Makes Pushdown Automata Expressive and Succinct pdf
    Joint work with Shibashis Guha, Ismaël Jecker, and Karoliina Lehtinen. Accepted for publication at MFCS 2021 (arXiv)
  • Optimal Strategies in Weighted Limit Gamespdf
    Joint work with Aniello Murano and Sasha Rubin. GandALF 2020
  • Optimally Resilient Strategies in Pushdown Safety Games pdf
    Joint work with Daniel Neider and Patrick Totzke. MFCS 2020
  • Good-for-games ω-Pushdown Automata pdf
    Joint work with Karoliina Lehtinen. LICS 2020
  • 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. HSCC 2020
  • Promptness and Bounded Fairness in Concurrent and Parameterized Systems pdf
    Joint work with Swen Jacobs and Mouhammad Sakr. VMCAI 2020
  • The Keys to Decidable HyperLTL Satisfiability: Small Models or Very Simple Formulas pdf
    Joint work with Corto Mascle. CSL 2020
  • Robust, Expressive, and Quantitative Linear Temporal Logics: Pick any Two for Free pdf
    Joint work with Daniel Neider and Alexander Weinert. 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

Posters

  • Adaptive strategies for rLTL gamespdf
    Joint work with Satya Prakash Nayak and Daniel Neider. HSCC 2021

Theses

Selected Presentations

  • Optimal Strategies in Weighted Limit Gamespdfvideo
    GandALF 2020, online, September 2020
  • Optimally Resilient Strategies in Pushdown Safety Gamespdf
    Highlights Conference 2020, online, September 2020
  • Optimally Resilient Strategies in Pushdown Safety Gamespdfvideo
    MFCS 2020, online, August 2020
  • Temporal Logics for Information-flow Policiespdf
    Royal Holloway, London, January 2020
  • 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: July 2021 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