On Regularity of Unary Probabilistic Automata

8 years 6 months ago

Download perso.crans.org

The quantitative veriﬁcation of Probabilistic Automata (PA) is undecidable in general. Unary PA are a simpler model where the choice of action is ﬁxed. Still, the quantitative veriﬁcation 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 deﬁned below), whose regularity would entail the decidability of quantitative veriﬁcation. Given an initial distribution, we represent the trajectory of a unary PA over time as an inﬁnite word over a ﬁnite 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 inﬁnite) 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

Real-time Traffic