Sriram Sankaranarayanan

Engg. Center ECOT 717
University of Colorado Boulder
Boulder, CO 80309-0430
Phone: (303) 492 6580

I am a professor in the Computer Science department at the University of Colorado at Boulder.

My research focuses on areas of programming languages & verification and cyber-physical systems. I work on fundamental problems involving modeling and analysis of autonomous cyber-physical systems with applications to artificial pancreas systems for treating type-1 diabetes, runtime monitoring for autonomous vehicles and interactions between humans and autonomous systems.

As a faculty member, I teach a variety of courses in the areas of programming languages, algorithms, mathematical optimization and specialized courses pertinent to my research areas. I also serve as an associate chair for undergraduate education jointly with Ioana Fleming.

I have been faculty at CU Boulder since 2009. Previously, I was a member of research staff at NEC Laboratories America from 2005-2009. I graduated with a PhD in (theoretical) Computer Science from Stanford University in 2005. Here is a link to a brief biography.

news

Jul 19, 2021	Invited talk on ``game based predictive runtime monitoring’’ at the https://workshops.inf.ed.ac.uk/SYNT2021/program.html.
Jul 9, 2021	Chou Yi successfully defended her PhD dissertation titled: ``Bayesian parameter estimation for nonlinear dynamics’’. Congratulations Dr. Yi Chou!

selected publications

Probabilistic Specification Learning for Planning with Safety Constraints

Kandai Watanabe, Nicholas Renninger, Sriram Sankaranarayanan, and Morteza Lahijanian

In Intelligent Robots and Systems (IROS), pp. TBA, 2021.
Note: To Appear.

Abs Bib URL

This paper proposes a framework for learning task specifications from demonstrations, while ensuring that the learned specifications do not violate safety constraints. Furthermore, we show how these specifications can be used in a planning problem to control the robot under environments that can be different from those encountered during the learning phase. We formulate the specification learning problem as a grammatical inference problem, using probabilistic automata to represent specifications. The edge probabilities of the resulting automata represent the demonstrator’s preferences. The main novelty in our approach is to incorporate the safety property during the learning process. We prove that the resulting automaton always respects a pre-specified safety property, and furthermore, the proposed method can easily be included in any Evidence-Driven State Merging (EDSM)-based automaton learning scheme. Finally, we introduce a planning algorithm that produces the most desirable plan by maximizing the probability of an accepting trace of the automaton. Case studies show that our algorithm learns the true probability distribution most accurately while maintaining safety. Since, specification is detached from the robot’s environment model, a satisfying plan can be synthesized for a variety of different robots and environments including both mobile robots and manipulators.
@inproceedings{ Watanabe+Others/2021/Probabilistic, title = { Probabilistic Specification Learning for Planning with Safety Constraints }, author = { Watanabe, Kandai and Renninger, Nicholas and Sankaranarayanan, Sriram and Lahijanian, Morteza }, booktitle= { Intelligent Robots and Systems (IROS) }, year = { 2021 }, publisher = { IEEE }, pages = { TBA }, numpages = { 8 }, }
Predictive Runtime Monitoring for Mobile Robots using Logic-Based Bayesian Intent Inference

Hansol Yoon, and Sriram Sankaranarayanan

In International Conference on Robotics and Automation (ICRA), pp. TBA, 2021.
Note: Cf. here for a video demo .

Abs Bib URL

We propose a predictive runtime monitoring framework that forecasts the distribution of future positions of mobile robots in order to detect and avoid impending property violations such as collisions with obstacles or other agents. Our approach uses a restricted class of temporal logic formulas to represent the likely intentions of the agents along with a combination of temporal logic-based optimal cost path planning and Bayesian inference to compute the probability of these intents given the current trajectory of the robot. First, we construct a large but finite hypothesis space of possible intents represented as temporal logic formulas whose atomic propositions are derived from a detailed map of the robot’s workspace. Next, our approach uses real-time observations of the robot’s position to update a distribution over temporal logic formulae that represent its likely intent. This is performed by using a combination of optimal cost path planning and a Boltzmann noisy rationality model. In this manner, we construct a Bayesian approach to evaluating the posterior probability of various hypotheses given the observed states and actions of the robot. Finally, we predict the future position of the robot by drawing posterior predictive samples using a Monte-Carlo method. We evaluate our framework using two different trajectory datasets that contain multiple scenarios implementing various tasks. The results show that our method can predict future positions precisely and efficiently, so that the computation time for generating a prediction is a tiny fraction of the overall time horizon.
@inproceedings{ Yoon+Sankaranarayanan/2021/Predictive, title = { Predictive Runtime Monitoring for Mobile Robots using Logic-Based Bayesian Intent Inference }, author = { Yoon, Hansol and Sankaranarayanan, Sriram }, booktitle= { International Conference on Robotics and Automation (ICRA) }, year = { 2021 }, publisher = { IEEE }, pages = { TBA }, numpages = { 7 }, }
Reasoning about Uncertainties in Discrete-Time Dynamical Systems using Polynomial Forms

Sriram Sankaranarayanan, Yi Chou, Eric Goubault, and Sylvie Putot

In Advances in Neural Information Processing System (NeurIPS), 2020.

Abs Bib URL Supp

