Adaptive and Sequential Gridding Procedures for the Abstraction and Verification of Stochastic Processes

DOI10.1137/120871456zbMath1278.93243OpenAlexW2171282796MaRDI QIDQ2871352

Sadegh Esmaeil Zadeh Soudjani, Alessandro Abate

Publication date: 22 January 2014

Published in: SIAM Journal on Applied Dynamical Systems (Search for Journal in Brave)

Full work available at URL: http://resolver.tudelft.nl/uuid:bfc36534-6546-4173-be20-c08d0aff2ee7

zbMATH Keywords

Markov chains approximations formal verification stochastic hybrid systems abstractions general state-space processes properties and specifications safety and invariance

Mathematics Subject Classification ID

Applications of Markov chains and discrete-time Markov processes on general state spaces (social mobility, learning theory, industrial processes, etc.) (60J20) Stochastic systems in control theory (general) (93E03)

Related Items (23)

Robust Control for Dynamical Systems with Non-Gaussian Noise via Formal Abstractions ⋮ Formal abstraction and synthesis of parametric stochastic processes ⋮ A stochastic games framework for verification and control of discrete time stochastic hybrid systems ⋮ Compositional abstraction-based synthesis for networks of stochastic switched systems ⋮ Probabilistic reachability and control synthesis for stochastic switched systems using the tamed Euler method ⋮ Compositional abstraction of large-scale stochastic systems: a relaxed dissipativity approach ⋮ Characterization and computation of infinite-horizon specifications over Markov processes ⋮ Verification of General Markov Decision Processes by Approximate Similarity Relations and Policy Refinement ⋮ Compositional abstraction refinement for control synthesis ⋮ Compositional synthesis of control barrier certificates for networks of stochastic systems against \(\omega\)-regular specifications ⋮ Symbolic control for stochastic systems via finite parity games ⋮ Model checking HPnGs in multiple dimensions: representing state sets as convex polytopes ⋮ Compositional abstraction-based synthesis for continuous-time stochastic hybrid systems ⋮ Reachability for partially observable discrete time stochastic hybrid systems ⋮ On the Relationship Between Bisimulation and Trace Equivalence in an Approximate Probabilistic Context ⋮ Control synthesis for stochastic systems given automata specifications defined by stochastic sets ⋮ Dynamic Bayesian networks for formal verification of structured stochastic processes ⋮ Probabilistic Model Checking of Labelled Markov Processes via Finite Approximate Bisimulations ⋮ The Robot Routing Problem for Collecting Aggregate Stochastic Rewards ⋮ Compositional construction of infinite abstractions for networks of stochastic control systems ⋮ Finite horizon discrete models for multi-agent control systems with coupled dynamics ⋮ Compositional abstraction-based synthesis of general MDPs via approximate probabilistic relations ⋮ Automated verification and synthesis of stochastic hybrid systems: a survey

Uses Software

PRISM

This page was built for publication: Adaptive and Sequential Gridding Procedures for the Abstraction and Verification of Stochastic Processes