Sciweavers

STACS
2016
Springer

On Regularity of Unary Probabilistic Automata

7 years 11 months ago
On Regularity of Unary Probabilistic Automata
The quantitative verification of Probabilistic Automata (PA) is undecidable in general. Unary PA are a simpler model where the choice of action is fixed. Still, the quantitative verification problem is open and known to be as hard as Skolem’s problem, a problem on linear recurrence sequences, whose decidability is open for at least 40 years. In this paper, we approach this problem by studying the languages generated by unary PAs (as defined below), whose regularity would entail the decidability of quantitative verification. Given an initial distribution, we represent the trajectory of a unary PA over time as an infinite word over a finite alphabet, where the nth letter represents a probability range after n steps. We extend this to a language of trajectories (a set of words), one trajectory for each initial distribution from a (possibly infinite) set. We show that if the eigenvalues of the transition matrix associated with the unary PA are all distinct positive real numbers,...
S. Akshay, Blaise Genest, Bruno Karelovic, Nikhil
Added 10 Apr 2016
Updated 10 Apr 2016
Type Journal
Year 2016
Where STACS
Authors S. Akshay, Blaise Genest, Bruno Karelovic, Nikhil Vyas
Comments (0)