Austin Jones

Bo Chen, Kevin Leahy, Austin Jones et al.

Data-driven systems are gathering increasing amounts of data from users, and sensitive user data requires privacy protections. In some cases, the data gathered is non-numerical or symbolic, and conventional approaches to privacy, e.g., adding noise, do not apply, though such systems still require privacy protections. Accordingly, we present a novel differential privacy framework for protecting trajectories generated by symbolic systems. These trajectories can be represented as words or strings over a finite alphabet. We develop new differential privacy mechanisms that approximate a sensitive word using a random word that is likely to be near it. An offline mechanism is implemented efficiently using a Modified Hamming Distance Automaton to generate whole privatized output words over a finite time horizon. Then, an online mechanism is implemented by taking in a sensitive symbol and generating a randomized output symbol at each timestep. This work is extended to Markov chains to generate differentially private state sequences that a given Markov chain could have produced. Statistical accuracy bounds are developed to quantify the accuracy of these mechanisms, and numerical results validate the accuracy of these techniques for strings of English words.

Kevin Leahy, Austin Jones, Cristian-Ioan Vasile

In this work, we focus on decomposing large multi-agent path planning problems with global temporal logic goals (common to all agents) into smaller sub-problems that can be solved and executed independently. Crucially, the sub-problems' solutions must jointly satisfy the common global mission specification. The agents' missions are given as Capability Temporal Logic (CaTL) formulas, a fragment of signal temporal logic, that can express properties over tasks involving multiple agent capabilities (sensors, e.g., camera, IR, and effectors, e.g., wheeled, flying, manipulators) under strict timing constraints. The approach we take is to decompose both the temporal logic specification and the team of agents. We jointly reason about the assignment of agents to subteams and the decomposition of formulas using a satisfiability modulo theories (SMT) approach. The output of the SMT is then distributed to subteams and leads to a significant speed up in planning time. We include computational results to evaluate the efficiency of our solution, as well as the trade-offs introduced by the conservative nature of the SMT encoding.

Austin Jones, Kevin Leahy, Matthew Hale

In this paper, we develop a privacy implementation for symbolic control systems. Such systems generate sequences of non-numerical data, and these sequences can be represented by words or strings over a finite alphabet. This work uses the framework of differential privacy, which is a statistical notion of privacy that makes it unlikely that privatized data will reveal anything meaningful about underlying sensitive data. To bring differential privacy to symbolic control systems, we develop an exponential mechanism that approximates a sensitive word using a randomly chosen word that is likely to be near it. The notion of "near" is given by the Levenshtein distance, which counts the number of operations required to change one string into another. We then develop a Levenshtein automaton implementation of our exponential mechanism that efficiently generates privatized output words. This automaton has letters as its states, and this work develops transition probabilities among these states that give overall output words obeying the distribution required by the exponential mechanism. Numerical results are provided to demonstrate this technique for both strings of English words and runs of a deterministic transition system, demonstrating in both cases that privacy can be provided in this setting while maintaining a reasonable degree of accuracy.

Kasra Yazdani, Austin Jones, Kevin Leahy et al.

As multi-agent systems proliferate and share more user data, new approaches are needed to protect sensitive data while still enabling system operation. To address this need, this paper presents a private multi-agent LQ control framework. Agents' state trajectories can be sensitive and we therefore protect them using differential privacy. We quantify the impact of privacy along three dimensions: the amount of information shared under privacy, the control-theoretic cost of privacy, and the tradeoffs between privacy and performance. These analyses are done in conventional control-theoretic terms, which we use to develop guidelines for calibrating privacy as a function of system parameters. Numerical results indicate that system performance remains within desirable ranges, even under strict privacy requirements.

Derya Aksaray, Austin Jones, Zhaodan Kong et al.

This paper addresses the problem of learning optimal policies for satisfying signal temporal logic (STL) specifications by agents with unknown stochastic dynamics. The system is modeled as a Markov decision process, in which the states represent partitions of a continuous space and the transition probabilities are unknown. We formulate two synthesis problems where the desired STL specification is enforced by maximizing the probability of satisfaction, and the expected robustness degree, that is, a measure quantifying the quality of satisfaction. We discuss that Q-learning is not directly applicable to these problems because, based on the quantitative semantics of STL, the probability of satisfaction and expected robustness degree are not in the standard objective form of Q-learning. To resolve this issue, we propose an approximation of STL synthesis problems that can be solved via Q-learning, and we derive some performance bounds for the policies obtained by the approximate approach. The performance of the proposed method is demonstrated via simulations.

Austin Jones, Derya Aksaray, Zhaodan Kong et al.

We consider the problem of steering a system with unknown, stochastic dynamics to satisfy a rich, temporally layered task given as a signal temporal logic formula. We represent the system as a Markov decision process in which the states are built from a partition of the state space and the transition probabilities are unknown. We present provably convergent reinforcement learning algorithms to maximize the probability of satisfying a given formula and to maximize the average expected robustness, i.e., a measure of how strongly the formula is satisfied. We demonstrate via a pair of robot navigation simulation case studies that reinforcement learning with robustness maximization performs better than probability maximization in terms of both probability of satisfaction and expected robustness.

Austin Jones, Mac Schwager, Calin Belta

We present a new temporal logic called Distribution Temporal Logic (DTL) defined over predicates of belief states and hidden states of partially observable systems. DTL can express properties involving uncertainty and likelihood that cannot be described by existing logics. A co-safe formulation of DTL is defined and algorithmic procedures are given for monitoring executions of a partially observable Markov decision process with respect to such formulae. A simulation case study of a rescue robotics application outlines our approach.

Austin Jones, Mac Schwager, Calin Belta

This technical report is an extended version of the paper 'A Receding Horizon Algorithm for Informative Path Planning with Temporal Logic Constraints' accepted to the 2013 IEEE International Conference on Robotics and Automation (ICRA). This paper considers the problem of finding the most informative path for a sensing robot under temporal logic constraints, a richer set of constraints than have previously been considered in information gathering. An algorithm for informative path planning is presented that leverages tools from information theory and formal control synthesis, and is proven to give a path that satisfies the given temporal logic constraints. The algorithm uses a receding horizon approach in order to provide a reactive, on-line solution while mitigating computational complexity. Statistics compiled from multiple simulation studies indicate that this algorithm performs better than a baseline exhaustive search approach.