SearcharxivSearch

arXiv subjects

Debraj Chakraborty

Publications and source records attributed to Debraj Chakraborty.

At least 19 recordsLinked to original sources

Explainably Safe Reinforcement Learning

Trust in a decision-making system requires both safety guarantees and the ability to interpret and understand its behavior. This is particularly important for learned systems, whose decision-making processes are often highly opaque. Shielding is a prominent model-based technique for enforcing safety in reinforcement learning. However, because shields are automatically synthesized using rigorous formal methods, their decisions are often similarly difficult for humans to interpret. Recently, decision trees became customary to represent controllers and policies. However, since shields are inherently non-deterministic, their decision tree representations become too large to be explainable in practice. To address this challenge, we propose a novel approach for explainable safe RL that enhances trust by providing human-interpretable explanations of the shield's decisions. Our method represents the shielding policy as a hierarchy of decision trees, offering top-down, case-based explanations. At design time, we use a world model to analyze the safety risks of executing actions in given states. Based on this analysis, we construct both the shield and a high-level decision tree that classifies states into risk categories (safe, critical, dangerous, unsafe), explaining why a situation may be safety-critical. At runtime, we generate localized decision trees that explain which actions are allowed and why others are deemed unsafe. Our method facilitates explainability of the safety aspect in safe-by-shielding reinforcement learning, requires no additional information beyond what is already used for shielding, incurs minimal overhead, and integrates readily into existing shielded RL pipelines. In our experiments, we compute explanations using decision trees that are several orders of magnitude smaller than the original shield.

cs.LG

Synthesizing POMDP Policies: Sampling Meets Model-checking via Learning

Partially Observable Markov Decision Processes (POMDPs) are the standard framework for decision-making under uncertainty. While sampling-based methods scale well, they lack formal correctness guarantees, making them unsuitable for safety-critical applications. Conversely, formal synthesis techniques provide correctness-by-construction but often struggle with scalability, as general POMDP synthesis is undecidable. To bridge this gap, we propose a synthesis framework that integrates sampling, automata learning, and model-checking. Inspired by Angluin's $L^*$ algorithm, our approach utilizes sampling as a membership oracle and model-checking as an equivalence oracle. This enables the synthesis of finite-state controllers with formal guarantees, provided the sampling-induced policy is regular. We establish a relative completeness result for this framework. Experimental results from our prototypical implementation demonstrate that this method successfully solves threshold-safety problems that remain challenging for existing formal synthesis tools. We believe our algorithm serves as a valuable component in a portfolio approach to tackling the inherent difficulty of POMDP synthesis problems.

cs.AI

Explainable Representation of Finite-Memory Policies for POMDPs using Decision Trees

Partially Observable Markov Decision Processes (POMDPs) are a fundamental framework for decision-making under uncertainty and partial observability. Since in general optimal policies may require infinite memory, they are hard to implement and often render most problems undecidable. Consequently, finite-memory policies are mostly considered instead. However, the algorithms for computing them are typically very complex, and so are the resulting policies. Facing the need for their explainability, we provide a representation of such policies, both (i) in an interpretable formalism and (ii) typically of smaller size, together yielding higher explainability. To that end, we combine models of Mealy machines and decision trees; the latter describing simple, stationary parts of the policies and the former describing how to switch among them. We design a translation for policies of the finite-state-controller (FSC) form from standard literature and show how our method smoothly generalizes to other variants of finite-memory policies. Further, we identify specific properties of recently used "attractor-based" policies, which allow us to construct yet simpler and smaller representations. Finally, we illustrate the higher explainability in a few case studies.

cs.AI

Resilient Strategies for Stochastic Systems: How Much Does It Take to Break a Winning Strategy?

We study the problem of resilient strategies in the presence of uncertainty. Resilient strategies enable an agent to make decisions that are robust against disturbances. In particular, we are interested in those disturbances that are able to flip a decision made by the agent. Such a disturbance may, for instance, occur when the intended action of the agent cannot be executed due to a malfunction of an actuator in the environment. In this work, we introduce the concept of resilience in the stochastic setting and present a comprehensive set of fundamental problems. Specifically, we discuss such problems for Markov decision processes with reachability and safety objectives, which also smoothly extend to stochastic games. To account for the stochastic setting, we provide various ways of aggregating the amounts of disturbances that may have occurred, for instance, in expectation or in the worst case. Moreover, to reason about infinite disturbances, we use quantitative measures, like their frequency of occurrence.

