arXiv subjects

Satya Prakash Nayak

Publications and source records attributed to Satya Prakash Nayak.

17 recordsLinked to original sources

arXiv2026

Context-Triggered Robust MPC for Temporal Logic Specifications

We consider the problem of synthesizing robust feedback controllers for discrete-time linear systems that ensure the satisfaction of context-dependent linear temporal logic specifications in the presence of additive bounded disturbances. Building on existing results that reduce context-triggered temporal logic synthesis to the realization of context-dependent reach-avoid-stay (cRAS) objectives, we focus on the corresponding low-level control synthesis problem. We first employ certificate-based conditions for the almost-sure satisfaction of RAS specifications. Based on these conditions, we propose a switching control architecture that combines robust model predictive control (MPC) with a local invariant controller, and show that the resulting MPC value function serves as a reachability certificate while avoidance is enforced through robust constraints and the stay is enforced via the local controller. To obtain computationally tractable formulations for the resulting robust optimizations, we employ convex duality to reformulate the robust constraints into equivalent deterministic optimization problems, yielding convex quadratic and second-order cone programs for relevant geometric settings. The proposed framework is demonstrated on a robot navigation problem with context-triggered logical switches in both static and moving environments. The results show significantly larger feasible sets than Lyapunov-based approaches, while naturally accommodating dynamic environments and online task reconfiguration.

eess.SY↗

arXiv2026

Concurrent Permissive Strategy Templates

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.

cs.GT↗

arXiv2025

Universal Safety Controllers with Learned Prophecies

