Specification Mining and Robust Design under Uncertainty
Abstract
In this paper, we propose Stochastic Temporal Logic (StTL) as a formalism for expressing probabilistic specifications on time-varying behaviors of controlled stochastic dynamical systems. To make StTL a more effective specification formalism, we introduce the quantitative semantics for StTL to reason about the robust satisfaction of an StTL specification by a given system. Additionally, we propose using the robustness value as the objective function to be maximized by a stochastic optimization algorithm for the purpose of controller design. Finally, we formulate an algorithm for parameter inference for Parameteric-StTL specifications, which allows specifications to be mined from output traces of the underlying system. We demonstrate and validate our framework on two case studies inspired by the automotive domain.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Oct 08, 2019
- Source ID
- 10.1145/3358231
Entities
People
- Jyotirmoy V. Deshmukh
- Panagiotis Kyriakis
- Paul Bogdan
Organizations
- Army Research Office
- Defense Advanced Research Projects Agency
- National Science Foundation
- University of Southern California