cs.GT

Incremental Data Driven Transfer Identification

We introduce a geometric method for online transfer identification of a deterministic linear time-invariant system. At the beginning of the identification process, we assume access to abundant data from a system that is similar, though not identical, to the true system. In the early stages of data collection from the true system, the dataset generated is still not sufficiently informative to enable precise identification. Consequently, multiple candidate models remain consistent with the observations available at that point. Our method picks, at each instant, the model closest to the similar system that is consistent with the current data. As more data are collected, the proposed model gradually moves away from the initial similar system and eventually converges to the true system when the data set grows to be informative. Numerical examples demonstrate the effectiveness of the incremental transfer identification paradigm, where identified models with minimal data are used to solve the pole placement problem.

eess.SY

Planar Herding of Multiple Evaders with a Single Herder

A planar herding problem is considered, where a superior pursuer herds a flock of non-cooperative, inferior evaders around a predefined target point. An inverse square law of repulsion is assumed between the pursuer and each evader. Two classes of pursuer trajectories are proposed: (i) a constant angular-velocity spiral, and (ii) a constant angular-velocity circle, both centered around the target point. For the spiraling pursuer, the radial velocity is dynamically adjusted based on a feedback law that depends on the instantaneous position of the evader, which is located at the farthest distance from the target at the start of the game. It is shown that, under suitable choices of the model parameters, all the evaders are herded into an arbitrarily small limit cycle around the target point. Meanwhile, the pursuer also converges onto a circular trajectory around the target. The conditions for the stability of these limit cycles are derived. For the circling pursuer, similar guarantees are provided along with explicit formulas for the radii of the limit cycles.

eess.SY

1-2-3-Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization

Despite the advances in probabilistic model checking, the scalability of the verification methods remains limited. In particular, the state space often becomes extremely large when instantiating parameterized Markov decision processes (MDPs) even with moderate values. Synthesizing policies for such \emph{huge} MDPs is beyond the reach of available tools. We propose a learning-based approach to obtain a reasonable policy for such huge MDPs. The idea is to generalize optimal policies obtained by model-checking small instances to larger ones using decision-tree learning. Consequently, our method bypasses the need for explicit state-space exploration of large models, providing a practical solution to the state-space explosion problem. We demonstrate the efficacy of our approach by performing extensive experimentation on the relevant models from the quantitative verification benchmark set. The experimental results indicate that our policies perform well, even when the size of the model is orders of magnitude beyond the reach of state-of-the-art analysis tools.

cs.AI

Explaining Control Policies through Predicate Decision Diagrams

Safety-critical controllers of complex systems are hard to construct manually. Automated approaches such as controller synthesis or learning provide a tempting alternative but usually lack explainability. To this end, learning decision trees (DTs) have been prevalently used towards an interpretable model of the generated controllers. However, DTs do not exploit shared decision-making, a key concept exploited in binary decision diagrams (BDDs) to reduce their size and thus improve explainability. In this work, we introduce predicate decision diagrams (PDDs) that extend BDDs with predicates and thus unite the advantages of DTs and BDDs for controller representation. We establish a synthesis pipeline for efficient construction of PDDs from DTs representing controllers, exploiting reduction techniques for BDDs also for PDDs.

cs.AI

Learning Explainable and Better Performing Representations of POMDP Strategies

Strategies for partially observable Markov decision processes (POMDP) typically require memory. One way to represent this memory is via automata. We present a method to learn an automaton representation of a strategy using a modification of the L*-algorithm. Compared to the tabular representation of a strategy, the resulting automaton is dramatically smaller and thus also more explainable. Moreover, in the learning process, our heuristics may even improve the strategy's performance. In contrast to approaches that synthesize an automaton directly from the POMDP thereby solving it, our approach is incomparably more scalable.

cs.AI