\emph{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 \emph{generic controller} whose outputs are conditioned by plant behavior, called \emph{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.

cs.LO↗

arXiv2025

Follow the STARs: Dynamic $ω$-Regular Shielding of Learned Policies

This paper presents a novel dynamic post-shielding framework that enforces the full class of $ω$-regular correctness properties over pre-computed probabilistic policies. This constitutes a paradigm shift from the predominant setting of safety-shielding -- i.e., ensuring that nothing bad ever happens -- to a shielding process that additionally enforces liveness -- i.e., ensures that something good eventually happens. At the core, our method uses Strategy-Template-based Adaptive Runtime Shields (STARs), which leverage permissive strategy templates to enable post-shielding with minimal interference. As its main feature, STARs introduce a mechanism to dynamically control interference, allowing a tunable enforcement parameter to balance formal obligations and task-specific behavior at runtime. This allows to trigger more aggressive enforcement when needed, while allowing for optimized policy choices otherwise. In addition, STARs support runtime adaptation to changing specifications or actuator failures, making them especially suited for cyber-physical applications. We evaluate STARs on a mobile robot benchmark to demonstrate their controllable interference when enforcing (incrementally updated) $ω$-regular correctness properties over learned probabilistic policies.

cs.AI↗

arXiv2025

Maximal Adaptation, Minimal Guidance: Permissive Reactive Robot Task Planning with Humans in the Loop

We present a novel framework for human-robot \emph{logical} interaction that enables robots to reliably satisfy (infinite horizon) temporal logic tasks while effectively collaborating with humans who pursue independent and unknown tasks. The framework combines two key capabilities: (i) \emph{maximal adaptation} enables the robot to adjust its strategy \emph{online} to exploit human behavior for cooperation whenever possible, and (ii) \emph{minimal tunable feedback} enables the robot to request cooperation by the human online only when necessary to guarantee progress. This balance minimizes human-robot interference, preserves human autonomy, and ensures persistent robot task satisfaction even under conflicting human goals. We validate the approach in a real-world block-manipulation task with a Franka Emika Panda robotic arm and in the Overcooked-AI benchmark, demonstrating that our method produces rich, \emph{emergent} cooperative behaviors beyond the reach of existing approaches, while maintaining strong formal guarantees.

cs.RO↗

arXiv2025

Quantitative Strategy Templates

This paper presents (permissive) \emph{Quantitative Strategy Templates} (QaSTels) to succinctly represent infinitely many winning strategies in two-player energy and mean-payoff games. This transfers the recently introduced concept of \emph{Permissive (qualitative) Strategy Templates} (PeSTels) for $ω$-regular games to games with quantitative objectives. We provide the theoretical and algorithmic foundations of (i) QaSTel synthesis, and (ii) their (incremental) combination with PeSTels for games with mixed quantitative and qualitative objectives. Using a prototype implementation of our synthesis algorithms, we demonstrate empirically that QaSTels extend the advantageous properties of strategy templates over single winning strategies -- known from PeSTels -- to games with (additional) quantitative objectives. This includes (i) the enhanced robustness of strategies due to their runtime-adaptability, and (ii) the compositionality of templates w.r.t. incrementally arriving objectives. We use control-inspired examples to illustrate these superior properties of QaSTels for CPS design.

cs.GT↗

arXiv2025

Synthesis of Universal Safety Controllers

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.

cs.LO↗

arXiv2025

Fair Quantitative Games

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.

cs.GT↗

arXiv2024

Localized Attractor Computations for Infinite-State Games (Full Version)

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.

cs.LO↗

arXiv2024

Contract-Based Distributed Synthesis in Two-Objective Parity Games

We present a novel method to compute $\textit{assume-guarantee contracts}$ in non-zerosum two-player games over finite graphs where each player has a different $ ω$-regular winning condition. Given a game graph $G$ and two parity winning conditions $Φ_0$ and $Φ_1$ over $G$, we compute $\textit{contracted strategy-masks}$ ($\texttt{csm}$) $(Ψ_{i},Φ_{i})$ for each Player $i$. Within a $\texttt{csm}$, $Φ_{i}$ is a $\textit{permissive strategy template}$ which collects an infinite number of winning strategies for Player $i$ under the assumption that Player $1-i$ chooses any strategy from the $\textit{permissive assumption template}$ $Ψ_{i}$. The main feature of $\texttt{csm}$'s is their power to $\textit{fully decentralize all remaining strategy choices}$ -- if the two player's $\texttt{csm}$'s are compatible, they provide a pair of new local specifications $Φ_0^\bullet$ and $Φ_1^\bullet$ such that Player $i$ can locally and fully independently choose any strategy satisfying $Φ_i^\bullet$ and the resulting strategy profile is ensured to be winning in the original two-objective game $(G,Φ_0,Φ_1)$. In addition, the new specifications $Φ_i^\bullet$ are $\textit{maximally cooperative}$, i.e., allow for the distributed synthesis of any cooperative solution. Further, our algorithmic computation of $\texttt{csm}$'s is complete and ensured to terminate. We illustrate how the unique features of our synthesis framework effectively address multiple challenges in the context of \enquote{correct-by-design} logical control software synthesis for cyber-physical systems and provide empirical evidence that our approach possess desirable structural and computational properties compared to state-of-the-art techniques.

cs.GT↗

arXiv2024

Most General Winning Secure Equilibria Synthesis in Graph Games

This paper considers the problem of co-synthesis in $k$-player games over a finite graph where each player has an individual $ω$-regular specification $ϕ_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 $(π_i)_{i\in[1;k]}$ that ensures the specification $ϕ:=\bigwedge_{i\in[1;k]}ϕ_i$ if no player deviates from their strategy $π_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 $(φ_i)_{i\in[1;k]}$ with $\bigwedge_{i\in[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 $π_i$ winning for $φ_i$ (against all other players) and all resulting strategy profiles $(π_i)_{i\in[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 $ω$-regular specification $ϕ_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 $ϕ_i$.

cs.GT↗

arXiv2023

Robust Computation Tree Logic

It is widely accepted that every system should be robust in that ``small'' violations of environment assumptions should lead to ``small'' violations of system guarantees, but it is less clear how to make this intuition mathematically precise. While significant efforts have been devoted to providing notions of robustness for Linear Temporal Logic (LTL), branching-time logics, such as Computation Tree Logic (CTL) and CTL*, have received less attention in this regard. To address this shortcoming, we develop ``robust'' extensions of CTL and CTL*, which we name robust CTL (rCTL) and robust CTL* (rCTL*). Both extensions are syntactically similar to their parent logics but employ multi-valued semantics to distinguish between ``large'' and ``small'' violations of the specification. We show that the multi-valued semantics of rCTL make it more expressive than CTL, while rCTL* is as expressive as CTL*. Moreover, we show that the model checking problem, the satisfiability problem, and the synthesis problem for rCTL and rCTL* have the same asymptotic complexity as their non-robust counterparts, implying that robustness can be added to branching-time logics for free.

cs.LO↗

arXiv2023

Solving Two-Player Games under Progress Assumptions

This paper considers the problem of solving infinite two-player games over finite graphs under various classes of progress assumptions motivated by applications in cyber-physical system (CPS) design. Formally, we consider a game graph G, a temporal specification $Φ$ and a temporal assumption $ψ$, where both are given as linear temporal logic (LTL) formulas over the vertex set of G. We call the tuple $(G,Φ,ψ)$ an 'augmented game' and interpret it in the classical way, i.e., winning the augmented game $(G,Φ,ψ)$ is equivalent to winning the (standard) game $(G,ψ\implies Φ)$. Given a reachability or parity game $(G,Φ)$ and some progress assumption $ψ$, this paper establishes whether solving the augmented game $(G,Φ,ψ)$ lies in the same complexity class as solving $(G,Φ)$. While the answer to this question is negative for arbitrary combinations of $Φ$ and $ψ$, a positive answer results in more efficient algorithms, in particular for large game graphs. We therefore restrict our attention to particular classes of CPS-motivated progress assumptions and establish the worst-case time complexity of the resulting augmented games. Thereby, we pave the way towards a better understanding of assumption classes that can enable the development of efficient solution algorithms in augmented two-player games.

cs.GT↗

arXiv2023

Context-triggered Abstraction-based Control Design

We consider the problem of automatically synthesizing a hybrid controller for non-linear dynamical systems which ensures that the closed-loop fulfills an arbitrary \emph{Linear Temporal Logic} specification. Moreover, the specification may take into account logical context switches induced by an external environment or the system itself. Finally, we want to avoid classical brute-force time- and space-discretization for scalability. We achieve these goals by a novel two-layer strategy synthesis approach, where the controller generated in the lower layer provides invariant sets and basins of attraction, which are exploited at the upper logical layer in an abstract way. In order to achieve this, we provide new techniques for both the upper- and lower-level synthesis. Our new methodology allows to leverage both the computing power of state space control techniques and the intelligence of finite game solving for complex specifications, in a scalable way.

eess.SY↗

arXiv2023

Synthesizing Permissive Winning Strategy Templates for Parity Games

We present a novel method to compute \emph{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 \emph{winning strategy template} $Ψ$ that collects an infinite number 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) \emph{incremental synthesis}, i.e., adapting strategies to newly arriving, \emph{additional} $ω$-regular objectives $Φ'$, and (ii) \emph{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 \emph{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.

cs.GT↗

arXiv2023

Computing Adequately Permissive Assumptions for Synthesis

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 $ω$-regular winning condition $Φ$ for the system player, we compute an $ω$-regular assumption $Ψ$ for the environment player, such that (i) every environment strategy compliant with $Ψ$ allows the system to fulfill $Φ$ (sufficiency), (ii) $Ψ$ can be fulfilled by the environment for every strategy of the system (implementability), and (iii) $Ψ$ does not prevent any cooperative strategy choice (permissiveness). For parity games, which are canonical representations of $ω$-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 $ω$-regular games, we provide the first algorithm to compute sufficient and implementable environment assumptions that are also permissive.

cs.GT↗

arXiv2022

Robustness-by-Construction Synthesis: Adapting to the Environment at Runtime

While most of the current synthesis algorithms only focus on correctness-by-construction, ensuring robustness has remained a challenge. Hence, in this paper, we address the robust-by-construction synthesis problem by considering the specifications to be expressed by a robust version of Linear Temporal Logic (LTL), called robust LTL (rLTL). rLTL has a many-valued semantics to capture different degrees of satisfaction of a specification, i.e., satisfaction is a quantitative notion. We argue that the current algorithms for rLTL synthesis do not compute optimal strategies in a non-antagonistic setting. So, a natural question is whether there is a way of satisfying the specification "better" if the environment is indeed not antagonistic. We address this question by developing two new notions of strategies. The first notion is that of adaptive strategies, which, in response to the opponent's non-antagonistic moves, maximize the degree of satisfaction. The idea is to monitor non-optimal moves of the opponent at runtime using multiple parity automata and adaptively change the system strategy to ensure optimality. The second notion is that of strongly adaptive strategies, which is a further refinement of the first notion. These strategies also maximize the opportunities for the opponent to make non-optimal moves. We show that computing such strategies for rLTL specifications is not harder than the standard synthesis problem, e.g., computing strategies with LTL specifications, and takes doubly-exponential time.

cs.LO↗