Universal Safety Controllers (USCs) are a promising logical control framework that guarantees the satisfaction of a given temporal safety specification when applied to any realizable plant model. Unlike traditional methods, which synthesize one logical controller over a given detailed plant model, USC synthesis constructs a generic controller whose outputs are conditioned by plant behavior, called prophecies. Thereby, USCs offer strong generalization and scalability benefits over classical logical controllers. However, the exact computation and verification of prophecies remain computationally challenging. In this paper, we introduce an approximation algorithm for USC synthesis that addresses these limitations via learning. Instead of computing exact prophecies, which reason about sets of trees via automata, we only compute under- and over-approximations from (small) example plants and infer computation tree logic (CTL) formulas as representations of prophecies. The resulting USC generalizes to unseen plants via a verification step and offers improved efficiency and explainability through small and concise CTL prophecies, which remain human-readable and interpretable. Experimental results demonstrate that our learned prophecies remain generalizable, yet are significantly more compact and interpretable than their exact tree automata representations.

Two-player games on finite graphs provide a rigorous foundation for modeling the strategic interaction between reactive systems and their environment. While concurrent game semantics naturally capture the synchronous interactions characteristic of many cyber-physical systems (CPS), their adoption in CPS design remains limited. Building on the concept of permissive strategy templates (PeSTels) for turn-based games, we introduce concurrent (permissive) strategy templates (ConSTels) – a novel representation for sets of randomized winning strategies in concurrent games with Safety, Büchi, and Co-Büchi objectives. ConSTels compactly encode infinite families of strategies, thereby supporting both offline and online adaptation. Offline, we exploit compositionality to enable incremental synthesis: combining ConSTels for simpler objectives into non-conflicting templates for more complex combined objectives. Online, we demonstrate how ConSTels facilitate runtime adaptation, adjusting action probabilities in response to observed opponent behavior to optimize performance while preserving correctness. We implemented ConSTel synthesis and adaptation in a prototype tool and experimentally show its potential.

Abstract We examine two-player games over finite weighted graphs with quantitative (mean-payoff or energy) objective, where one of the players additionally needs to satisfy a fairness objective. The specific fairness we consider is called strong transition fairness, given by a subset of edges of one of the players, which asks the player to take fair edges infinitely often if their source nodes are visited infinitely often. We show that when fairness is imposed on player 1, these games fall within the class of previously studied $$\omega $$ ω -regular mean-payoff and energy games. On the other hand, when the fairness is on player 2, to the best of our knowledge, these games have not been previously studied. We provide gadget-based algorithms for fair mean-payoff games where fairness is imposed on either player, and for fair energy games where the fairness is imposed on player 1. For all variants of fair mean-payoff and fair energy (under unknown initial credit) games, we give pseudo-polynomial algorithms to compute the winning regions of both players. Additionally, we analyze the strategy complexities required for these games. Our work is the first to extend the study of strong transition fairness, as well as gadget-based approaches, to the quantitative setting. We thereby demonstrate that the simplicity of strong transition fairness, as well as the applicability of gadget-based techniques, can be leveraged beyond the $$\omega $$ ω -regular domain.

Abstract The goal of logical controller synthesis is to automatically compute a control strategy that regulates the discrete, event-driven behavior of a given plant s.t. a temporal logic specification holds over all remaining traces. Standard approaches to this problem construct a two-player game by composing a given complete plant model and the logical specification and applying standard algorithmic techniques to extract a control strategy. However, due to the often enormous state space of a complete plant model, this process can become computationally infeasible. In this paper, we introduce a novel synthesis approach that constructs a universal controller derived solely from the game obtained by the standard translation of the logical specification. The universal controller’s moves are annotated with prophecies – predictions about the plant’s behavior that ensure the move is safe. By evaluating these prophecies, the universal controller can be adapted to any plant over which the synthesis problem is realizable. This approach offers several key benefits, including enhanced scalability with respect to the plant’s size, adaptability to changes in the plant, and improved explainability of the resulting control strategy. We also present encouraging experimental results obtained with our prototype tool, unicon .

Abstract Infinite-state games are a commonly used model for the synthesis of reactive systems with unbounded data domains. Symbolic methods for solving such games need to be able to construct intricate arguments to establish the existence of winning strategies. Often, large problem instances require prohibitively complex arguments. Therefore, techniques that identify smaller and simpler sub-problems and exploit the respective results for the given game-solving task are highly desirable. In this paper, we propose the first such technique for infinite-state games. The main idea is to enhance symbolic game-solving with the results of localized attractor computations performed in sub-games. The crux of our approach lies in identifying useful sub-games by computing permissive winning strategy templates in finite abstractions of the infinite-state game. The experimental evaluation of our method demonstrates that it outperforms existing techniques and is applicable to infinite-state games beyond the state of the art.

We consider the problem of computing distributed logical controllers for two interacting system components via a novel sound and complete contract-based synthesis framework. Based on a discrete abstraction of component interactions as a two-player game over a finite graph and specifications for both components given as ω -regular (e.g. LTL) properties over this graph, we co-synthesize contract and controller candidates locally for each component and propose a negotiation mechanism which iteratively refines these candidates until a solution to the given distributed synthesis problem is found. Our framework relies on the recently introduced concept of permissive templates which collect an infinite number of controller candidates in a concise data structure. We utilize the efficient computability, adaptability and compositionality of such templates to obtain an efficient, yet sound and complete negotiation framework for contract-based distributed logical control. We showcase the superior performance of our approach by comparing our prototype tool CoSMo to the state-of-the-art tool on a robot motion planning benchmark suite.

