Abstract
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, then the language is effectively regular. Further, we show that this result is at the boundary of regularity, as nonregular languages can be generated when the restrictions are even slightly relaxed. The regular representation of the language allows us to reason about more general properties, e.g., robustness of a regular property in a neighbourhood around a given distribution.
BibTeX  Entry
@InProceedings{akshay_et_al:LIPIcs:2016:5709,
author = {S. Akshay and Blaise Genest and Bruno Karelovic and Nikhil Vyas},
title = {{On Regularity of Unary Probabilistic Automata}},
booktitle = {33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)},
pages = {8:18:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959770019},
ISSN = {18688969},
year = {2016},
volume = {47},
editor = {Nicolas Ollinger and Heribert Vollmer},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2016/5709},
URN = {urn:nbn:de:0030drops57093},
doi = {10.4230/LIPIcs.STACS.2016.8},
annote = {Keywords: Probabilistic automata, Symbolic dynamics, Markov chains, Skolem problem, Regularity}
}
Keywords: 

Probabilistic automata, Symbolic dynamics, Markov chains, Skolem problem, Regularity 
Seminar: 

33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016) 
Issue Date: 

2016 
Date of publication: 

16.02.2016 