More Like this

1. Probably Approximate Safety Verification of Hybrid Dynamical Systems

   https://doi.org/10.1007/978-3-030-32409-4_15  

   Xue, Bai; Fränzle, Martin; Zhao, Hengjun; Zhan, Naijun; Easwaran, Arvind (January 2019, International Conference on Formal Engineering Methods)

   In this paper we present a method based on linear programming that facilitates reliable safety verification of hybrid dynamical systems subject to perturbation inputs over the infinite time horizon. The verification algorithm applies the probably approximately correct (PAC) learning framework and consequently can be regarded as statistically formal verification in the sense that it provides formal safety guarantees expressed using error probabilities and confidences. The safety of hybrid systems in this framework is verified via the computation of so-called PAC barrier certificates, which can be computed by solving a linear programming problem. Based on scenario approaches, the linear program is constructed by a family of independent and identically distributed state samples. In this way we can conduct verification of hybrid dynamical systems that existing methods are not capable of dealing with. Some preliminary experiments demonstrate the performance of our approach. 

   more » « less
2. Toeplitz quotient C*-algebras and ratio limits for random walks

   Dor-On, Adam (January 2021, Documenta mathematica)

   We study quotients of the Toeplitz C*-algebra of a random walk, similar to those studied by the author and Markiewicz for finite stochastic matrices. We introduce a new Cuntz-type quotient C*-algebra for random walks that have convergent ratios of transition probabilities. These C*-algebras give rise to new notions of ratio limit space and boundary for such random walks, which are computed by appealing to a companion paper by Woess. Our combined results are leveraged to identify a unique symmetry-equivariant quotient C*-algebra for any symmetric random walk on a hyperbolic group, shedding light on a question of Viselter on C*-algebras of subproduct systems. 

   more » « less
3. Verifiable Obstacle Detection

   https://doi.org/10.1109/ISSRE55969.2022.00017  

   Bansal, Ayoosh; Kim, Hunmin; Yu, Simon; Li, Bo; Hovakimyan, Naira; Caccamo, Marco; Sha, Lui (October 2022, Verifiable Obstacle Detection)

   Perception of obstacles remains a critical safety concern for autonomous vehicles. Real-world collisions have shown that the autonomy faults leading to fatal collisions originate from obstacle existence detection. Open source autonomous driving implementations show a perception pipeline with complex interdependent Deep Neural Networks. These networks are not fully verifiable, making them unsuitable for safety-critical tasks. In this work, we present a safety verification of an existing LiDAR based classical obstacle detection algorithm. We establish strict bounds on the capabilities of this obstacle detection algorithm. Given safety standards, such bounds allow for determining LiDAR sensor properties that would reliably satisfy the standards. Such analysis has as yet been unattainable for neural network based perception systems. We provide a rigorous analysis of the obstacle detection s 

   more » « less
4. Modelchecking Safety Properties in Randomized Security Protocols. In: Nigam V. et al. (eds) Logic, Language, and Security.

   https://doi.org/10.1007/978-3-030-62077-6_12  

   Bauer, Matt S; Chadha, Rohit; Viswanathan, Mahesh (October 2020, Logic, Language, and Security (Lecture Notes in Computer Science))

   null (Ed.)

   Automated reasoning tools for security protocols model protocols as non-deterministic processes that communicate through a Dolev-Yao attacker. There are, however, a large class of protocols whose correctness relies on an explicit ability to model and reason about randomness. Although such protocols lie at the heart of many widely adopted systems for anonymous communication, they have so-far eluded automated verification techniques. We propose an algorithm for reasoning about safety properties for randomized protocols. The algorithm is implemented as an extension of Stochastic Protocol ANalyzer (Span), the mechanized tool that reasons about the indistinguishability properties of randomized protocols. Using Span, we conduct the first automated verification on several randomized security protocols and uncover previously unknown design weaknesses in several of the protocols we analyzed. 

   more » « less
5. Generalizing Convolutional Neural Networks for Equivarianceto Lie Groups on Arbitrary Continuous Data

   Finzi, M; Stanton, S; Izmailov, P; Wilson, A.G. (January 2020, International Conference on Machine Learning)

   The translation equivariance of convolutional layers enables convolutional neural networks to generalize well on image problems. While translation equivariance provides a powerful inductive bias for images, we often additionally desire equivariance to other transformations, such as rotations, especially for non-image data. We propose a general method to construct a convolutional layer that is equivariant to transformations from any specified Lie group with a surjective exponential map. Incorporating equivariance to a new group requires implementing only the group exponential and logarithm maps, enabling rapid prototyping. Showcasing the simplicity and generality of our method, we apply the same model architecture to images, ball-and-stick molecular data, and Hamiltonian dynamical systems. For Hamiltonian systems, the equivariance of our models is especially impactful, leading to exact conservation of linear and angular momentum. 

   more » « less