In this paper, we offer a formal framework to automatically synthesize a hybrid controller for continuous-time nonlinear stochastic control systems while addressing control challenges closely integrated with logical decision-making processes. The primary goal is to enforce complex logic specifications that encompass context switches initiated by either the external environment or the system itself. The proposed game-solving framework adopts a two-layer strategy synthesis approach: (i) in the lower layer, it employs control barrier certificates to synthesize controllers that guarantee reach-while-avoid specifications over complex stochastic systems, and (ii) these controllers are subsequently utilized in a higher logical layer during a game-based logical control synthesis process. This approach enables the utilization of computational capabilities derived from state space control techniques and taps into the problem-solving intelligence inherent in finite games to handle complex logic specifications. We demonstrate the efficacy of our proposed approach over a robotic case study.

Abstract This paper considers the problem of co-synthesis in k-player games over a finite graph where each player has an individual $$\omega $$ ω -regular specification $$\phi _i$$ ϕ i . In this context, a secure equilibrium (SE) is a Nash equilibrium w.r.t. the lexicographically ordered objectives of each player to first satisfy their own specification, and second, to falsify other players’ specifications. A winning secure equilibrium (WSE) is an SE strategy profile $$(\pi _i)_{i\in [1;k]}$$ ( π i ) i ∈ [ 1 ; k ] that ensures the specification $$\phi :=\bigwedge _{i\in [1;k]}\phi _i$$ ϕ : = ⋀ i ∈ [ 1 ; k ] ϕ i if no player deviates from their strategy $$\pi _i$$ π i . Distributed implementations generated from a WSE make components act rationally by ensuring that a deviation from the WSE strategy profile is immediately punished by a retaliating strategy that makes the involved players lose. In this paper, we move from deviation punishment in WSE-based implementations to a distributed, assume-guarantee based realization of WSE. This shift is obtained by generalizing WSE from strategy profiles to specification profiles $$(\varphi _i)_{i\in [1;k]}$$ ( φ i ) i ∈ [ 1 ; k ] with $$\bigwedge _{i\in [1;k]}\varphi _i = \phi $$ ⋀ i ∈ [ 1 ; k ] φ i = ϕ , which we call most general winning secure equilibria (GWSE). Such GWSE have the property that each player can individually pick a strategy $$\pi _i$$ π i winning for $$\varphi _i$$ φ i (against all other players) and all resulting strategy profiles $$(\pi _i)_{i\in [1;k]}$$ ( π i ) i ∈ [ 1 ; k ] are guaranteed to be a WSE. The obtained flexibility in players’ strategy choices can be utilized for robustness and adaptability of local implementations. Concretely, our contribution is three-fold: (1) we formalize GWSE for k-player games over finite graphs, where each player has an $$\omega $$ ω -regular specification $$\phi _i$$ ϕ i ; (2) we devise an iterative semi-algorithm for GWSE synthesis in such games, and (3) obtain an exponential-time algorithm for GWSE synthesis with parity specifications $$\phi _i$$ ϕ i .

Abstract We present a novel method to compute permissive winning strategies in two-player games over finite graphs with $$ \omega $$ ω -regular winning conditions. Given a game graph G and a parity winning condition $$\varPhi $$ Φ , we compute a winning strategy template $$\varPsi $$ Ψ that collects an infinite number of winning strategies for objective $$\varPhi $$ Φ 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., adapting strategies to newly arriving, additional $$\omega $$ ω -regular objectives $$\varPhi '$$ Φ ′ , and (ii) fault-tolerant control, i.e., adapting strategies to the occasional or persistent unavailability of actuators. The main features of our strategy 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 instances, i.e. handling a large problem class efficiently in practice.

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.

This poster presents a new technique to synthesize a reactive hybrid controller which actuates a non-linear control system in response to external logical inputs to fulfill an omega-regular specification over a finite set of logical input and observation predicates.

Abstract We automatically compute 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 $$\varPhi $$ for the system player, we compute an $$\omega $$ -regular assumption $$\varPsi $$ for the environment player, such that (i) every environment strategy compliant with $$\varPsi $$ allows the system to fulfill $$\varPhi $$ (sufficiency), (ii) $$\varPsi $$ can be fulfilled by the environment for every strategy of the system (implementability), and (iii) $$\varPsi $$ 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 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 $$\omega $$ -regular games, we provide the first algorithm to compute sufficient and implementable environment assumptions that are also permissive.

We consider the problem of synthesizing the most robust controllers using the Abstraction-Based Controller Design (ABCD). First, we perform a finite-state abstraction of the continuous dynamic system. We then synthesize a most robust control strategy in the finite space by formulating it as a two-player game. Finally, we refine the strategy to a controller for the original problem. To preserve robustness, we consider the specifications for the controllers to be expressed in Robust Linear Temporal Logic (rLTL), which allows the reasoning about how robust the specification is. However, the current algorithms for rLTL synthesis do not compute optimally robust controllers. It only considers the worst-case analysis for reactive synthesis. Hence, we develop two new notions of adaptive strategies. One is Weakly Adaptive strategy, which, in response to the opponent's bad choices, adaptively changes the degree of satisfaction we want to achieve to ensure the optimality w.r.t. the current stage. The second one is Strongly adaptive strategy, which is weakly adaptive that also maximizes the chances of the opponent making a bad choice. We show that the computability problem for both the strategies is not harder than the classical one and can be solved in doubly-exponential time.