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.

We address the synthesis of control policies for unknown discrete-time stochastic dynamical systems to satisfy temporal logic objectives. We present a data-driven, abstraction-based control framework that integrates online learning with novel incremental game-solving. Under appropriate continuity assumptions, our method abstracts the system dynamics into a finite stochastic (2.5-player) game graph derived from data. Given a requirement over time on this graph, we compute the winning region -- i.e., the set of initial states from which the objective is satisfiable -- in the resulting game, together with a corresponding control policy. Our main contribution is the construction of abstractions, winning regions and control policies incrementally, as data about the system dynamics accumulates. Concretely, our algorithm refines under- and over-approximations of reachable sets for each state-action pair as new data samples arrive. These refinements induce structural modifications in the game graph abstraction -- such as the addition or removal of nodes and edges -- which in turn modify the winning region. Crucially, we show that these updates are inherently monotonic: under-approximations only grow, over-approximations only shrink, and the winning region only expands. We exploit this monotonicity by defining an objective-induced ranking function on the nodes of the abstract game that increases monotonically as new data samples are incorporated. These ranks underpin our novel incremental game-solving algorithm, which employs customized gadgets (DAG-like subgames) within a rank-lifting algorithm to efficiently update the winning region. Numerical case studies demonstrate significant computational savings compared to the baseline approach, which resolves the entire game from scratch whenever new data samples arrive.

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.

Abstract We consider two-player games over finite graphs in which both players are restricted by fairness constraints on their moves. Given a two player game graph $$G=(V,E)$$ G = ( V , E ) and a set of fair moves $$E_f\subseteq E$$ E f ⊆ E a player is said to play fair in G if they choose an edge $$e\in E_f$$ e ∈ E f infinitely often whenever the source node of e is visited infinitely often. Otherwise, they play unfair . We equip such games with two $$\omega $$ ω -regular winning conditions $$\alpha $$ α and $$\beta $$ β deciding the winner of mutually fair and mutually unfair plays, respectively. Whenever one player plays fair and the other plays unfair, the fairly playing player wins the game. The resulting games are called fair $$\alpha /\beta $$ α / β games . We formalize fair $$\alpha /\beta $$ α / β games and show that they are determined. For fair parity/parity games, i.e., fair $$\alpha /\beta $$ α / β games where $$\alpha $$ α and $$\beta $$ β are given each by a parity condition over G , we provide a polynomial reduction to (normal) parity games via a gadget construction inspired by the reduction of stochastic parity games to parity games. We further give a direct symbolic fixpoint algorithm to solve fair parity/parity games. On a conceptual level, we illustrate the translation between the gadget-based reduction and the direct symbolic algorithm which uncovers the underlying similarities of solution algorithms for fair and stochastic parity games, as well as for the recently considered class of fair games in which only one player is restricted by fair moves.

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.

Abstract We present a flexible and efficient toolchain to symbolically solve (standard) Rabin games, fair-adversarial Rabin games, and "Image missing" -player Rabin games. To our best knowledge, our tools are the first ones to be able to solve these problems. Furthermore, using these flexible game solvers as a back-end, we implemented a tool for computing correct-by-construction controllers for stochastic dynamical systems under LTL specifications. Our implementations use the recent theoretical result that all of these games can be solved using the same symbolic fixpoint algorithm but utilizing different, domain specific calculations of the involved predecessor operators. The main feature of our toolchain is the utilization of two programming abstractions: one to separate the symbolic fixpoint computations from the predecessor calculations, and another one to allow the integration of different BDD libraries as back-ends. In particular, we employ a multi-threaded execution of the fixpoint algorithm by using the multi-threaded BDD library Sylvan, which leads to enormous computational savings.

