Sriram Sankaranarayanan

selected publications

1. Decoding Output Sequences for Discrete-Time Linear Hybrid Systems

   Monal Narasimhamurthy, and Sriram Sankaranarayanan

   In ACM International Conference on Hybrid Systems: Computation and Control (HSCC), pp. 6:1–6:7, 2022.

   Abs Bib URL

   In this paper, we study the "decoding" problem for discrete-time, stochastic hybrid systems with linear dynamics in each mode. Given an output trace of the system, the decoding problem seeks to construct a sequence of modes and states that yield a trace "as close as possible" to the original output trace. The decoding problem generalizes the state estimation problem, and is applicable to hybrid systems with non-determinism. The decoding problem is NP-complete, and can be reduced to solving a mixed-integer linear program (MILP). In this paper, we decompose the decoding problem into two parts: (a) finding a sequence of discrete modes and transitions; and (b) finding corresponding continuous states for the mode/transition sequence. In particular, once a sequence of modes/transitions is fixed, the problem of "filling in" the continuous states is performed by a linear programming problem. In order to support the decomposition, we "cover" the set of all possible mode/transition sequences by a finite subset. We use well-known probabilistic arguments to justify a choice of cover with high confidence and design randomized algorithms for finding such covers. Our approach is demonstrated on a series of benchmarks, wherein we observe that relatively tiny fraction of the possible mode/transition sequences can be used as a cover. Furthermore, we show that the resulting linear programs can be solved rapidly by exploiting the tree structure of the set cover.

           @inproceedings{ Narasimhamurthy+Sankaranarayanan/2022/Decoding,
           title = { Decoding Output Sequences for Discrete-Time Linear Hybrid Systems },
           author = {   Narasimhamurthy, Monal  and    Sankaranarayanan, Sriram   },
           booktitle= {  ACM International Conference on Hybrid Systems:
                  Computation and Control (HSCC) },  
           year = { 2022 },  
           publisher = { ACM }, 
           pages = { 6:1–6:7 }, 
           
           
           
           
           
           }
           

2. Static Analysis of ReLU Neural Networks with Tropical Polyhedra

   Eric Goubault, Sebastien Palumby, Sylvie Putot, Louis Rustenholz, and Sriram Sankaranarayanan

   In Static Analysis Symposium (SAS), Lecture Notes in Computer Science Vol. 12913, pp. 166–190, 2021.

   Abs Bib URL

   This paper studies the problem of range analysis for feedforward neural networks, which is a basic primitive for applications such as robustness of neural networks, compliance to specifications and reachability analysis of neural-network feedback systems. Our approach focuses on ReLU (rectified linear unit) feedforward neural nets that present specific difficulties: approaches that exploit derivatives do not apply in general, the number of patterns of neuron activations can be quite large even for small networks, and convex approximations are generally too coarse. In this paper, we employ set-based methods and abstract interpretation that have been very successful in coping with similar difficulties in classical program verification. We present an approach that abstracts ReLU feedforward neural networks using tropical polyhedra. We show that tropical polyhedra can efficiently abstract ReLU activation function, while being able to control the loss of precision due to linear computations. We show how the connection between ReLU networks and tropical rational functions can provide approaches for range analysis of ReLU neural networks.

           @inproceedings{ Goubault+Others/2021/Static,
           title = { Static Analysis of ReLU Neural Networks with Tropical Polyhedra },
           author = {   Goubault, Eric  and    Palumby, Sebastien  and    Putot, Sylvie  and    Rustenholz, Louis  and    Sankaranarayanan, Sriram   },
           booktitle= { Static Analysis Symposium (SAS) },  
           year = { 2021 },  
           publisher = { Springer }, 
           pages = { 166–190 }, 
           
           series = { Lecture Notes in Computer Science },  
           volume = { 12913 },  
           
           
           }
           

3. 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

4. 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 },  
           
           
           
           
           }
           

5. 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 },  
           
           
           }