arXiv subjects

Ufuk Topcu

Publications and source records attributed to Ufuk Topcu.

At least 307 records · Page 17Linked to original sources

arXiv2019

Incentive Design for Temporal Logic Objectives

We study the problem of designing an optimal sequence of incentives that a principal should offer to an agent so that the agent's optimal behavior under the incentives realizes the principal's objective expressed as a temporal logic formula. We consider an agent with a finite decision horizon and model its decision-making process as a Markov decision process (MDP). Under certain assumptions, we present a polynomial-time algorithm to synthesize an incentive sequence that minimizes the cost to the principal. We show that if the underlying MDP has only deterministic transitions, the principal can hide its objective from the agent and still realize the desired behavior through incentives. On the other hand, an MDP with stochastic transitions may require the principal to share its objective with the agent. Finally, we demonstrate the proposed method in motion planning examples where a principal changes the optimal trajectory of an agent by providing incentives.

math.OC↗

arXiv2019

Training Classifiers For Feedback Control

One approach for feedback control using high dimensional and rich sensor measurements is to classify the measurement into one out of a finite set of situations, each situation corresponding to a (known) control action. This approach computes a control action without estimating the state. Such classifiers are typically learned from a finite amount of data using supervised machine learning algorithms. We model the closed-loop system resulting from control with feedback from classifier outputs as a piece-wise affine differential inclusion. We show how to train a linear classifier based on performance measures related to learning from data and the local stability properties of the resulting closed-loop system. The training method is based on the projected gradient descent algorithm. We demonstrate the advantage of training classifiers using control-theoretic properties on a case study involving navigation using range-based sensors.

math.OC↗

arXiv2019

Toward Achieving Formal Guarantees for Human-Aware Controllers in Human-Robot Interactions

With the primary objective of human-robot interaction being to support humans' goals, there exists a need to formally synthesize robot controllers that can provide the desired service. Synthesis techniques have the benefit of providing formal guarantees for specification satisfaction. There is potential to apply these techniques for devising robot controllers whose specifications are coupled with human needs. This paper explores the use of formal methods to construct human-aware robot controllers to support the productivity requirements of humans. We tackle these types of scenarios via human workload-informed models and reactive synthesis. This strategy allows us to synthesize controllers that fulfill formal specifications that are expressed as linear temporal logic formulas. We present a case study in which we reason about a work delivery and pickup task such that the robot increases worker productivity, but not stress induced by high work backlog. We demonstrate our controller using the Toyota HSR, a mobile manipulator robot. The results demonstrate the realization of a robust robot controller that is guaranteed to properly reason and react in collaborative tasks with human partners.

cs.RO↗

arXiv2019

Distributed Synthesis of Surveillance Strategies for Mobile Sensors

We study the problem of synthesizing strategies for a mobile sensor network to conduct surveillance in partnership with static alarm triggers. We formulate the problem as a multi-agent reactive synthesis problem with surveillance objectives specified as temporal logic formulas. In order to avoid the state space blow-up arising from a centralized strategy computation, we propose a method to decentralize the surveillance strategy synthesis by decomposing the multi-agent game into subgames that can be solved independently. We also decompose the global surveillance specification into local specifications for each sensor, and show that if the sensors satisfy their local surveillance specifications, then the sensor network as a whole will satisfy the global surveillance objective. Thus, our method is able to guarantee global surveillance properties in a mobile sensor network while synthesizing completely decentralized strategies with no need for coordination between the sensors. We also present a case study in which we demonstrate an application of decentralized surveillance strategy synthesis.

cs.AI↗

arXiv2018

Robust Myopic Control for Systems with Imperfect Observations

Control of systems operating in unexplored environments is challenging due to lack of complete model knowledge. Additionally, under measurement noises, data collected from onboard sensors are of limited accuracy. This paper considers imperfect state observations in developing a control strategy for systems moving in unknown environments. First, we include hard constraints in the problem for safety concerns. Given the observed states, the robust myopic control approach learns local dynamics, explores all possible trajectories within the observation error bound, and computes the optimal control action using robust optimization. Finally, we validate the method in an OSIRIS-REx-based asteroid landing scenario.

eess.SY↗

arXiv2018

Information-Guided Temporal Logic Inference with Prior Knowledge

