We describe an approach to Statistical Model Checking (SMC) that produces not only an estimate of the probability that specified properties (a.k.a. predicates) are satisfied, but also an “input attribution” for those predicates. We use logistic regression to generate the input attribution as a set of linear and non-linear functions of the inputs that explain conditions under which a predicate is satisfied. These functions provide quantitative insight into factors that influence the predicate outcome. We have implemented our approach on a distributed SMC infrastructure, demeter, that uses Linux Docker containers to isolate simulations (a.k.a. trials) from each other. Currently, demeter is deployed on six 20-core blade servers, and can perform tens of thousands of trials in a few hours.We demonstrate our approach on examples involving robotic agents interacting in a simulated physical environment. Our approach synthesizes input attributions that are both meaningful to the investigator and have predictive value on the predicate outcomes.
CITATION STYLE
Hansen, J. P., Chaki, S., Hissam, S., Edmondson, J., Moreno, G. A., & Kyle, D. (2016). Input attribution for statistical model checking using logistic regression. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10012 LNCS, pp. 185–200). Springer Verlag. https://doi.org/10.1007/978-3-319-46982-9_12
Mendeley helps you to discover research relevant for your work.