k-Inductive Barrier Certificates for Stochastic Systems

DOI10.1145/3501710.3519532OpenAlexW4225388096MaRDI QIDQ6120705

Unnamed Author, Unnamed Author, Majid Zamani, Ashutosh Trivedi

Publication date: 21 February 2024

Published in: 25th ACM International Conference on Hybrid Systems: Computation and Control (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/3501710.3519532

zbMATH Keywords

stochastic dynamical systemsbarrier certificatesk-inductionsafety specificationreachability specification

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

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A game-based abstraction-refinement framework for Markov decision processes
• Automatic analysis of DMA races using model checking and \(k\)-induction
• Semidefinite programming relaxations for semialgebraic problems
• Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems
• Stochastic stability and control
• Barrier certificates for nonlinear model validation
• Formal Verification and Synthesis for Discrete-Time Stochastic Systems
• Convex Programs for Temporal Verification of Nonlinear Dynamical Systems
• Using SeDuMi 1.02, A Matlab toolbox for optimization over symmetric cones
• Inner-Approximating Reachable Sets for Polynomial Systems With Time-Varying Uncertainties
• A Framework for Worst-Case and Stochastic Safety Verification Using Barrier Certificates
• Temporal logic verification of stochastic systems using barrier certificates

This page was built for publication: k-Inductive Barrier Certificates for Stochastic Systems