Strategy synthesis for partially-known switched stochastic systems

Conference paper (2021)

Authors

John Jackson University of Colorado
L. Laurenti Team Luca Laurenti - Mechanical, Maritime and Materials Engineering
Eric Frew University of Colorado
Morteza Lahijanian University of Colorado
Research Group
Team Luca Laurenti (Mechanical, Maritime and Materials Engineering) (TU Delft)
Copyright: © 2021 John Jackson, L. Laurenti, Eric Frew, Morteza Lahijanian
DOI: https://doi.org/10.1145/3447928.3456649
Formal synthesis Gaussian process regression Safe autonomy Switched stochastic systems Uncertain markov decision processes
More Info
expand_more

Published Date

2021

Language

English

Reuse Rights

Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.

Faculty

Mechanical, Maritime and Materials Engineering

Department

Delft Center for Systems and Control

Research Group

Team Luca Laurenti

Abstract

We present a data-driven framework for strategy synthesis for partially-known switched stochastic systems. The properties of the system are specified using linear temporal logic (LTL) over finite traces (LTLf), which is as expressive as LTL and enables interpretations over finite behaviors. The framework first learns the unknown dynamics via Gaussian process regression. Then, it builds a formal abstraction of the switched system in terms of an uncertain Markov model, namely an Interval Markov Decision Process (IMDP), by accounting for both the stochastic behavior of the system and the uncertainty in the learning step. Then, we synthesize a strategy on the resulting IMDP that maximizes the satisfaction probability of the LTLf specification and is robust against all the uncertainties in the abstraction. This strategy is then refined into a switching strategy for the original stochastic system. We show that this strategy is near-optimal and provide a bound on its distance (error) to the optimal strategy. We experimentally validate our framework on various case studies, including both linear and non-linear switched stochastic systems.