In this paper, we propose polynomial forms to represent distributions of state variables over time for discrete-time stochastic dynamical systems. This problem arises in a variety of applications in areas ranging from biology to robotics. Our approach allows us to rigorously represent the probability distribution of state variables over time, and provide guaranteed bounds on the expectations, moments and probabilities of tail events involving the state variables. First, we recall ideas from interval arithmetic, and use them to rigorously represent the state variables at time t as a function of the initial state variables and noise symbols that model the random exogenous inputs encountered before time t. Next, we show how concentration of measure inequalities can be employed to prove rigorous bounds on the tail probabilities of these state variables. We demonstrate interesting applications that demonstrate how our approach can be useful in some situations to establish mathematically guaranteed bounds that are of a different nature from those obtained through simulations with pseudo-random numbers.
@inproceedings{ Sankaranarayanan+Others/2020/Uncertainty, title = { Reasoning about Uncertainties in Discrete-Time Dynamical Systems using Polynomial Forms }, author = { Sankaranarayanan, Sriram and Chou, Yi and Goubault, Eric and Putot, Sylvie }, booktitle= { Advances in Neural Information Processing System (NeurIPS) }, year = { 2020 }, publisher = { Curran Associates }, numpages = { 13 }, }
Cf. Code and Examples
Predictive Runtime Monitoring of Vehicle Models Using Bayesian Estimation and Reachability Analysis

Yi Chou, Hansol Yoon, and Sriram Sankaranarayanan

In Intl. Conference on Intelligent Robots and Systems (IROS), pp. 2111-2118, 2020.

Abs Bib URL

We present a predictive runtime monitoring technique for estimating future vehicle positions and the probability of collisions with obstacles. Vehicle dynamics model how the position and velocity change over time as a function of external inputs. They are commonly described by discrete-time stochastic models. Whereas positions and velocities can be measured, the inputs (steering and throttle) are not directly measurable in these models. In our paper, we apply Bayesian inference techniques for real-time estimation, given prior distribution over the unknowns and noisy state measurements. Next, we pre-compute the set-valued reachability analysis to approximate future positions of a vehicle. The pre-computed reachability sets are combined with the posterior probabilities computed through Bayesian estimation to provided a predictive verification framework that can be used to detect impending collisions with obstacles. Our approach is evaluated using the coordinated-turn vehicle model for a UAV using on-board measurement data obtained from a flight test of a Talon UAV. We also compare the results with sampling-based approaches. We find that precomputed reachability analysis can provide accurate warnings up to 6 seconds in advance and the accuracy of the warnings improve as the time horizon is narrowed from 6 to 2 seconds. The approach also outperforms sampling in terms of on-board computation cost and accuracy measures.
@inproceedings{ Chou+Yoon+Sankaranarayanan/2020/Predictive, title = { Predictive Runtime Monitoring of Vehicle Models Using Bayesian Estimation and Reachability Analysis }, author = { Chou, Yi and Yoon, Hansol and Sankaranarayanan, Sriram }, booktitle= { Intl. Conference on Intelligent Robots and Systems (IROS) }, year = { 2020 }, publisher = { IEEE Press }, pages = { 2111-2118 }, }
Quantitative Analysis of Programs with Probabilities and Concentration of Measure Inequalities

Sriram Sankaranarayanan

In Foundations of Probabilistic Programming (Editors: Gilles Barthe, Joost-Pieter Katoen, and Alexandra Silva), 2020.

Abs Bib URL

The quantitative analysis of probabilistic programs answers queries involving the expected values of program variables and expressions involving them, as well as bounds on the probabilities of assertions. In this chapter, we will present the use of concentration of measure inequalities to reason about such bounds. First, we will briefly present and motivate standard concentration of measure inequalities. Next, we survey approaches to reason about quantitative properties using concentration of measure inequalities, illustrating these on numerous motivating examples. Finally, we discuss currently open challenges in this area for future work.
@inproceedings{ Sankaranaranyanan/2020/Concentration, title = { Quantitative Analysis of Programs with Probabilities and Concentration of Measure Inequalities }, author = { Sankaranarayanan, Sriram }, booktitle= { Foundations of Probabilistic Programming (Editors: Gilles Barthe, Joost-Pieter Katoen, and Alexandra Silva) }, year = { 2020 }, publisher = { Cambridge University Press }, numpages = { 30 }, }
Reachability Analysis using Message Passing over Tree Decompositions.

Sriram Sankaranarayanan

In International Conference on Computer-Aided Verification (CAV), Lecture Notes in Computer Science (LNCS) Vol. 12224, pp. 604–628, 2020.

Abs Bib URL

In this paper, we study efficient approaches to reachability analysis for discrete-time nonlinear dynamical systems when the dependencies among the variables of the system have low treewidth. Reachability analysis over nonlinear dynamical systems asks if a given set of target states can be reached, starting from an initial set of states. This is solved by computing conservative over approximations of the reachable set using abstract domains to represent these approximations. However, most approaches must tradeoff the level of conservatism against the cost of performing analysis, especially when the number of system variables increases. This makes reachability analysis challenging for nonlinear systems with a large number of state variables. Our approach works by constructing a dependency graph among the variables of the system. The tree decomposition of this graph builds a tree wherein each node of the tree is labeled with subsets of the state variables of the system. Furthermore, the tree decomposition satisfies important structural properties. Using the tree decomposition, our approach abstracts a set of states of the high dimensional system into a tree of sets of lower dimensional projections of this state. We derive various properties of this abstract domain, including conditions under which the original high dimensional set can be fully recovered from its low dimensional projections. Next, we use ideas from message passing developed originally for belief propagation over Bayesian networks to perform reachability analysis over the full state space in an efficient manner. We illustrate our approach on some interesting nonlinear systems with low treewidth to demonstrate the advantages of our approach.
@inproceedings{ Sankaranarayanan/2020/Tree, title = { Reachability Analysis using Message Passing over Tree Decompositions. }, author = { Sankaranarayanan, Sriram }, booktitle= { International Conference on Computer-Aided Verification (CAV) }, year = { 2020 }, publisher = { Springer }, pages = { 604–628 }, series = { Lecture Notes in Computer Science (LNCS) }, volume = { 12224 }, }