This paper investigates the problem of inferring knowledge from data so that the inferred knowledge is interpretable and informative to humans who have prior knowledge. Given a dataset as a collection of system trajectories, we infer parametric linear temporal logic (pLTL) formulas that are informative and satisfied by the trajectories in the dataset with high probability. The informativeness of the inferred formula is measured by the information gain with respect to given prior knowledge represented by a prior probability distribution. We first present two algorithms to compute the information gain with a focus on two types of prior probability distributions: stationary probability distributions and probability distributions expressed by discrete time Markov chains. Then we provide a method to solve the inference problem for a subset of pLTL formulas with polynomial time complexity with respect to the number of Boolean connectives in the formula. We provide implementations of the proposed approach on explaining anomalous patterns, patterns changes and explaining the policies of Markov decision processes.

cs.LO↗

arXiv2018

The Partially Observable Games We Play for Cyber Deception

Progressively intricate cyber infiltration mechanisms have made conventional means of defense, such as firewalls and malware detectors, incompetent. These sophisticated infiltration mechanisms can study the defender's behavior, identify security caveats, and modify their actions adaptively. To tackle these security challenges, cyber-infrastructures require active defense techniques that incorporate cyber deception, in which the defender (deceiver) implements a strategy to mislead the infiltrator. To this end, we use a two-player partially observable stochastic game (POSG) framework, wherein the deceiver has full observability over the states of the POSG, and the infiltrator has partial observability. Then, the deception problem is to compute a strategy for the deceiver that minimizes the expected cost of deception against all strategies of the infiltrator. We first show that the underlying problem is a robust mixed-integer linear program, which is intractable to solve in general. Towards a scalable approach, we compute optimal finite-memory strategies for the infiltrator by a reduction to a series of synthesis problems for parametric Markov decision processes. We use these infiltration strategies to find robust strategies for the deceiver using mixed-integer linear programming. We illustrate the performance of our technique on a POSG model for network security. Our experiments demonstrate that the proposed approach handles scenarios considerably larger than those of the state-of-the-art methods.

cs.AI↗

arXiv2018

Cost-Bounded Active Classification Using Partially Observable Markov Decision Processes

Active classification, i.e., the sequential decision-making process aimed at data acquisition for classification purposes, arises naturally in many applications, including medical diagnosis, intrusion detection, and object tracking. In this work, we study the problem of actively classifying dynamical systems with a finite set of Markov decision process (MDP) models. We are interested in finding strategies that actively interact with the dynamical system, and observe its reactions so that the true model is determined efficiently with high confidence. To this end, we present a decision-theoretic framework based on partially observable Markov decision processes (POMDPs). The proposed framework relies on assigning a classification belief (a probability distribution) to each candidate MDP model. Given an initial belief, some misclassification probabilities, a cost bound, and a finite time horizon, we design POMDP strategies leading to classification decisions. We present two different approaches to find such strategies. The first approach computes the optimal strategy "exactly" using value iteration. To overcome the computational complexity of finding exact solutions, the second approach is based on adaptive sampling to approximate the optimal probability of reaching a classification decision. We illustrate the proposed methodology using two examples from medical diagnosis and intruder detection.

eess.SY↗

arXiv2018

Transfer Entropy in MDPs with Temporal Logic Specifications

Emerging applications in autonomy require control techniques that take into account uncertain environments, communication and sensing constraints, while satisfying highlevel mission specifications. Motivated by this need, we consider a class of Markov decision processes (MDPs), along with a transfer entropy cost function. In this context, we study highlevel mission specifications as co-safe linear temporal logic (LTL) formulae. We provide a method to synthesize a policy that minimizes the weighted sum of the transfer entropy and the probability of failure to satisfy the specification. We derive a set of coupled non-linear equations that an optimal policy must satisfy. We then use a modified Arimoto-Blahut algorithm to solve the non-linear equations. Finally, we demonstrated the proposed method on a navigation and path planning scenario of a Mars rover.

eess.SY↗

arXiv2018

Least Inferable Policies for Markov Decision Processes

