Abstraction-based synthesis for stochastic systems with omega-regular objectives

DOI10.1016/j.nahs.2022.101204zbMath1497.93069arXiv2001.09236OpenAlexW3002811560MaRDI QIDQ2158881

Jeongmin Huh, Samuel Coogan, Maxence Dutreix

Publication date: 26 July 2022

Published in: Nonlinear Analysis. Hybrid Systems (Search for Journal in Brave)

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

zbMATH Keywords

formal methodsstochastic systemsbounded-parameter Markov decision processesfinite-state abstractionsinterval-valued Markov chains

Mathematics Subject Classification ID

Discrete-time control/observation systems (93C55) Synthesis problems (93B50) Markov and semi-Markov decision processes (90C40) Stochastic systems in control theory (general) (93E03)

Related Items (5)

Symbolic control for stochastic systems via finite parity games ⋮ Distributionally Robust Strategy Synthesis for Switched Stochastic Systems ⋮ Interval Markov Decision Processes with Continuous Action-Spaces ⋮ Poster Abstract: A Toolchain for Accelerated Symbolic Control ⋮ Automated verification and synthesis of stochastic hybrid systems: a survey

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Finite abstractions with robustness margins for temporal logic-based control synthesis
• Linear temporal logic symbolic model checking
• Bounded-parameter Markov decision processes
• Formal methods for discrete-time dynamical systems
• Reachability analysis of uncertain systems using bounded-parameter Markov decision processes
• Interval iteration algorithm for MDPs and IMDPs
• Formal Verification and Synthesis for Discrete-Time Stochastic Systems
• Specification-guided controller synthesis for linear systems and safe linear-time temporal logic
• Efficient finite abstraction of mixed monotone systems
• SCOTS
• Markov Set-Chains as Abstractions of Stochastic Hybrid Systems
• Formal Synthesis of Control Strategies for Positive Monotone Systems
• A Fully Automated Framework for Control of Linear Systems from Temporal Logic Specifications
• Specification-Guided Verification and Abstraction Refinement of Mixed Monotone Stochastic Systems
• Efficiency through uncertainty
• StocHy - automated verification and synthesis of stochastic processes
• Linear Time Logic Control of Discrete-Time Linear Systems
• Approximate Abstractions of Stochastic Hybrid Systems
• Temporal Logic Control of Discrete-Time Piecewise Affine Systems
• Hybrid Systems: Computation and Control
• Tools and Algorithms for the Construction and Analysis of Systems

This page was built for publication: Abstraction-based synthesis for stochastic systems with omega-regular objectives