Strategy synthesis for partially-known switched stochastic systems

DOI10.1145/3447928.3456649arXiv2104.02172MaRDI QIDQ6201583FDOQ6201583

Authors:

Publication date: 21 February 2024

Published in: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/2104.02172

zbMATH Keywords

Gaussian process regressionswitched stochastic systemsformal synthesissafe autonomyuncertain Markov decision processes

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30)

Cites Work

• Information-Theoretic Regret Bounds for Gaussian Process Optimization in the Bandit Setting
• On the influence of the kernel on the consistency of support vector machines
• Concentration inequalities and model selection. Ecole d'Eté de Probabilités de Saint-Flour XXXIII -- 2003.
• Title not available (Why is that?)
• Title not available (Why is that?)
• Stochastic Modeling and Control of Biological Systems: The Lactose Regulation System ofEscherichia Coli
• Formal Verification and Synthesis for Discrete-Time Stochastic Systems
• Bounded-parameter Markov decision processes
• An introduction to the theory of reproducing kernel Hilbert spaces
• Advanced Lectures on Machine Learning
• Reachability analysis of uncertain systems using bounded-parameter Markov decision processes
• Verification of Hybrid Systems
• A General Safety Framework for Learning-Based Control in Uncertain Robotic Systems
• Sherlock - A tool for verification of neural network feedback systems
• Formal and Efficient Synthesis for Continuous-Time Linear Stochastic Hybrid Processes
• Multi-objective Robust Strategy Synthesis for Interval Markov Decision Processes
• Efficiency through uncertainty
• On the effect of perturbation of conditional probabilities in total variation
• Data driven stability analysis of black-box switched linear systems
• Title not available (Why is that?)
• Data-driven and model-based verification via Bayesian identification and reachability analysis

This page was built for publication: Strategy synthesis for partially-known switched stochastic systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6201583)