arXiv subjects

Ufuk Topcu

Publications and source records attributed to Ufuk Topcu.

At least 271 records · Page 15Linked to original sources

arXiv2020

Qualitative Controller Synthesis for Consumption Markov Decision Processes

Consumption Markov Decision Processes (CMDPs) are probabilistic decision-making models of resource-constrained systems. In a CMDP, the controller possesses a certain amount of a critical resource, such as electric power. Each action of the controller can consume some amount of the resource. Resource replenishment is only possible in special reload states, in which the resource level can be reloaded up to the full capacity of the system. The task of the controller is to prevent resource exhaustion, i.e. ensure that the available amount of the resource stays non-negative, while ensuring an additional linear-time property. We study the complexity of strategy synthesis in consumption MDPs with almost-sure Büchi objectives. We show that the problem can be solved in polynomial time. We implement our algorithm and show that it can efficiently solve CMDPs modelling real-world scenarios.

cs.FL↗

arXiv2020

Verification of Markov Decision Processes with Risk-Sensitive Measures

We develop a method for computing policies in Markov decision processes with risk-sensitive measures subject to temporal logic constraints. Specifically, we use a particular risk-sensitive measure from cumulative prospect theory, which has been previously adopted in psychology and economics. The nonlinear transformation of the probabilities and utility functions yields a nonlinear programming problem, which makes computation of optimal policies typically challenging. We show that this nonlinear weighting function can be accurately approximated by the difference of two convex functions. This observation enables efficient policy computation using convex-concave programming. We demonstrate the effectiveness of the approach on several scenarios.

cs.AI↗

arXiv2020

Privacy-Preserving Policy Synthesis in Markov Decision Processes

In decision-making problems, the actions of an agent may reveal sensitive information that drives its decisions. For instance, a corporation's investment decisions may reveal its sensitive knowledge about market dynamics. To prevent this type of information leakage, we introduce a policy synthesis algorithm that protects the privacy of the transition probabilities in a Markov decision process. We use differential privacy as the mathematical definition of privacy. The algorithm first perturbs the transition probabilities using a mechanism that provides differential privacy. Then, based on the privatized transition probabilities, we synthesize a policy using dynamic programming. Our main contribution is to bound the "cost of privacy," i.e., the difference between the expected total rewards with privacy and the expected total rewards without privacy. We also show that computing the cost of privacy has time complexity that is polynomial in the parameters of the problem. Moreover, we establish that the cost of privacy increases with the strength of differential privacy protections, and we quantify this increase. Finally, numerical experiments on two example environments validate the established relationship between the cost of privacy and the strength of data privacy protections.

eess.SY↗

arXiv2020

Scalable Synthesis of Minimum-Information Linear-Gaussian Control by Distributed Optimization

We consider a discrete-time linear-quadratic Gaussian control problem in which we minimize a weighted sum of the directed information from the state of the system to the control input and the control cost. The optimal control and sensing policies can be synthesized jointly by solving a semidefinite programming problem. However, the existing solutions typically scale cubic with the horizon length. We leverage the structure in the problem to develop a distributed algorithm that decomposes the synthesis problem into a set of smaller problems, one for each time step. We prove that the algorithm runs in time linear in the horizon length. As an application of the algorithm, we consider a path-planning problem in a state space with obstacles under the presence of stochastic disturbances. The algorithm computes a locally optimal solution that jointly minimizes the perception and control cost while ensuring the safety of the path. The numerical examples show that the algorithm can scale to thousands of horizon length and compute locally optimal solutions.

eess.SY↗

arXiv2020

Identifying Sparse Low-Dimensional Structures in Markov Chains: A Nonnegative Matrix Factorization Approach

We consider the problem of learning low-dimensional representations for large-scale Markov chains. We formulate the task of representation learning as that of mapping the state space of the model to a low-dimensional state space, called the kernel space. The kernel space contains a set of meta states which are desired to be representative of only a small subset of original states. To promote this structural property, we constrain the number of nonzero entries of the mappings between the state space and the kernel space. By imposing the desired characteristics of the representation, we cast the problem as a constrained nonnegative matrix factorization. To compute the solution, we propose an efficient block coordinate gradient descent and theoretically analyze its convergence properties.

cs.LG↗

arXiv2020

Online Synthesis for Runtime Enforcement of Safety in Multi-Agent Systems

