I am an associate professor at the Distributed, Embedded and Intelligent Systems research group of the Department of Computer Science at Aalborg University. My main research interests are on temporal logics, the reactive synthesis problem, and automata theory.
Before arriving in Aalborg, I was a lecturer at the Department of Computer Science at the University of Liverpool. Even before that, I spent postdocs at the Reactive Systems Group at Saarland University and 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 28th, 2024: Joint work with Hadar Frenkel showing that second-order HyperLTL satisfiability and model-checking are very, very hard has been accepted at CSL 2025.
  • August 26th, 2024: Work on monitoring of real-time systems under assumptions with Alessandro Cimatti, Thomas M. Grosen, Kim G. Larsen, and Stefano Tonetta has been accepted at SEFM 2024.
  • August 6th, 2024: Work on monitoring of real-time systems under delayed observations with Martin Fränzle, Thomas M. Grosen, and Kim G. Larsen has been accepted at iFM 2024.
  • August 5th, 2024: The work robustifying Probabilistic CTL for free has been accepted at Information Processing Letters.
  • July 29th, 2024: Joint work with Christian Schilling on reachability for neural-network controllers accepted in the prost-proceedings of AISOLA 2023.
  • July 29th, 2024: Joint work with Sean Kauffman and Kim G. Larsen on data-free Nfer accepted at RV 2024.
  • May 3rd, 2024: I have joined the PC of LAMAS&SR 2024, co-located with KR24. Submit your papers by July 17th.
  • April 30th, 2024: New preprint on computing effective Skolem functions for HyperLTL: Imperfect-information multi-player games with lookahead do the trick. Joint work with Sarah Winter.
  • April 30th, 2024: New preprint on monitoring of real-time systems under delayed observations. Joint work with Martin Fränzle, Thomas M. Grosen, and Kim G. Larsen.
  • February 26th, 2024: The journal version of our rCTL paper has been accepted for publication in the special issue of Innovations of Systems and Software Engineering decidated to NFM 2022. Joint work with Satya Prakash Nayak, Daniel Neider and Rajarshi Roy.
  • February 26th, 2024: I have joined the PC of GandALF 2024. Prepare your papers now, the conference takes place early this year.
  • November 28th, 2023: New preprint showing that second-order HyperLTL satisfiability and model-checking are very, very hard.
  • November 28th, 2023: The journal version our MFCS 2021 paper studying history-deterministic pushdown automata on finite words has been accepted for publication in LMCS. Joint work with Shibashis Guha, Ismaël Jecker, and Karoliina Lehtinen.
  • August 16th, 2023: The full version of the TASE 2022 paper settling the complexity of nfer has been accepted to the Science of Computer Programming special issue dedicated to the conference. Joint work with Sean Kauffman.
  • August 11th, 2023: Joint work with Martin Fränzle and Sarah Winter comparing two notions of delay in infinite games has been accepted at GandALF 2023.
  • July 12th, 2023: Joint work with Aniello Murano and Daniel Neider on robust alternating temporal logics has been accepted at JELIA 2023.
  • June 28th, 2023: Joint work with Enzo Erlich, Shibashis Guha, Ismaël Jecker, and Karoliina Lehtinen on history-deterministic Parikh automata and related models has been accepted at CONCUR 2023.
  • June 12th, 2023: New preprint showing that Probabilistic CTL can be robustified for free.
  • June 1st, 2023: New preprint with Martin Fränzle and Sarah Winter comparing two notions of delay in infinite games, which turn out to be more closely related than expected.
  • April 30th, 2023: I will give an invited lecture on synthesis of infinite-state systems at the Reactive synthesis: Main Achievements and current trends - Third edition of the UNIVR/UNIUD summer school on formal methods for cyber-physical systems in Udine.
  • March 31st, 2023: I joined the PC of CSL 2024. Submit your paper by July 31st.
  • March 27th, 2023: I joined the PC of EUMAS 2023. Submit your paper by May 20th.
  • February 15th, 2023: I joined the PC of MFCS 2023. Submit your papers by April 28th, 2023.
  • January 26th, 2023: I joined the PC of GandALF 2023. Submit your papers by June 23rd, 2023.
  • November 17th, 2022: I joined the PC of CONCUR 2023, part of Confest 2023. Submit your papers by May 2nd, 2023.
  • October 14th, 2022: I finally updated and uploaded the lecture notes on Infinite Games, joint work with Felix Klein and Alexander Weinert. In case of questions, errors, or suggestions for improvements please send an email. Thank you to everybody who has used the notes for their teaching or has reported issues.
  • September 23rd, 2022: Joint work with Sarah Winter showing that delay games with weak Muller conditions are hard has been accepted for publication in the post-proceedings of the IMS workshop Automata Theory and Applications: Games, Learning and Structures.
  • September 19th, 2022: Joint work with Shibashis Guha, Ismaël Jecker, and Karoliina Lehtinen on Parikh automata over infinite words accepted for publication at FSTTCS 2022.
  • September 16th, 2022: New preprint with Enzo Erlich, Shibashis Guha, Ismaël Jecker, and Karoliina Lehtinen on history-deterministic Parikh automata and related models. Some of the results were obtained during Enzo's internship in Aalborg.
  • September 5th, 2022: New preprint with Shibashis Guha, Ismaël Jecker, and Karoliina Lehtinen introducing and studying Parikh automata over infinite words.
  • July 11th, 2022: The journal version of our rLTL monitoring paper is accepted for publication in Formal Methods of System Design. Joint work with many co-authors.
  • June 30th, 2022: New preprint revisiting the monoitoring of timed properties, with divergence, uncertainty, and predictions. Joint work with Thomas Møller Grosen, Sean Kauffman and Kim G. Larsen.
  • Unpinned: I am organizing MOVEP 2022, a five-day summer school on modelling and verification of parallel processes, in Aalborg. We have an amazing lineup of invited speakers and there will be a student session. Please come visit us and participate.
  • May 30th, 2022: I am a PC member for OVERLAY 2022 in Udine. Deadline for paper submission is September 30th.
  • April 26th, 2022: How do you play against a not necessarily antogonistic opponent in a quantitative world? Exploit bad moves of the opponent and give him the chance to make bad moves: New preprint with Satya Prakash Nayak and Daniel Neider.
  • April 19th, 2022: Joint work with Sean Kauffman analyzing the complexity of the nfer evaluation problem accepted for publication at TASE 2022.
  • March 15th, 2022: Robust CTL will be presented at NFM 2022. Joint work with Satya Prakash Nayak, Daniel Neider and Rajarshi Roy.
  • March 8th, 2022: The first step towards showing that Muller delay games are harder than parity delay games: weak Muller delay games are harder than parity delay games. Joint work with Sarah Winter.
  • March 1st, 2022: New preprint with Sean Kauffman evaluating the complexity of nfer.
  • January 26th, 2022: New preprint with Satya Prakash Nayak, Daniel Neider and Rajarshi Roy introducing Robust Computation Tree Logic.
  • January 4th, 2022: I am a PC member for CSL 2023 in Warsaw. Please consider submitting your papers.
  • August 1st, 2021: I joined the Distributed, Embedded and Intelligent Systems research group at 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 quantitative 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 Aalborg University