In a variety of applications, an agent's success depends on the knowledge that an adversarial observer has or can gather about the agent's decisions. It is therefore desirable for the agent to achieve a task while reducing the ability of an observer to infer the agent's policy. We consider the task of the agent as a reachability problem in a Markov decision process and study the synthesis of policies that minimize the observer's ability to infer the transition probabilities of the agent between the states of the Markov decision process. We introduce a metric that is based on the Fisher information as a proxy for the information leaked to the observer and using this metric formulate a problem that minimizes expected total information subject to the reachability constraint. We proceed to solve the problem using convex optimization methods. To verify the proposed method, we analyze the relationship between the expected total information and the estimation error of the observer, and show that, for a particular class of Markov decision processes, these two values are inversely proportional.

math.OC↗

arXiv2018

Graph-Based Controller Synthesis for Safety-Constrained, Resilient Systems

Resilience to damage, component degradation, and adversarial action is a critical consideration in design of autonomous systems. In addition to designing strategies that seek to prevent such negative events, it is vital that an autonomous system remains able to achieve its control objective even if the system partially loses control authority. While loss of authority limits the system's control capabilities, it may be possible to use the remaining authority in such a way that the system's control objectives remain achievable. In this paper, we consider the problem of optimal design for an autonomous system with discrete-time linear dynamics where the available control actions depend on adversarial input produced as a result of loss of authority. The central question is how to partition the set of control inputs that the system can apply in such a way that the system state remains within a safe set regardless of an adversarial input limiting the available control inputs to a single partition elements. We interpret such a problem first as a variant of a safety game, and then as a problem of existence of an appropriate edge labeling on a graph. We obtain conditions for existence and a computationally efficient algorithm for determining a system design and a control policy that preserve system safety. We illustrate our results on two examples: a damaged autonomous vehicle and a method of communication over a channel that ensures a minimal running digital sum.

math.OC↗

arXiv2018

Synthesis in pMDPs: A Tale of 1001 Parameters

This paper considers parametric Markov decision processes (pMDPs) whose transitions are equipped with affine functions over a finite set of parameters. The synthesis problem is to find a parameter valuation such that the instantiated pMDP satisfies a specification under all strategies. We show that this problem can be formulated as a quadratically-constrained quadratic program (QCQP) and is non-convex in general. To deal with the NP-hardness of such problems, we exploit a convex-concave procedure (CCP) to iteratively obtain local optima. An appropriate interplay between CCP solvers and probabilistic model checkers creates a procedure --- realized in the open-source tool PROPhESY --- that solves the synthesis problem for models with thousands of parameters.

cs.AI↗

arXiv2018

Randomized Greedy Sensor Selection: Leveraging Weak Submodularity

We study the problem of estimating a random process from the observations collected by a network of sensors that operate under resource constraints. When the dynamics of the process and sensor observations are described by a state-space model and the resource are unlimited, the conventional Kalman filter provides the minimum mean-square error (MMSE) estimates. However, at any given time, restrictions on the available communications bandwidth and computational capabilities and/or power impose a limitation on the number of network nodes whose observations can be used to compute the estimates. We formulate the problem of selecting the most informative subset of the sensors as a combinatorial problem of maximizing a monotone set function under a uniform matroid constraint. For the MMSE estimation criterion we show that the maximum element-wise curvature of the objective function satisfies a certain upper-bound constraint and is, therefore, weak submodular. We develop an efficient randomized greedy algorithm for sensor selection and establish guarantees on the estimator's performance in this setting. Extensive simulation results demonstrate the efficacy of the randomized greedy algorithm compared to state-of-the-art greedy and semidefinite programming relaxation methods.

eess.SP↗

arXiv2018

Structured Synthesis for Probabilistic Systems

We introduce the concept of structured synthesis for Markov decision processes where the structure is induced from finitely many pre-specified options for a system configuration. The resulting synthesis problem is in general a nonlinear programming problem (NLP) with integer variables. As solving NLPs is in general not feasible, we present an alternative approach. We present a transformation of models specified in the {PRISM} probabilistic programming language to models that account for all possible system configurations by means of nondeterministic choices. Together with a control module that ensures consistent configurations throughout the system, this transformation enables the use of optimized tools for model checking in a black-box fashion. While this transformation increases the size of a model, experiments with standard benchmarks show that the method provides a feasible approach for structured synthesis. Moreover, we demonstrate the usefulness along a realistic case study involving surveillance by unmanned aerial vehicles in a shipping facility.

