On Regularity of Unary Probabilistic Automata

Authors S. Akshay, Blaise Genest, Bruno Karelovic, Nikhil Vyas

Thumbnail PDF


  • Filesize: 0.66 MB
  • 14 pages

Document Identifiers

Author Details

S. Akshay
Blaise Genest
Bruno Karelovic
Nikhil Vyas

Cite AsGet BibTex

S. Akshay, Blaise Genest, Bruno Karelovic, and Nikhil Vyas. On Regularity of Unary Probabilistic Automata. In 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 47, pp. 8:1-8:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


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 n-th 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 non-regular 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.
  • Probabilistic automata
  • Symbolic dynamics
  • Markov chains
  • Skolem problem
  • Regularity


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. M. Agrawal, S. Akshay, B. Genest, and P. S. Thiagarajan. Approximate verification of the symbolic dynamics of Markov chains. In LICS, pages 55-64. IEEE Computer Society, 2012. Google Scholar
  2. M. Agrawal, S. Akshay, B. Genest, and P. S. Thiagarajan. Approximate verification of the symbolic dynamics of Markov chains. J.ACM, 62(1):183-235, 2015. Google Scholar
  3. S. Akshay, T. Antonopoulos, J. Ouaknine, and J. Worrell. Reachability problems for Markov chains. Information Processing Letters, 115(2):155-158, 2015. Google Scholar
  4. S. Akshay, B. Genest, B. Karelovic, and N. Vyas. On regularity of unary probabilistic automata. Technical report available online at http://perso.crans.org/~genest/AGKV16.pdf, 2015.
  5. Alberto Bertoni. The solution of problems relative to probabilistic automata in the frame of the formal languages theory. In GI Jahrestagung, pages 107-112, 1974. Google Scholar
  6. R. Chadha, Dileep Kini, and M. Viswanathan. Decidable Problems for Unary PFAs. In QEST, pages 329-344. LNCS 8657, 2014. Google Scholar
  7. K. Chatterjee and M. Tracol. Decidable Problems for Probabilistic Automata on Infinite Words. In LICS, pages 185-194. IEEE Computer Society, 2012. Google Scholar
  8. N. Fijalkow, H. Gimbert, and Y. Ouahladj. Deciding the Value 1 Problem for Probabilistic Leaktight Automata. In LICS, pages 295-304. IEEE Computer Society, 2012. Google Scholar
  9. H. Gimbert and Y. Ouahladj. Probabilistic Automata on Finite Words: Decidable and Undecidable Problems. In ICALP, pages 527-538. LNCS 6199, 2010. Google Scholar
  10. V. Halava, T. Harju, and M. Hirvensalo. Positivity of second order linear recurrent sequences. Discrete Applied Mathematics, 154(3), 2006. Google Scholar
  11. V. A. Korthikanti, M. Viswanathan, G. Agha, and Y. Kwon. Reasoning about MDPs as transformers of probability distributions. In QEST, p. 199-208. IEEE, 2010. Google Scholar
  12. C. Lech. A note on recurring series. Ark. Mat., 2, 1953. Google Scholar
  13. O. Madani, S. Hanks, and A. Condon. On the undecidability of probabilistic planning and related stochastic optimization problems. Artificial Intelligence, 147(1-2):5-34, 2003. Google Scholar
  14. K. Mahler. Eine arithmetische Eigenschaft der Taylor-koeffizienten rationaler Funktionen. Proc. Akad. Wet. Amsterdam, 38, 1935. Google Scholar
  15. L. Maruthi, I. Tkachev, A. Carta, E. Cinquemani, P. Hersen, G. Batt., and A. Abate. Towards real-time control of gene expression at the single cell level: a stochastic control approach. In CMSB, pages 155-172. LNCS/LNBI, 2014. Google Scholar
  16. J. Ouaknine and J. Worrell. Decision problems for linear recurrence sequences. In RP, pages 21-28, 2012. Google Scholar
  17. J. Ouaknine and J. Worrell. On the Positivity Problem for simple linear recurrence sequences. In ICALP, pages 318-329. LNCS 8573, 2014. Google Scholar
  18. J. Ouaknine and J. Worrell. Positivity problems for low-order linear recurrence sequences. In SODA, pages 366-379. ACM-SIAM, 2014. Google Scholar
  19. J. Ouaknine and J. Worrell. Ultimate Positivity is decidable for simple linear recurrence sequences. In ICALP, pages 330-341. LNCS 8573, 2014. Google Scholar
  20. Azaria Paz. Introduction to Probabilistic Automata. Academic Press, 1971. Google Scholar
  21. Michael O. Rabin. Probabilistic automata. Information and Control, 6(3):230-245, 1963. Google Scholar
  22. P. Turakainen. On Stochastic Languages. Information and Control, 12:304-313, 1968. Google Scholar