All teaching materials can be found on Moodle.

At University of Liverpool

Lecture COMP313 "Formal Methods" (taught thrice).

At Saarland University

Supervision

Lecture Notes

Events

Publications

Under Submission

  • History-deterministic Parikh Automata (journal version) pdf
    Joint work with Enzo Erlich, Mario Grobler, Shibashis Guha, Ismaël Jecker, and Karoliina Lehtinen. arXiv
  • Synchronous Team Semantics for Temporal Logicspdf
    Joint work with Andreas Krebs, Arne Meier, and Jonni Virtema. arXiv
  • Tracy, Traces, and Transducers: Computable Counterexamples and Explanations for HyperLTL Model-Checkingpdf
    Joint work with Sarah Winter. arXiv
  • On the Existence of Reactive Strategies Resilient to Delaypdf
    Joint work with Martin Fränzle, Paul Kröger, and Sarah Winter. arXiv
  • HyperLTL Satisfiability is Highly Undecidable, HyperCTL* is Even Harderpdf
    Joint work with Marie Fortin, Louwe B. Kuijer, and Patrick Totzke. arXiv

Journal Papers

Conference Papers

  • The Complexity of Second-order HyperLTLpdf
    Joint work with Hadar Frenkel. Accepted for publication at CSL 2025 (arXiv).
  • Exploiting Assumptions for Effective Monitoring of Real-Time Properties under Partial Observabilitypdf
    Joint work with Alessandro Cimatti, Thomas M. Grosen, Kim G. Larsen, and Stefano Tonetta. SEFM 2024.
  • Monitoring Real-Time Systems under Parametric Delaypdf
    Joint work with Martin Fränzle, Thomas M. Grosen, and Kim G. Larsen. iFM 2024.
  • The Reachability Problem for Neural-Network Control Systemspdf
    Joint work with Christian Schilling. AISOLA 2023.
  • The Complexity of Data-Free Nferpdf
    Joint work with Sean Kauffman and Kim G. Larsen. RV 2024
  • Strategies Resilient to Delay: Games under Delayed Control vs. Delay Gamespdf
    Joint work with Martin Fränzle and Sarah Winter. GandALF 2023
  • Robust Alternating-time Temporal Logicspdf
    Joint work with Aniello Murano and Daniel Neider. JELIA 2023
  • History-deterministic Parikh Automata pdf
    Joint work with Enzo Erlich, Shibashis Guha, Ismaël Jecker, and Karoliina Lehtinen. CONCUR 2023
  • Weak Muller Conditions Make Delay Games Hard pdf
    Joint work with Sarah Winter. IMS workshop Automata Theory and Applications: Games, Learning and Structures 2021
  • Parikh Automata over Infinite Words pdf
    Joint work with Shibashis Guha, Ismaël Jecker, and Karoliina Lehtinen. FSTTCS 2022
  • Robustness-by-Construction Synthesis: Adapting to the Environment at Runtime pdf
    Joint work with Satya Prakash Nayak and Daniel Neider. ISOLA 2022
  • Monitoring Timed Properties (Revisited) pdf
    Joint work with Thomas Møller Grosen, Sean Kauffman and Kim G. Larsen. FORMATS 2022
  • The Complexity of Evaluating nfer pdf
    Joint work with Sean Kauffman. TASE 2022
  • Robust Computation Tree Logic pdf
    Joint work with Satya Prakash Nayak, Daniel Neider and Rajarshi Roy. NFM 2022
  • 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. MFCS 2021
  • A Bit of Nondeterminism Makes Pushdown Automata Expressive and Succinct pdf
    Joint work with Shibashis Guha, Ismaël Jecker, and Karoliina Lehtinen. MFCS 2021 (Best Paper Award)
  • 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

  • History-deterministic Pushdown Automatapdf
    IRIF, Paris, July 2024
  • Synthesis of Infinite-state Systemspdf
    Reactive synthesis: Main Achievements and current trends - Third edition of the UNIVR/UNIUD summer school on formal methods for cyber-physical systems, September 2023
  • Logics for Hyperpropertiespdf
    Reactive synthesis: Main Achievements and current trends - Third edition of the UNIVR/UNIUD summer school on formal methods for cyber-physical systems, September 2023
  • Temporal Logics for the Specification of Hyperpropertiespdf
    NetVAS 2022, Bertinoro, October 2022
  • On Parikh Automata: Infinite Words, Games, and History-determinismpdfvideo
    Highlights Conference 2022, online, July 2022
  • How Undecidable are HyperLTL and HyperCTL*?pdf
    Highlights Conference 2021, online, September 2021
  • A Bit of Nondeterminism Makes Pushdown Automata Expressive and Succinctpdf
    Highlights Conference 2021, online, September 2021
  • 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
  • Distributed PROMPT-LTL Synthesis 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: October 2024 pdf

Contact

Email

mzi cs.aau.dk

Office

Room 1.2.06
Cassiopeia
Selma Lagerløfs Vej 300
9220 Aalborg

Phone

+45 9940 8770

Mail

Aalborg University
Department of Computer Science
Selma Lagerløfs Vej 300
9220 Aalborg
Denmark