ASHWANI ANAND

When a system sends messages through a lossy channel, then the language encoding all sequences of messages can be abstracted by its downward closure, i.e. the set of all (not necessarily contiguous) subwords. This is useful because even if the system has infinitely many states, its downward closure is a regular language. However, if the channel has congestion control based on priorities assigned to the messages, then we need a finer abstraction: The downward closure with respect to the priority embedding. As for subword-based downward closures, one can also show that these priority downward closures are always regular. While computing finite automata for the subword-based downward closure is well understood, nothing is known in the case of priorities. We initiate the study of this problem and provide algorithms to compute priority downward closures for regular languages, one-counter languages, and context-free languages.

This paper presents a new method to automatically compute permissive strategies and permissive assumptions in 𝜔-regular two-player games on graphs to enable strategy adaptation both during synthesis and execution of distributed symbolic controllers.

We present a novel method to compute permissive winning strategies in two-player games over finite graphs with ω-regular winning conditions. Given a game graph G and a parity winning condition Φ, we compute a winning strategy template Ψ that collects an infinite num- ber of winning strategies for objective Φ in a concise data structure. We use this new representation of sets of winning strategies to tackle two problems arising from applications of two-player games in the context of cyber-physical system design – (i) incremental synthesis, i.e., adapt- ing strategies to newly arriving, additional ω-regular objectives Φ' , and (ii) fault-tolerant control, i.e., adapting strategies to the occasional or persistent unavailability of actuators. The main features of our strat- egy templates – which we utilize for solving these challenges – are their easy computability, adaptability, and compositionality. For incremental synthesis, we empirically show on a large set of benchmarks that our technique vastly outperforms existing approaches if the number of added specifications increases. While our method is not complete, our prototype implementation returns the full winning region in all 1400 benchmark in- stances, i.e. handling a large problem class efficiently in practice.

We solve the problem of automatically computing a new class of environment assumptions in two-player turn-based finite graph games which characterize an ``adequate cooperation'' needed from the environment to allow the system player to win. Given an $\omega$-regular winning condition $\Phi$ for the system player, we compute an $\omega$-regular assumption $\Psi$ for the environment player, such that (i) every environment strategy compliant with $\Psi$ allows the system to fulfill $\Phi$ (sufficiency), (ii) $\Psi$ can be fulfilled by the environment for every strategy of the system (implementability), and (iii) $\Psi$ does not prevent any cooperative strategy choice (permissiveness).

For parity games, which are canonical representations of $\omega$-regular games, we present a polynomial-time algorithm for the symbolic computation of \emph{adequately permissive assumptions} and show that our algorithm runs faster and produces better assumptions than existing approaches---both theoretically and empirically. To the best of our knowledge, for \emph{$\omega$-regular} games, we provide the first algorithm to compute sufficient and implementable environment assumptions that are also \emph{permissive}.

The notion of separating automata was introduced by Bojanczyk and Czerwinski for understanding the first quasipolynomial time algorithm for parity games. In this paper we show that separating automata is a powerful tool for constructing algorithms solving games with combinations of objectives. We construct two new algorithms: the first for disjunctions of parity and mean payoff objectives, matching the best known complexity, and the second for disjunctions of mean payoff objectives, improving on the state of the art. In both cases the algorithms are obtained through the construction of small separating automata, using as black boxes the existing constructions for parity objectives and for mean payoff objectives.