A shield is attached to a system to guarantee safety by correcting the system's behavior at runtime. Existing methods that employ design-time synthesis of shields do not scale to multi-agent systems. Moreover, such shields are typically implemented in a centralized manner, requiring global information on the state of all agents in the system. We address these limitations through a new approach where the shields are synthesized at runtime and do not require global information. There is a shield onboard every agent, which can only modify the behavior of the corresponding agent. In this approach, which is fundamentally decentralized, the shield on every agent has two components: a pathfinder that corrects the behavior of the agent and an ordering mechanism that dynamically modifies the priority of the agent. The current priority determines if the shield uses the pathfinder to modify behavior of the agent. We derive an upper bound on the maximum deviation for any agent from its original behavior. We prove that the worst-case synthesis time is quadratic in the number of agents at runtime as opposed to exponential at design-time for existing methods. We test the performance of the decentralized, runtime shield synthesis approach on a collision-avoidance problem. For 50 agents in a 50x50 grid, the synthesis at runtime requires a few seconds per agent whenever a potential collision is detected. In contrast, the centralized design-time synthesis of shields for a similar setting is intractable beyond 4 agents in a 5x5 grid.

eess.SY↗

arXiv2020

Scenario-Based Verification of Uncertain MDPs

We consider Markov decision processes (MDPs) in which the transition probabilities and rewards belong to an uncertainty set parametrized by a collection of random variables. The probability distributions for these random parameters are unknown. The problem is to compute the probability to satisfy a temporal logic specification within any MDP that corresponds to a sample from these unknown distributions. In general, this problem is undecidable, and we resort to techniques from so-called scenario optimization. Based on a finite number of samples of the uncertain parameters, each of which induces an MDP, the proposed method estimates the probability of satisfying the specification by solving a finite-dimensional convex optimization problem. The number of samples required to obtain a high confidence on this estimate is independent from the number of states and the number of random parameters. Experiments on a large set of benchmarks show that a few thousand samples suffice to obtain high-quality confidence bounds with a high probability.

cs.LO↗

arXiv2020

Playing Against Opponents With Limited Memory

We study \emph{partial-information} two-player turn-based games on graphs with omega-regular objectives, when the partial-information player has \emph{limited memory}. Such games are a natural formalization for reactive synthesis when the environment player is not genuinely adversarial to the system player. The environment player has goals of its own, but the exact goal of the environment player is unknown to the system player. We prove that the problem of determining the existence of a winning strategy for the system player is PSPACE-hard for reachability, safety, and parity objectives. Moreover, when the environment player is memoryless, the problem is PSPACE-complete. However, it is simpler to decide if the environment player has a winning strategy; it is only NP-complete. Additionally, we construct a game where the the partial-information player needs at least $\mathcal{O}(\sqrt{n})$ bits of memory to retain winning strategies in a game of size $\mathcal{O}(n)$.

cs.FL↗

arXiv2020

Verifiable RNN-Based Policies for POMDPs Under Temporal Logic Constraints

Recurrent neural networks (RNNs) have emerged as an effective representation of control policies in sequential decision-making problems. However, a major drawback in the application of RNN-based policies is the difficulty in providing formal guarantees on the satisfaction of behavioral specifications, e.g. safety and/or reachability. By integrating techniques from formal methods and machine learning, we propose an approach to automatically extract a finite-state controller (FSC) from an RNN, which, when composed with a finite-state system model, is amenable to existing formal verification tools. Specifically, we introduce an iterative modification to the so-called quantized bottleneck insertion technique to create an FSC as a randomized policy with memory. For the cases in which the resulting FSC fails to satisfy the specification, verification generates diagnostic information. We utilize this information to either adjust the amount of memory in the extracted FSC or perform focused retraining of the RNN. While generally applicable, we detail the resulting iterative procedure in the context of policy synthesis for partially observable Markov decision processes (POMDPs), which is known to be notoriously hard. The numerical experiments show that the proposed approach outperforms traditional POMDP synthesis methods by 3 orders of magnitude within 2% of optimal benchmark values.

cs.AI↗

arXiv2020

Adaptive Teaching of Temporal Logic Formulas to Learners with Preferences

