Robustly complete finite-state abstractions for verification of stochastic systems
From MaRDI portal
Publication:2112105
DOI10.1007/978-3-031-15839-1_5OpenAlexW4229045235MaRDI QIDQ2112105
Publication date: 18 January 2023
Full work available at URL: https://arxiv.org/abs/2205.01854
robustnesscompletenesslinear temporal logicsoundness\( \mathcal{L}_1\)-perturbationfinite-state abstractionmetrizable space of probability measuresverification of stochastic systems
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Characterization and computation of infinite-horizon specifications over Markov processes
- Quantitative model-checking of controlled discrete-time Markov processes
- Verification of discrete time stochastic hybrid systems: a stochastic reach-avoid decision problem
- Closing the gap between discrete abstractions and continuous control: completeness via robustness and controllability
- Embedded population systems in Markov set-chains
- Approximately bisimilar symbolic models for nonlinear control systems
- Bounded-parameter Markov decision processes
- Formal methods for discrete-time dynamical systems
- Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems
- Reachability analysis of uncertain systems using bounded-parameter Markov decision processes
- Formal Verification and Synthesis for Discrete-Time Stochastic Systems
- On the connections between PCTL and dynamic programming
- Quantitative automata model checking of autonomous stochastic hybrid systems
- Regularization of bellman equations for infinite-horizon probabilistic properties
- Formula-free finite abstractions for linear temporal verification of stochastic hybrid systems
- Markov Set-Chains as Abstractions of Stochastic Hybrid Systems
- On Choosing and Bounding Probability Metrics
- A Fully Automated Framework for Control of Linear Systems from Temporal Logic Specifications
- Approximately Bisimilar Symbolic Models for Incrementally Stable Switched Systems
- Robustly Complete Synthesis of Memoryless Controllers for Nonlinear Systems With Reach-and-Stay Specifications
- Specification-Guided Verification and Abstraction Refinement of Mixed Monotone Stochastic Systems
- Symbolic controller synthesis for Büchi specifications on stochastic systems
- Stochastic Equations in Infinite Dimensions
- Efficiency through uncertainty
- Robust Abstractions for Control Synthesis
- Linear Time Logic Control of Discrete-Time Linear Systems
- Computer Aided Verification
This page was built for publication: Robustly complete finite-state abstractions for verification of stochastic systems