This paper discusses the problem of efficiently solving parity games where player Odd has to obey an additional 'strong transition fairness constraint' on its vertices -- given that a player Odd vertex $v$ is visited infinitely often, a particular subset of the outgoing edges (called live edges) of $v$ has to be taken infinitely often. Such games, which we call 'Odd-fair parity games', naturally arise from abstractions of cyber-physical systems for planning and control. In this paper, we present a new Zielonka-type algorithm for solving Odd-fair parity games. This algorithm not only shares 'the same worst-case time complexity' as Zielonka's algorithm for (normal) parity games but also preserves the algorithmic advantage Zielonka's algorithm possesses over other parity solvers with exponential time complexity. We additionally introduce a formalization of Odd player winning strategies in such games, which were unexplored previous to this work. This formalization serves dual purposes: firstly, it enables us to prove our Zielonka-type algorithm; secondly, it stands as a noteworthy contribution in its own right, augmenting our understanding of additional fairness assumptions in two-player games.

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.

We present a flexible and efficient toolchain to symbolically solve (standard) Rabin games, fair-adversarial Rabin games, and 21/2-player Rabin games. To our best knowledge, our tools are the first ones to be able to solve these problems. Furthermore, using the optimized game solvers as back-end, we implement a tool for computing correct-by-construction controllers for stochastic dynamical systems with LTL specifications. An important feature of our toolchain is the flexibility created through two programming abstractions: one separates the symbolic fixpoint computations from the predecessor calculations, and the other one allows effortless switching between different BDD libraries. We empirically compare the benefits of using the CUDD and Sylvan BDD libraries, and report substantial computational savings of our tool compared to the state-of-the-art.

This short paper presents a lazy symbolic output-feedback controller synthesis algorithm for state-based safety specifications over large transition systems. The novel idea of our approach is to integrate an iterative algorithm for observer design with an online adaptable safety controller synthesis algorithm. This allows us to iteratively update the safety controller to observer refinements and to guide these refinements by the existing controller. This results in efficient lazy synthesis of a safety controller whose domain increases with the time spent in synthesis. We present simulation results for a synthetic robot motion planning example showing the benefits of our algorithm compared to the standard approach.

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 present BOCoSy, a tool for Bounded symbolic Output-feedback Controller Synthesis. Given a specification, BOCoSy synthesizes symbolic output-feedback controllers which interact with a given plant via a pre-defined finite symbolic interface. BOCoSy solves this problem by a new lazy abstraction-refinement technique which starts with a very coarse abstraction of the external trace semantics of the given plant and iteratively removes non-admissible behavior from this abstract model until a controller is found. BOCoSy steers the search for controllers towards small and concise state space representations by utilizing ideas from bounded synthesis. As a result, BOCoSy returns small and explainable controllers that are still powerful enough to solve the given synthesis problem. We show that BOCoSy is able to synthesize small, human readable symbolic controllers quickly on a set of benchmarks.

Abstract We consider turn-based stochastic 2-player games on graphs with $$\omega $$ ω -regular winning conditions. We provide a direct symbolic algorithm for solving such games when the winning condition is formulated as a Rabin condition. For a stochastic Rabin game withkpairs over a game graph withnvertices, our algorithm runs in $$O(n^{k+2}k!)$$ O(nk+2k!) symbolic steps, which improves the state of the art. We have implemented our symbolic algorithm, along with performance optimizations including parallellization and acceleration, in a BDD-based synthesis tool called . We demonstrate the superiority of compared to the state of the art on a set of synthetic benchmarks derived from the VLTS benchmark suite and on a control system benchmark from the literature. In our experiments, performed significantly faster with up totwoorders of magnitude improvement in computation time.

We consider abstraction-based design of output-feedback controllers for dynamical systems with a finite set of inputs and outputs against specifications in linear-time temporal logic. The usual procedure for abstraction-based controller design (ABCD) first constructs a finite-state abstraction of the underlying dynamical system, and second, uses reactive synthesis techniques to compute an abstract state-feedback controller on the abstraction. In this context, our contribution is two-fold: (I) we define a suitable relation between the original system and its abstraction which characterizes the soundness and completeness conditions for an abstract state-feedback controller to be refined to a concrete output-feedback controller for the original system, and (II) we provide an algorithm to compute a sound finite-state abstraction fulfilling this relation.

