Data-driven probabilistic modeling and verification of human driver behavior

D. Sadigh, K. Driggs-Campbell, A. Puggelli, W. Li, V. Shia, R. Bajcsy, A. L. Sangiovanni-Vincentelli, S. S. Sastry, S. A. Seshia

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.

Original languageEnglish (US)
Title of host publicationFormal Verification and Modeling in Human-Machine Systems - Papers from the AAAI Spring Symposium, Technical Report
PublisherAI Access Foundation
Number of pages6
ISBN (Print)9781577356554
StatePublished - 2014
Externally publishedYes
Event2014 AAAI Spring Symposium - Palo Alto, CA, United States
Duration: Mar 24 2014Mar 26 2014

Publication series

NameAAAI Spring Symposium - Technical Report


Conference2014 AAAI Spring Symposium
Country/TerritoryUnited States
CityPalo Alto, CA

ASJC Scopus subject areas

  • Artificial Intelligence


Dive into the research topics of 'Data-driven probabilistic modeling and verification of human driver behavior'. Together they form a unique fingerprint.

Cite this