Formal Verification and Synthesis for Discrete-Time Stochastic Systems

DOI10.1109/TAC.2015.2398883MaRDI QIDQ2982621zbMATH OpenFDO

Authors Morteza Lahijanian, Sean B. Andersson, Calin Belta

Publication date 16 May 2017

Published in IEEE Transactions on Automatic Control (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1109/TAC.2015.2398883

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Stochastic systems in control theory (general) (93E03)

Cited in

(28)

• On the use of MTBDDs for performability analysis and verification of stochastic systems.
• Verification and control for probabilistic hybrid automata with finite bisimulations
• Probabilistic guarantees for safe deep reinforcement learning
• Formal methods for discrete-time dynamical systems
• Automated verification and synthesis of stochastic hybrid systems: a survey
• Robustly complete finite-state abstractions for verification of stochastic systems
• Abstraction-based synthesis for stochastic systems with omega-regular objectives
• Collaborative models for autonomous systems controller synthesis
• Automatic verification of competitive stochastic systems
• Finite verification of the characteristic specification of discrete systems
• Data-driven verification of stochastic linear systems with signal temporal logic constraints
• Quantitative verification and strategy synthesis for stochastic games
• Control synthesis for stochastic systems given automata specifications defined by stochastic sets
• Formal and Efficient Synthesis for Continuous-Time Linear Stochastic Hybrid Processes
• Robust Control for Dynamical Systems with Non-Gaussian Noise via Formal Abstractions
• Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games
• k-Inductive Barrier Certificates for Stochastic Systems
• Symbolic control for stochastic systems via finite parity games
• Strategy synthesis for partially-known switched stochastic systems
• Distributionally Robust Strategy Synthesis for Switched Stochastic Systems
• Interval Markov Decision Processes with Continuous Action-Spaces
• Data-driven verification and synthesis of stochastic systems via barrier certificates
• Formal controller synthesis for Markov jump linear systems with uncertain dynamics
• Interval Markov decision processes with multiple objectives: from robust strategies to Pareto curves
• Secondary safety control for systems with sector bounded nonlinearities
• Scalable control synthesis for stochastic systems via structural imdp abstractions
• Memory-dependent abstractions of stochastic systems through the Lens of transfer operators
• Efficient strategy synthesis for switched stochastic systems with distributional uncertainty

This page was built for publication: Formal Verification and Synthesis for Discrete-Time Stochastic Systems

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