Model-checking branching-time properties of probabilistic automata and probabilistic one-counter automata

TL;DR

This paper proves that model-checking probabilistic automata and probabilistic one-counter automata against branching-time temporal logics (PCTL and PCTL*) is undecidable, highlighting fundamental limitations in automated verification.

Contribution

It establishes the undecidability of model-checking for these probabilistic models against branching-time logics, extending previous results to more complex automata.

Findings

Model-checking probabilistic finite automata is undecidable.

Undecidability extends to probabilistic one-counter automata.

Reductions from the emptiness problem are used to prove undecidability.

Abstract

This paper studies the problem of model-checking of probabilistic automaton and probabilistic one-counter automata against probabilistic branching-time temporal logics (PCTL and PCTL$^*$). We show that it is undecidable for these problems. We first show, by reducing to emptiness problem of probabilistic automata, that the model-checking of probabilistic finite automata against branching-time temporal logics are undecidable. And then, for each probabilistic automata, by constructing a probabilistic one-counter automaton with the same behavior as questioned probabilistic automata the undecidability of model-checking problems against branching-time temporal logics are derived, herein.