Machine teaching is an algorithmic framework for teaching a target hypothesis via a sequence of examples or demonstrations. We investigate machine teaching for temporal logic formulas -- a novel and expressive hypothesis class amenable to time-related task specifications. In the context of teaching temporal logic formulas, an exhaustive search even for a myopic solution takes exponential time (with respect to the time span of the task). We propose an efficient approach for teaching parametric linear temporal logic formulas. Concretely, we derive a necessary condition for the minimal time length of a demonstration to eliminate a set of hypotheses. Utilizing this condition, we propose a myopic teaching algorithm by solving a sequence of integer programming problems. We further show that, under two notions of teaching complexity, the proposed algorithm has near-optimal performance. The results strictly generalize the previous results on teaching preference-based version space learners. We evaluate our algorithm extensively under a variety of learner types (i.e., learners with different preference models) and interactive protocols (e.g., batched and adaptive). The results show that the proposed algorithms can efficiently teach a given target temporal logic formula under various settings, and that there are significant gains of teaching efficacy when the teacher adapts to the learner's current hypotheses or uses oracles.

cs.AI↗

arXiv2020

Policy Synthesis for Factored MDPs with Graph Temporal Logic Specifications

We study the synthesis of policies for multi-agent systems to implement spatial-temporal tasks. We formalize the problem as a factored Markov decision process subject to so-called graph temporal logic specifications. The transition function and the spatial-temporal task of each agent depend on the agent itself and its neighboring agents. The structure in the model and the specifications enable to develop a distributed algorithm that, given a factored Markov decision process and a graph temporal logic formula, decomposes the synthesis problem into a set of smaller synthesis problems, one for each agent. We prove that the algorithm runs in time linear in the total number of agents. The size of the synthesis problem for each agent is exponential only in the number of neighboring agents, which is typically much smaller than the number of agents. We demonstrate the algorithm in case studies on disease control and urban security. The numerical examples show that the algorithm can scale to hundreds of agents.

cs.MA↗

arXiv2020

Robust Policy Synthesis for Uncertain POMDPs via Convex Optimization

We study the problem of policy synthesis for uncertain partially observable Markov decision processes (uPOMDPs). The transition probability function of uPOMDPs is only known to belong to a so-called uncertainty set, for instance in the form of probability intervals. Such a model arises when, for example, an agent operates under information limitation due to imperfect knowledge about the accuracy of its sensors. The goal is to compute a policy for the agent that is robust against all possible probability distributions within the uncertainty set. In particular, we are interested in a policy that robustly ensures the satisfaction of temporal logic and expected reward specifications. We state the underlying optimization problem as a semi-infinite quadratically-constrained quadratic program (QCQP), which has finitely many variables and infinitely many constraints. Since QCQPs are non-convex in general and practically infeasible to solve, we resort to the so-called convex-concave procedure to convexify the QCQP. Even though convex, the resulting optimization problem still has infinitely many constraints and is NP-hard. For uncertainty sets that form convex polytopes, we provide a transformation of the problem to a convex QCQP with finitely many constraints. We demonstrate the feasibility of our approach by means of several case studies that highlight typical bottlenecks for our problem. In particular, we show that we are able to solve benchmarks with hundreds of thousands of states, hundreds of different observations, and we investigate the effect of different levels of uncertainty in the models.

math.OC↗

arXiv2020

Policy Synthesis for Switched Linear Systems with Markov Decision Process Switching

