Tradeoffs in Controller Synthesis (TriCS)

Project Description

• Principal Investigator: Martin Zimmermann
• Scientific Assistant: Alexander Weinert
• Funding: DFG research grant
• Funding Period: 2015-2018

Project Goals

The goal of this project is to increase the applicability of automated controller synthesis and to improve the quality of synthesized controllers by developing techniques to analyze tradeoffs between optimization criteria like size and quality of the controller, and by developing algorithms to compute controllers that are optimal with respect to more than one of these criteria. According to the state of the art there are two diverging approaches to synthesis: compute controllers within the upper bounds on memory requirements, but disregarding semantic quality, or to compute optimal controllers, which are much larger than the upper bounds. This raises the question whether there is a tradeoff between size and quality: are optimal controllers necessarily larger than generic ones?

Publications

• Quantitative Reductions and Vertex-Ranked Games
  Alexander Weinert. GandALF 2018

• Finite-state Strategies in Delay Games
  Sarah Winter and Martin Zimmermann. arXiv.

• Visibly Linear Dynamic Logic
  Alexander Weinert and Martin Zimmermann. TCS 747.

• Synthesizing Optimally Resilient Controllers
  Daniel Neider, Alexander Weinert, and Martin Zimmermann, CSL 2018.

• Parity Games with Weights
  Sven Schewe, Alexander Weinert, and Martin Zimmermann, CSL 2018.

• Parity to Safety in Polynomial Time for Pushdown and Collapsible Pushdown Systems
  Matthew Hague, Roland Meyer, Sebastian Muskalla, and Martin Zimmermann, MFCS 2018.

• Team Semantics for the Specification and Verification of Hyperproperties
  Andreas Krebs, Arne Meier, Jonni Virtema, and Martin Zimmermann, MFCS 2018.

• The Complexity of Counting Models of Linear-time Temporal Logic
  Hazem Torfah and Martin Zimmermann, Acta Informatica 55(3).

• Parameterized Linear Temporal Logics Meet Costs: Still not Costlier than LTL
  Martin Zimmermann, Acta Informatica 55(2).

• Distributed Synthesis for Parameterized Temporal Logics
  Swen Jacobs, Leander Tentrup, and Martin Zimmermann, accepted for publication in Information and Computation.

• Easy to Win, Hard to Master: Optimal Strategies in Parity Games with Costs
  Alexander Weinert and Martin Zimmermann, LMCS 13(3).

• Finite-state Strategies in Delay Games
  Martin Zimmermann, GandALF 2017.

• VLDL Satisfiability and Model Checking via Tree Automata
  Alexander Weinert, FSTTCS 2017

• Quantitative Reductions and Vertex-Ranked Infinite Games
  Alexander Weinert, arXiv.

• Games with Costs and Delays
  Martin Zimmermann, LICS 2017.

• Parametric Linear Dynamic Logic
  Peter Faymonville and Martin Zimmermann, Information and Computation 253(2).

• Bounding Average-energy Games
  Patricia Bouyer, Piotr Hofman, Nicolas Markey, Mickael Randour and Martin Zimmermann, FoSSaCS 2017.

• The First-Order Logic of Hyperproperties
  Bernd Finkbeiner and Martin Zimmermann, STACS 2017.

• Prompt Delay
  Felix Klein and Martin Zimmermann, FSTTCS 2016.

• Visibly Linear Dynamic Logic
  Alexander Weinert and Martin Zimmermann, FSTTCS 2016.

• Delay Games with WMSO+U winning conditions
  Martin Zimmermann, RAIRO-ITA 50(2)

• Limit your Consumption! Finding Bounds in Average-energy Games
  Kim G. Larsen, Simon Laursen, and Martin Zimmermann, QAPL 2016

• Approximating Optimal Bounds in Prompt-LTL Realizability in Doubly-exponential Time
  Leander Tentrup, Alexander Weinert, and Martin Zimmermann, GandALF 2016.

• Distributed PROMPT-LTL Synthesis
  Swen Jacobs, Leander Tentrup, and Martin Zimmermann, GandALF 2016.

• The Complexity of Counting Models of Linear-time Temporal Logic
  Hazem Torfah and Martin Zimmermann. Acta Informatica, article in press.

• Parameterized Linear Temporal Logics Meet Costs: Still not Costlier than LTL
  Martin Zimmermann. Acta Informatica, article in press.

• How Much Lookahead is Needed to Win Infinite Games?
  Felix Klein and Martin Zimmermann, LMCS 12(3).

• Easy to Win, Hard to Master: Optimal Strategies in Parity Games with Costs
  Alexander Weinert and Martin Zimmermann, CSL 2016.

• Optimal Strategy Synthesis for Request-Response Games
  Florian Horn, Wolfgang Thomas, Nico Wallmeier, and Martin Zimmermann, RAIRO-ITA 49(3).

• Parameterized Linear Temporal Logics Meet Costs: Still not Costlier than LTL
  Martin Zimmermann, GandALF 2015.

• What are Strategies in Delay Games? Borel Determinacy for Games with Lookahead
  Felix Klein and Martin Zimmermann, CSL 2015.

• How much lookahead is needed to win infinite games?
  Felix Klein and Martin Zimmermann, ICALP 2015.

• Delay Games with WMSO+U Winning Conditions
  Martin Zimmermann, CSR 2015.