We consider the computation of resilient controllers for perturbed non-linear dynamical systems w.r.t. linear-time temporal logic specifications. We address this problem through the paradigm of Abstraction-Based Controller Design (ABCD) where a finite state abstraction of the perturbed system dynamics is constructed and utilized for controller synthesis. In this context, our contribution is twofold: (I) We construct abstractions which model the impact of occasional high disturbance spikes on the system via the so called disturbance edges. (II) We show that the application of resilient reactive synthesis techniques to these abstract models results in controllers which render the resulting closed loop system maximally resilient to these occasional high disturbance spikes. We have implemented this resilient ABCD workflow on top of SCOTS and showcase our method through multiple robot planning examples.

Distributed reactive synthesis is the problem of algorithmically constructing controllers of distributed, communicating systems so that each closed-loop system satisfies a given temporal specification. We present an algorithm, called negotiation, for sound (but necessarily incomplete) distributed reactive synthesis based on assume-guarantee decompositions. The negotiation algorithm iteratively constructs assumptions and guarantees for each system. In each iteration, each system attempts to fulfill its specification and its guarantee (from the previous round), under the current assumption on the other systems, by solving a reactive synthesis problem. If the specification is not realizable, the algorithm computes a sufficient assumption on the other systems that ensures it can realize the specification and guarantee. This additional assumption further constrains the behavior of other systems and they might require an additional assumption, leading to the next round in the negotiation. The process terminates when a compatible assumption-guarantee pair is found for each system, which is sufficient to also satisfy the specification of each system. We have built a tool called Agnes that implements this algorithm. Using Agnes, we empirically demonstrate the effectiveness of our proposed algorithm on two case studies.

Many problems in reactive synthesis are stated using two formulas—an environment assumption and a system guarantee—and ask for an implementation that satisfies the guarantee in environments that satisfy their assumption. Reactive synthesis tools often produce strategies that formally satisfy such specifications by actively preventing an environment assumption from holding. While formally correct, such strategies do not capture the intention of the designer. We introduce an additional requirement in reactive synthesis, non-conflictingness, which asks that a system strategy should always allow the environment to fulfill its liveness requirements. We give an algorithm for solving GR(1) synthesis that produces non-conflicting strategies. Our algorithm is given by a 4-nested fixed point in the $$\mu $$ -calculus, in contrast to the usual 3-nested fixed point for GR(1). Our algorithm ensures that, in every environment that satisfies its assumptions on its own, traces of the resulting implementation satisfy both the assumptions and the guarantees. In addition, the asymptotic complexity of our algorithm is the same as that of the usual GR(1) solution. We have implemented our algorithm and show how its performance compares to the usual GR(1) synthesis algorithm.

We present multi-layered abstraction-based controller synthesis, which extends standard abstraction-based controller synthesis (ABCS) algorithms for continuous-time control systems by simultaneously maintaining several "layers" of abstract systems with decreasing precision. The resulting abstract multi-layered controller uses the coarsest abstraction whenever this is feasible, and dynamically adjusts the precision---by moving to a more precise abstraction and back to a coarser abstraction---based on the structure of the given control problem. Abstract multi-layered controllers can be refined to controllers with non-uniform resolution using feedback refinement relations established between each abstract layer and the concrete system, resulting in a sound ABCS method. We provide multi-layered controller synthesis algorithms for reachability, safety, and generalized Büchi specifications; our approach can be generalized to any ω-regular objective. Our algorithms are complete relative to single-layered synthesis on the finest layer. We empirically demonstrate that multi-layered synthesis can outperform standard (single-layer) ABCS algorithms on a number of examples, despite the additional cost of constructing multiple abstract systems.