Characterization and computation of infinite horizon specifications over Markov processes
For researchers in formal verification and stochastic systems, this provides a theoretical foundation and computational methods for verifying infinite-horizon properties with guaranteed error bounds.
This work addresses the formal verification of infinite-horizon PCTL specifications over discrete-time Markov processes, focusing on how absorbing sets affect the uniqueness of Bellman equation solutions. It introduces approximation techniques with explicit convergence rates and formal error bounds.
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.