Characterization and computation of infinite horizon specifications over Markov processes

TL;DR

This paper investigates how structural features of Markov processes affect the solutions of Bellman equations for infinite-horizon properties, introducing new computational methods with convergence guarantees.

Contribution

It analyzes the impact of absorbing sets on solution uniqueness and develops approximation techniques with explicit convergence rates and error bounds.

Findings

Structural features influence solution uniqueness of Bellman equations.

New approximation algorithms with proven convergence rates.

Explicit error bounds for infinite-horizon property computations.

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.