cs.SE↗

arXiv2018

Verification of Uncertain POMDPs Using Barrier Certificates

We consider a class of partially observable Markov decision processes (POMDPs) with uncertain transition and/or observation probabilities. The uncertainty takes the form of probability intervals. Such uncertain POMDPs can be used, for example, to model autonomous agents with sensors with limited accuracy, or agents undergoing a sudden component failure, or structural damage [1]. Given an uncertain POMDP representation of the autonomous agent, our goal is to propose a method for checking whether the system will satisfy an optimal performance, while not violating a safety requirement (e.g. fuel level, velocity, and etc.). To this end, we cast the POMDP problem into a switched system scenario. We then take advantage of this switched system characterization and propose a method based on barrier certificates for optimality and/or safety verification. We then show that the verification task can be carried out computationally by sum-of-squares programming. We illustrate the efficacy of our method by applying it to a Mars rover exploration example.

eess.SY↗

arXiv2018

Deception in Optimal Control

In this paper, we consider an adversarial scenario where one agent seeks to achieve an objective and its adversary seeks to learn the agent's intentions and prevent the agent from achieving its objective. The agent has an incentive to try to deceive the adversary about its intentions, while at the same time working to achieve its objective. The primary contribution of this paper is to introduce a mathematically rigorous framework for the notion of deception within the context of optimal control. The central notion introduced in the paper is that of a belief-induced reward: a reward dependent not only on the agent's state and action, but also adversary's beliefs. Design of an optimal deceptive strategy then becomes a question of optimal control design on the product of the agent's state space and the adversary's belief space. The proposed framework allows for deception to be defined in an arbitrary control system endowed with a reward function, as well as with additional specifications limiting the agent's control policy. In addition to defining deception, we discuss design of optimally deceptive strategies under uncertainties in agent's knowledge about the adversary's learning process. In the latter part of the paper, we focus on a setting where the agent's behavior is governed by a Markov decision process, and show that the design of optimally deceptive strategies under lack of knowledge about the adversary naturally reduces to previously discussed problems in control design on partially observable or uncertain Markov decision processes. Finally, we present two examples of deceptive strategies: a "cops and robbers" scenario and an example where an agent may use camouflage while moving. We show that optimally deceptive strategies in such examples follow the intuitive idea of how to deceive an adversary in the above settings.

math.OC↗

arXiv2018

Affine Multiplexing Networks: System Analysis, Learning, and Computation

We introduce a novel architecture and computational framework for formal, automated analysis of systems with a broad set of nonlinearities in the feedback loop, such as neural networks, vision controllers, switched systems, and even simple programs. We call this computational structure an affine multiplexing network (AMN). The architecture is based on interconnections of two basic conceptual building blocks: multiplexers ($μ$), and affine transformations ($α$). When attached together appropriately, these building blocks translate to conjunctions and disjunctions of affine statements, resulting in an encoding of the network into satisfiability modulo theory (SMT), mixed integer programming, and sequential convex optimization solvers. We show how to formulate and verify system properties like stability and robustness, how to compute margins, and how to verify performance through a sequence of SMT queries. As illustration, we use the framework to verify closed loop, possibly nonlinear dynamical systems that contain neural networks in the loop, and hint at a number of extensions that can make AMNs a potent playground for interfacing between machine learning, control, convex and nonconvex optimization, and formal methods.

math.OC↗

arXiv2018

Privacy Verification in POMDPs via Barrier Certificates

Privacy is an increasing concern in cyber-physical systems that operates over a shared network. In this paper, we propose a method for privacy verification of cyber- physical systems modeled by Markov decision processes (MDPs) and partially-observable Markov decision processes (POMDPs) based on barrier certificates. To this end, we consider an opacity-based notion of privacy, which is characterized by the beliefs in system states. We show that the belief update equations can be represented as discrete-time switched systems, for which we propose a set of conditions for privacy verification in terms of barrier certificates. We further demonstrate that, for MDPs and for POMDPs, privacy verification can be computationally implemented by solving a set of semi-definite programs and sum-of-squares programs, respectively. The method is illustrated by an application to privacy verification of an inventory management system.

eess.SY↗