An algorithmic approximation of the infimum reachability probability for Probabilistic Finite Automata

TL;DR

This paper presents an algorithm to approximate the lowest probability of a Probabilistic Finite Automata reaching a specific set of states, addressing a problem that is undecidable for the supremum case.

Contribution

It introduces a novel approximation algorithm for the infimum reachability probability in PFAs, contrasting with the undecidability of the supremum case.

Findings

The algorithm effectively approximates the infimum probability within a specified error threshold.

The work highlights the decidability of infimum approximation, unlike the supremum case.

It connects probabilistic automata analysis with model checking techniques.

Abstract

Given a Probabilistic Finite Automata (PFA), a set of states S, and an error threshold e > 0, our algorithm approximates the infimum probability (quantifying over all infinite words) that the automata reaches S. Our result contrasts with the known result that the approximation problem is undecidable if we consider the supremum instead of the infimum. Since we study the probability of reaching a set of states, instead of the probability of ending in an accepting state, our work is more related to model checking than to formal languages.