Quantitative Approximation of the Probability Distribution of a Markov Process by Formal Abstractions

DOI10.2168/LMCS-11(3:8)2015zbMATH Open1342.60120arXiv1504.00039OpenAlexW1956206657MaRDI QIDQ3196339FDOQ3196339

Alessandro Abate, Sadegh Esmaeil Zadeh Soudjani

Publication date: 29 October 2015

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Abstract: The goal of this work is to formally abstract a Markov process evolving in discrete time over a general state space as a finite-state Markov chain, with the objective of precisely approximating its state probability distribution in time, which allows for its approximate, faster computation by that of the Markov chain. The approach is based on formal abstractions and employs an arbitrary finite partition of the state space of the Markov process, and the computation of average transition probabilities between partition sets. The abstraction technique is formal, in that it comes with guarantees on the introduced approximation that depend on the diameters of the partitions: as such, they can be tuned at will. Further in the case of Markov processes with unbounded state spaces, a procedure for precisely truncating the state space within a compact set is provided, together with an error bound that depends on the asymptotic properties of the transition kernel of the original process. The overall abstraction algorithm, which practically hinges on piecewise constant approximations of the density functions of the Markov process, is extended to higher-order function approximations: these can lead to improved error bounds and associated lower computational requirements. The approach is practically tested to compute probabilistic invariance of the Markov process under study, and is compared to a known alternative approach from the literature.

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

zbMATH Keywords

Markov processesprobability distributionsdiscrete-time stochastic systemsformal abstractions

Mathematics Subject Classification ID

Computational methods in Markov chains (60J22) Numerical analysis or methods applied to Markov chains (65C40) Central limit and other weak theorems (60F05) Markov chains (discrete-time Markov processes on discrete state spaces) (60J10) Discrete-time Markov processes on general state spaces (60J05)

Cited In (8)

• Formal abstraction and synthesis of parametric stochastic processes
• Verification of General Markov Decision Processes by Approximate Similarity Relations and Policy Refinement
• A unified framework for coordination of thermostatically controlled loads
• Automated verification and synthesis of stochastic hybrid systems: a survey
• Compositional abstraction of large-scale stochastic systems: a relaxed dissipativity approach
• Model-Based Formal Reliability Analysis of Grid Dynamics with Solar Energy Sources
• Verification of quantum systems using barrier certificates
• Dynamic Bayesian networks for formal verification of structured stochastic processes

Uses Software

• PRISM
• MRMC
• MPT

Recommendations

• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• \(q\)-distributions and Markov processes 👍 👎
• Approximation of Markov chains 👍 👎
• Quantitative approximations of evolving probability measures and sequential Markov chain Monte Carlo methods 👍 👎
• Approximations of non-homogeneous Markov chains on abstract states spaces 👍 👎
• An approximation theorem for Markov processes 👍 👎
• A probability approximation framework: Markov process approach 👍 👎
• Distribution, approximation and probabilistic model checking 👍 👎

This page was built for publication: Quantitative Approximation of the Probability Distribution of a Markov Process by Formal Abstractions

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