Abstract: Probabilistic systems are often modeled as factored Markov decision processes (MDPs), where the states are composed out of the local states of components and each transition involves only a small subset of the components. To exploit the concurrency that arises naturally in such systems, we formulate, as a first step, a restricted class of factored MDPs called Causally Deterministic Factored MDPs (CMDPs, for short). We use this model to port several basic notions from concurrency theory to the framework of factored MDPs. In particular, we provide a concurrent semantics for CMDPs based on the classical notion of event structures. Then using this semantics, we show that local reachability properties of CMDPs can be computed efficiently using a greedy strategy. Finally, we implement our ideas in a prototype and apply it to four models, confirming the potential for substantial improvements over state-of-the-art methods.

This is joint work with S. Akshay and Tobias Meggendorfer.

Abstract: AI-based components have become integral to Cyber-Physical Systems (CPS), enabling transformative functionalities across various domains including transportation, energy, and medicine. Specifically, machine learning components are now widely used for perception, control, and decision-making in safety-critical applications, necessitating rigorous verification methods to ensure safe deployment in real-world environments.

In this talk, we present a formal approach for verifying the safety of AI-enabled CPS. We focus on closed-loop systems that integrate dynamical models of physical processes with neural network-based perception and control modules. We explore two verification scenarios: (1) controllers implemented as neural networks, and (2) perception pipelines combining camera models with neural networks. A key challenge in both settings is the scalability of verification algorithms, particularly due to the large size of neural networks and the complexity introduced by image-based perception.

To address these challenges, we propose abstraction techniques that simplify system representations and make verification tractable. Specifically, we introduce two novel data structures: Interval Neural Networks, which provide abstract representations of neural network behaviors, and Interval Images, which serve as abstract symbolic representations of a set of images. We also present novel abstraction-refinement algorithms that efficiently search for small abstractions to prove system safety. Our experimental results demonstrate that these abstraction-refinement algorithms significantly improve scalability and efficiency by quickly identifying small abstractions to prove safety, enabling the analysis of complex, large-scale AI-enabled CPS.

We also discuss verification approaches for evolving neural networks and highlight ongoing work on stability analysis, refinement checking, compositional analysis, and related challenges.

This work is a collaborative effort with students and postdoctoral researchers in the Trustworthy AI and Autonomous Systems (TRAITS) Lab, in collaboration with the Indian Institute of Science (IISc), and is supported by NSF and Amazon Research Awards.

Abstract: The Word Problem in finitely generated subgroups of \(\textsf{GL}_d(\mathbb{Z})\) is the following: given a word on a fixed finite alphabet of invertible matrices with integer coefficients, decide whether this word evaluates to the identity matrix. The Word Problem is trivially decidable, in polynomial time. Its worst-case complexity is known to be \(\mathcal{O}(n\log^2 n)\). We give an algorithm which solves it with linear average-case complexity. This is done under the bit-complexity model, which accounts for the fact that large integers are handled, and under the assumption that the input words are chosen uniformly at random among words of a given length.

This is joint work with Frédérique Bassino and Cyril Nicaud.