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 his/her state, e.g., whether he or she is attentive or distracted.
Title
Data-Driven Probabilistic Modeling and Verification of Human Driver Behavior
Published
2013-12-05
Full Collection Name
Electrical Engineering & Computer Sciences Technical Reports
Other Identifiers
EECS-2013-197
Type
Text
Extent
8 p
Archive
The Engineering Library
Usage Statement
Researchers may make free and open use of the UC Berkeley Library’s digitized public domain materials. However, some materials in our online collections may be protected by U.S. copyright law (Title 17, U.S.C.). Use or reproduction of materials protected by copyright beyond that allowed by fair use (Title 17, U.S.C. § 107) requires permission from the copyright owners. The use or reproduction of some materials may also be restricted by terms of University of California gift or purchase agreements, privacy and publicity rights, or trademark law. Responsibility for determining rights status and permissibility of any use or reproduction rests exclusively with the researcher. To learn more or make inquiries, please see our permissions policies (https://www.lib.berkeley.edu/about/permissions-policies).