Fast Randomized Subspace System Identification for Large I/O Data

In this article, a novel fast randomized subspace system identification method for estimating combined deterministic-stochastic LTI state-space models, is proposed. The algorithm is especially well-suited to identify high-order and multi-scale systems with both fast and slow dynamics, which typically require a large number of input-output data samples for accurate identification using traditional subspace methods. Instead of working with such large matrices, the dataset is compressed using randomized methods, which preserve the range-spaces of these matrices almost surely. A novel identification algorithm using this compressed dataset, is proposed. This method enables the handling of extremely large datasets, which often make conventional algorithms like N4SID, MOESP, etc. run out of computer memory. Moreover the proposed method outperforms these algorithms in terms of memory-cost, data-movement, flop count and computation time for cases where these algorithms still work in-spite of large data sizes. The effectiveness of the proposed algorithm is established by theoretical analysis and various real and simulated case studies.

eess.SY

Learning from similar systems and online data-driven LQR using iterative randomised data compression

The problem of data-driven recursive computation of receding horizon LQR control through a randomized combination of online/current and historical/recorded data is considered. It is assumed that large amounts of historical input-output data from a system, which is similar but not identical to the current system under consideration, is available. This (possibly large) data set is compressed through a novel randomized subspace algorithm to directly synthesize an initial solution of the standard LQR problem, which however is sub-optimal due to the inaccuracy of the historical model. The first instance of this input is used to actuate the current system and the corresponding instantaneous output is used to iteratively re-solve the LQR problem through a computationally inexpensive randomized rank-one update of the old compressed data. The first instance of the re-computed input is applied to the system at the next instant, output recorded and the entire procedure is repeated at each subsequent instant. As more current data becomes available, the algorithm learns automatically from the new data while simultaneously controlling the system in near optimal manner. The proposed algorithm is computationally inexpensive due to the initial and repeated compression of old and newly available data. Moreover, the simultaneous learning and control makes this algorithm particularly suited for adapting to unknown, poorly modeled and time-varying systems without any explicit exploration stage. Simulations demonstrate the effectiveness of the proposed algorithm vs popular exploration/exploitation approaches to LQR control.

eess.SY

Bi-Objective Lexicographic Optimization in Markov Decision Processes with Related Objectives

We consider lexicographic bi-objective problems on Markov Decision Processes (MDPs), where we optimize one objective while guaranteeing optimality of another. We propose a two-stage technique for solving such problems when the objectives are related (in a way that we formalize). We instantiate our technique for two natural pairs of objectives: minimizing the (conditional) expected number of steps to a target while guaranteeing the optimal probability of reaching it; and maximizing the (conditional) expected average reward while guaranteeing an optimal probability of staying safe (w.r.t. some safe set of states). For the first combination of objectives, which covers the classical frozen lake environment from reinforcement learning, we also report on experiments performed using a prototype implementation of our algorithm and compare it with what can be obtained from state-of-the-art probabilistic model checkers solving optimal reachability.

cs.GT

Formally-Sharp DAgger for MCTS: Lower-Latency Monte Carlo Tree Search using Data Aggregation with Formal Methods

We study how to efficiently combine formal methods, Monte Carlo Tree Search (MCTS), and deep learning in order to produce high-quality receding horizon policies in large Markov Decision processes (MDPs). In particular, we use model-checking techniques to guide the MCTS algorithm in order to generate offline samples of high-quality decisions on a representative set of states of the MDP. Those samples can then be used to train a neural network that imitates the policy used to generate them. This neural network can either be used as a guide on a lower-latency MCTS online search, or alternatively be used as a full-fledged policy when minimal latency is required. We use statistical model checking to detect when additional samples are needed and to focus those additional samples on configurations where the learnt neural network policy differs from the (computationally-expensive) offline policy. We illustrate the use of our method on MDPs that model the Frozen Lake and Pac-Man environments -- two popular benchmarks to evaluate reinforcement-learning algorithms.

cs.AI

Asynchronous Distributed Consensus with Minimum Communication

