Data-Driven Probabilistic Modeling and Verification of Human Driver Behavior

Dorsa Sadigh, Katherine Driggs-Campbell, Alberto Puggelli, Wenchao Li, Victor Shia, Ruzena Bajcsy, Alberto L. Sangiovanni-Vincentelli, S. Shankar Sastry, and Sanjit A. Seshia. Data-Driven Probabilistic Modeling and Verification of Human Driver Behavior. In Formal Verification and Modeling in Human-Machine Systems, AAAI Spring Symposium, March 2014.

Download

[pdf] 

Abstract

We address the problem of formally verifying quantitative properties of driver models.We first propose a novel stochastic model of the driver behavior based on Convex Markov Chains, i.e., Markov chains in which the transition probabilities are only known to lie in convex uncertainty sets. This formalism captures the intrinsic uncertainty in estimating transition probabilities starting from experimentally-collected data. We then formally verify properties of the model expressed in probabilistic computation tree logic (PCTL). Results show that our approach can correctly predict quantitative information about driver behavior depending on her state, e.g., whether he or she is attentive or distracted.

BibTeX

@inproceedings{sadigh-aaaifv14,
  author    = {Dorsa Sadigh and Katherine Driggs-Campbell and Alberto Puggelli and Wenchao Li and Victor Shia and Ruzena Bajcsy and Alberto L. Sangiovanni-Vincentelli and S. Shankar Sastry and Sanjit A. Seshia},
  title     = {Data-Driven Probabilistic Modeling and Verification of Human Driver Behavior},
 booktitle = {Formal Verification and Modeling in Human-Machine Systems, AAAI Spring Symposium},
 month = "March",
 year = {2014},
 abstract={We address the problem of formally verifying quantitative 
properties of driver models.We first propose a novel stochastic 
model of the driver behavior based on Convex Markov 
Chains, i.e., Markov chains in which the transition probabilities 
are only known to lie in convex uncertainty sets. This formalism 
captures the intrinsic uncertainty in estimating transition 
probabilities starting from experimentally-collected data. 
We then formally verify properties of the model expressed 
in probabilistic computation tree logic (PCTL). Results show 
that our approach can correctly predict quantitative information 
about driver behavior depending on her state, e.g., 
whether he or she is attentive or distracted.},
}