Strategy synthesis for partially-known switched stochastic systems

DOI10.1145/3447928.3456649MaRDI 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)

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)

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.

Cites work

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

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)