In this paper, the communication effort required in a multi-agent system (MAS) is minimized via an explicit optimization formulation. The paper considers a MAS of single-integrator agents with bounded inputs and a time-invariant communication graph. A new model of discrete asynchronous communication and a distributed consensus protocol based on it, are proposed. The goal of the proposed protocol is to minimize the aggregate number of communication instants of all agents, required to steer the state trajectories inside a pres-specified bounded neighbourhood within a pre-specified time. Due to information structure imposed by the underlying communication graph, an individual agent does not know the global parameters in the MAS, which are required for the above-mentioned minimization. To counter this uncertainty, the worst-case realizations of the global parameters are considered, which lead to min-max type optimizations. The control rules in the proposed protocol are obtained as the closed form solutions of these optimization problems. Hence, the proposed protocol does not increase the burden of run-time computation making it suitable for time-critical applications.

eess.SY

Graphical estimation of multivariate count time series

The problems of selecting partial correlation and causality graphs for count data are considered. A parameter driven generalized linear model is used to describe the observed multivariate time series of counts. Partial correlation and causality graphs corresponding to this model explain the dependencies between each time series of the multivariate count data. In order to estimate these graphs with tunable sparsity, an appropriate likelihood function maximization is regularized with an l1-type constraint. A novel MCEM algorithm is proposed to iteratively solve this regularized MLE. Asymptotic convergence results are proved for the sequence generated by the proposed MCEM algorithm with l1-type regularization. The algorithm is first successfully tested on simulated data. Thereafter, it is applied to observed weekly dengue disease counts from each ward of Greater Mumbai city. The interdependence of various wards in the proliferation of the disease is characterized by the edges of the inferred partial correlation graph. On the other hand, the relative roles of various wards as sources and sinks of dengue spread is quantified by the number and weights of the directed edges originating from and incident upon each ward. From these estimated graphs, it is observed that some special wards act as epicentres of dengue spread even though their disease counts are relatively low.

stat.ML

Safe Learning for Near Optimal Scheduling

In this paper, we investigate the combination of synthesis, model-based learning, and online sampling techniques to obtain safe and near-optimal schedulers for a preemptible task scheduling problem. Our algorithms can handle Markov decision processes (MDPs) that have 1020 states and beyond which cannot be handled with state-of-the art probabilistic model-checkers. We provide probably approximately correct (PAC) guarantees for learning the model. Additionally, we extend Monte-Carlo tree search with advice, computed using safety games or obtained using the earliest-deadline-first scheduler, to safely explore the learned model online. Finally, we implemented and compared our algorithms empirically against shielded deep Q-learning on large task systems.

cs.AI

A time-optimal feedback control for a particular case of the game of two cars

In this paper, a time-optimal feedback solution to the game of two cars, for the case where the pursuer is faster and more agile than the evader, is presented. The concept of continuous subsets of the reachable set is introduced to characterize the time-optimal pursuit-evasion game under feedback strategies. Using these subsets it is shown that, if initially the pursuer is distant enough from the evader, then the feedback saddle point strategies for both the pursuer and the evader are coincident with one of the common tangents from the minimum radius turning circles of the pursuer to the minimum radius turning circles of the evader. Using geometry, four feasible tangents are identified and the feedback min-max strategy for the pursuer and the max-min strategy for the evader are derived by solving a $2 \times 2$ matrix game at each instant. Insignificant computational effort is involved in evaluating the pursuer and evader inputs using the proposed feedback control law and hence it is suitable for real-time implementation. The proposed law is validated further by comparing the resulting trajectories with those obtained by solving the differential game using numerical techniques.

eess.SY

Monte Carlo Tree Search guided by Symbolic Advice for MDPs

In this paper, we consider the online computation of a strategy that aims at optimizing the expected average reward in a Markov decision process. The strategy is computed with a receding horizon and using Monte Carlo tree search (MCTS). We augment the MCTS algorithm with the notion of symbolic advice, and show that its classical theoretical guarantees are maintained. Symbolic advice are used to bias the selection and simulation strategies of MCTS. We describe how to use QBF and SAT solvers to implement symbolic advice in an efficient way. We illustrate our new algorithm using the popular game Pac-Man and show that the performances of our algorithm exceed those of plain MCTS as well as the performances of human players.

cs.GT