LO2: Automata-theoretic foundations for probabilistic synthesis

In synthesis of finite-state systems from temporal logic specifications, we consider finite-state programs (like circuits or controllers) that transform a stream of input signals into a stream of output signals. The task is to automatically construct such a program from a given specification, for example a formula in temporal logic, that describes the allowed input–output behaviors of the system. In the classical setting of an antagonistic environment, algorithms based on games and tree automata have been developed, and the problem is well-understood. In synthesis for probabilistic systems, the environment chooses the input signals randomly, and the goal is to synthesise a program that, for example, satisfies the specification almost surely or with positive probability. While some aspects of this probabilistic synthesis problem have been analysed, a systematic study based on the corresponding models of tree automata with randomisation and stochastic games is missing.

The synthesis problem for probabilistic environments is studied for the temporal logics LTL and CTL used as specification languages. The developed methods are based on tree automata with classical semantics, and the desired probabilistic meaning is captured by ad hoc modifications of the automata and games. Tree automata (on infinite trees) with a probabilistic semantics are studied, where two variations of the semantics are investigated. The first one defines a run as accepting if almost all paths are accepting (the set of rejecting branches has probability zero), and the second one requires almost all runs to be accepting. The algorithmic methods developed for the second model are based on partially observable Markov decision processes (POMDPs).

The goal of this dissertation project is to develop a solid foundation of automata and game-theoretic methods for synthesis in probabilistic environments. Its main objectives are:

  • Develop a complete theory of probabilistic automata on infinite trees, considering different types of acceptance conditions, and non-deterministic and alternating automata, compare the resulting language classes, and analyse the algorithmic and closure properties of the different automata models.
  • Develop game-theoretic methods, in particular for partially observable stochastic games, to deal with algorithmic questions for probabilistic tree automata.
  • Use the automata and game-theoretic methods to develop a clean framework for dealing with the synthesis questions from logical specifications in probabilistic environments.