Compositional Simulation-Based Analysis of AI-Based Autonomous Systems for Markovian Specifications

Beyazit Yalcinkaya, Hazem Torfah, Daniel J. Fremont, and Sanjit A. Seshia. Compositional Simulation-Based Analysis of AI-Based Autonomous Systems for Markovian Specifications. In 23rd International Conference on Runtime Verification (RV), pp. 191–212, Lecture Notes in Computer Science 14245, Springer, 2023.

Download

[pdf] 

Abstract

We present a framework for the compositional simulation-based analysis of AI-based autonomous systems for Markovian safety specifications. Our compositional approach allows us to cut down the cost of executing a large number of long-running simulations, by decomposing a simulation-based analysis task into several shorter and more efficient ones. Results obtained from the individual analyses are then stitched together to generate a result for the overall simulation-based task. Our approach is based on a decomposition of scenarios formalized as concurrent hierarchical probabilistic extended state machines that describe sequential and parallel compositions of scenarios. We present two instantiations of our framework for falsification and statistical verification. Using case studies from the autonomous driving domain, we demonstrate the scalability of our compositional approach in comparison to a monolithic analysis approach.

BibTeX

@inproceedings{yalcinkaya-rv23,
  author       = {Beyazit Yalcinkaya and
                  Hazem Torfah and
                  Daniel J. Fremont and
                  Sanjit A. Seshia},
  editor       = {Panagiotis Katsaros and
                  Laura Nenzi},
  title        = {Compositional Simulation-Based Analysis of {AI}-Based Autonomous Systems
                  for {Markovian} Specifications},
  booktitle    = {23rd International Conference on Runtime Verification (RV)},
  series       = {Lecture Notes in Computer Science},
  volume       = {14245},
  pages        = {191--212},
  publisher    = {Springer},
  year         = {2023},
  abstract  = {We present a framework for the compositional simulation-based analysis of AI-based autonomous systems for Markovian safety specifications. Our compositional approach allows us to cut down the cost of executing a large number of long-running simulations, by decomposing a simulation-based analysis task into several shorter and more efficient ones. Results obtained from the individual analyses are then stitched together to generate a result for the overall simulation-based task. Our approach is based on a decomposition of scenarios formalized as concurrent hierarchical probabilistic extended state machines that describe sequential and parallel compositions of scenarios. We present two instantiations of our framework for falsification and statistical verification. Using case studies from the autonomous driving domain, we demonstrate the scalability of our compositional approach in comparison to a monolithic analysis approach.},
}