We study the synthesis of mode switching protocols for a class of discrete-time switched linear systems in which the mode jumps are governed by Markov decision processes (MDPs). We call such systems MDP-JLS for brevity. Each state of the MDP corresponds to a mode in the switched system. The probabilistic state transitions in the MDP represent the mode transitions. We focus on finding a policy that selects the switching actions at each mode such that the switched system that follows these actions is guaranteed to be stable. Given a policy in the MDP, the considered MDP-JLS reduces to a Markov jump linear system (MJLS). {We consider both mean-square stability and stability with probability one. For mean-square stability, we leverage existing stability conditions for MJLSs and propose efficient semidefinite programming formulations to find a stabilizing policy in the MDP. For stability with probability one, we derive new sufficient conditions and compute a stabilizing policy using linear programming. We also extend the policy synthesis results to MDP-JLS with uncertain mode transition probabilities.

eess.SY↗

arXiv2019

Controller Synthesis of Wind Turbine Generator and Energy Storage System with Stochastic Wind Variations under Temporal Logic Specifications

In this paper, we present a controller synthesis approach for wind turbine generators (WTG) and energy storage systems with metric temporal logic (MTL) specifications, with provable probabilistic guarantees in the stochastic environment of wind power generation. The MTL specifications are requirements for the grid frequency deviations, WTG rotor speed variations and the power flow constraints at different lines. We present the stochastic control bisimulation function, which bounds the divergence of the trajectories of a switched stochastic control system and the switched nominal control system in a probabilistic fashion.We first design a feedforward controller by solving an optimization problem for the nominal trajectory of the deterministic control system with robustness against initial state variations and stochastic uncertainties. Then we generate a feedback control law from the data of the simulated trajectories. We implement our control method on both a four-bus system and a nine-bus system, and test the effectiveness of the method with a generation loss disturbance. We also test the advantage of the feedback controller over the feedforward controller when unexpected disturbance occurs.

eess.SY↗

arXiv2019

Minimizing the Information Leakage Regarding High-Level Task Specifications

We consider a scenario in which an autonomous agent carries out a mission in a stochastic environment while passively observed by an adversary. For the agent, minimizing the information leaked to the adversary regarding its high-level specification is critical in creating an informational advantage. We express the specification of the agent as a parametric linear temporal logic formula, measure the information leakage by the adversary's confidence in the agent's mission specification, and propose algorithms to synthesize a policy for the agent which minimizes the information leakage to the adversary. In the scenario considered, the adversary aims to infer the specification of the agent from a set of candidate specifications, each of which has an associated likelihood probability. The agent's objective is to synthesize a policy that maximizes the entropy of the adversary's likelihood distribution while satisfying its specification. We propose two approaches to solve the resulting synthesis problem. The first approach computes the exact satisfaction probabilities for each candidate specification, whereas the second approach utilizes the Fréchet inequalities to approximate them. For each approach, we formulate a mixed-integer program with a quasiconcave objective function. We solve the problem using a bisection algorithm. Finally, we compare the performance of both approaches on numerical simulations.

math.OC↗

arXiv2019

Strategy Synthesis for Surveillance-Evasion Games with Learning-Enabled Visibility Optimization

This paper studies a two-player game with a quantitative surveillance requirement on an adversarial target moving in a discrete state space and a secondary objective to maximize short-term visibility of the environment. We impose the surveillance requirement as a temporal logic constraint.We then use a greedy approach to determine vantage points that optimize a notion of information gain, namely, the number of newly-seen states. By using a convolutional neural network trained on a class of environments, we can efficiently approximate the information gain at each potential vantage point.Subsequent vantage points are chosen such that moving to that location will not jeopardize the surveillance requirement, regardless of any future action chosen by the target. Our method combines guarantees of correctness from formal methods with the scalability of machine learning to provide an efficient approach for surveillance-constrained visibility optimization.

cs.RO↗

arXiv2019

Online Active Perception for Partially Observable Markov Decision Processes with Limited Budget

Active perception strategies enable an agent to selectively gather information in a way to improve its performance. In applications in which the agent does not have prior knowledge about the available information sources, it is crucial to synthesize active perception strategies at runtime. We consider a setting in which at runtime an agent is capable of gathering information under a limited budget. We pose the problem in the context of partially observable Markov decision processes. We propose a generalized greedy strategy that selects a subset of information sources with near-optimality guarantees on uncertainty reduction. Our theoretical analysis establishes that the proposed active perception strategy achieves near-optimal performance in terms of expected cumulative reward. We demonstrate the resulting strategies in simulations on a robotic navigation problem.

cs.AI↗

arXiv2019

Reactive Synthesis with Maximum Realizability of Linear Temporal Logic Specifications

A challenging problem for autonomous systems is to synthesize a reactive controller that conforms to a set of given correctness properties. Linear temporal logic (LTL) provides a formal language to specify the desired behavioral properties of systems. In applications in which the specifications originate from various aspects of the system design, or consist of a large set of formulas, the overall system specification may be unrealizable. Driven by this fact, we develop an optimization variant of synthesis from LTL formulas, where the goal is to design a controller that satisfies a set of hard specifications and minimally violates a set of soft specifications. To that end, we introduce a value function that, by exploiting the LTL semantics, quantifies the level of violation of properties. Inspired by the idea of bounded synthesis, we fix a bound on the implementation size and search for an implementation that is optimal with respect to the said value function. We propose a novel maximum satisfiability encoding of the search for an optimal implementation (within the given bound on the implementation size). We iteratively increase the bound on the implementation size until a termination criterion, such as a threshold over the value function, is met.

cs.FL↗