Characterization and computation of infinite horizon specifications over Markov processes

Abstract

This work is devoted to the formal verification of specifications over general discrete-time Markov processes, with an emphasis on infinite-horizon properties. These properties, formulated in a modal logic known as PCTL, can be expressed through value functions defined over the state space of the process. The main goal is to understand how structural features of the model (primarily the presence of absorbing sets) influence the uniqueness of the solutions of corresponding Bellman equations. Furthermore, this contribution shows that the investigation of these structural features leads to new computational techniques to calculate the specifications of interest: the emphasis is to derive approximation techniques with associated explicit convergence rates and formal error bounds.

Cited by in corpus (5)

• Robust Control for Dynamical Systems With Non-Gaussian Noise via Formal Abstractions
• Symbolic Controller Synthesis for Büchi Specifications on Stochastic Systems
• Quantitative Approximation of the Probability Distribution of a Markov Process by Formal Abstractions
• Sampling-based Approximations with Quantitative Performance for the Probabilistic Reach-Avoid Problem over General Markov Processes
• Computation of ruin probabilities for general discrete-time Markov models