When is Containment Decidable for Probabilistic Automata?

Authors Laure Daviaud, Marcin Jurdzinski, Ranko Lazic, Filip Mazowiecki, Guillermo A. Pérez , James Worrell

Thumbnail PDF


  • Filesize: 0.53 MB
  • 14 pages

Document Identifiers

Author Details

Laure Daviaud
  • University of Warwick, Coventry, UK
Marcin Jurdzinski
  • University of Warwick, Coventry, UK
Ranko Lazic
  • University of Warwick, Coventry, UK
Filip Mazowiecki
  • Université de Bordeaux, Bordeaux, France
Guillermo A. Pérez
  • Université libre de Bruxelles, Brussels, Belgium
James Worrell
  • University of Oxford, Oxford, UK

Cite AsGet BibTex

Laure Daviaud, Marcin Jurdzinski, Ranko Lazic, Filip Mazowiecki, Guillermo A. Pérez, and James Worrell. When is Containment Decidable for Probabilistic Automata?. In 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 107, pp. 121:1-121:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


The containment problem for quantitative automata is the natural quantitative generalisation of the classical language inclusion problem for Boolean automata. We study it for probabilistic automata, where it is known to be undecidable in general. We restrict our study to the class of probabilistic automata with bounded ambiguity. There, we show decidability (subject to Schanuel's conjecture) when one of the automata is assumed to be unambiguous while the other one is allowed to be finitely ambiguous. Furthermore, we show that this is close to the most general decidable fragment of this problem by proving that it is already undecidable if one of the automata is allowed to be linearly ambiguous.

Subject Classification

ACM Subject Classification
  • Theory of computation → Quantitative automata
  • Theory of computation → Probabilistic computation
  • Probabilistic automata
  • Containment
  • Emptiness
  • Ambiguity


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


  1. Shaull Almagor, Udi Boker, and Orna Kupferman. What’s decidable about weighted automata? In Tevfik Bultan and Pao-Ann Hsiung, editors, Automated Technology for Verification and Analysis, 9th International Symposium, ATVA 2011, Taipei, Taiwan, October 11-14, 2011. Proceedings, volume 6996 of Lecture Notes in Computer Science, pages 482-491. Springer, 2011. URL: http://dx.doi.org/10.1007/978-3-642-24372-1_37.
  2. Rohit Chadha, A. Prasad Sistla, Mahesh Viswanathan, and Yue Ben. Decidable and expressive classes of probabilistic automata. In Andrew M. Pitts, editor, Foundations of Software Science and Computation Structures - 18th International Conference, FoSSaCS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, volume 9034 of Lecture Notes in Computer Science, pages 200-214. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-662-46678-0_13.
  3. Henri Cohen. A course in computational algebraic number theory, volume 138 of Graduate texts in mathematics. Springer, 1993. URL: http://www.worldcat.org/oclc/27810276.
  4. Thomas Colcombet. On distance automata and regular cost function. Presented at the Dagstuhl seminar “Advances and Applications of Automata on Words and Trees”, 2010. Google Scholar
  5. Lu Feng, Tingting Han, Marta Z. Kwiatkowska, and David Parker. Learning-based compositional verification for synchronous probabilistic systems. In Tevfik Bultan and Pao-Ann Hsiung, editors, Automated Technology for Verification and Analysis, 9th International Symposium, ATVA 2011, Taipei, Taiwan, October 11-14, 2011, volume 6996 of Lecture Notes in Computer Science, pages 511-521. Springer, 2011. URL: http://dx.doi.org/10.1007/978-3-642-24372-1_40.
  6. Nathanaël Fijalkow. Undecidability results for probabilistic automata. SIGLOG News, 4(4):10-17, 2017. URL: http://dx.doi.org/10.1145/3157831.3157833.
  7. Nathanaël Fijalkow, Hugo Gimbert, Edon Kelmendi, and Youssouf Oualhadj. Deciding the value 1 problem for probabilistic leaktight automata. Logical Methods in Computer Science, 11(2), 2015. URL: http://dx.doi.org/10.2168/LMCS-11(2:12)2015.
  8. Nathanaël Fijalkow, Cristian Riveros, and James Worrell. Probabilistic automata of bounded ambiguity. In Roland Meyer and Uwe Nestmann, editors, 28th International Conference on Concurrency Theory, CONCUR 2017, September 5-8, 2017, Berlin, Germany, volume 85 of LIPIcs, pages 19:1-19:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. URL: http://dx.doi.org/10.4230/LIPIcs.CONCUR.2017.19.
  9. Holger Giese, Nelly Bencomo, Liliana Pasquale, Andres J. Ramirez, Paola Inverardi, Sebastian Wätzoldt, and Siobhán Clarke. Living with uncertainty in the age of runtime models. In Nelly Bencomo, Robert B. France, Betty H. C. Cheng, and Uwe Assmann, editors, Models@run.time - Foundations, Applications, and Roadmaps [Dagstuhl Seminar 11481, November 27 - December 2, 2011], volume 8378 of Lecture Notes in Computer Science, pages 47-100. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-319-08915-7_3.
  10. Hugo Gimbert and Youssouf Oualhadj. Probabilistic automata on finite words: Decidable and undecidable problems. In Samson Abramsky, Cyril Gavoille, Claude Kirchner, Friedhelm Meyer auf der Heide, and Paul G. Spirakis, editors, Automata, Languages and Programming, 37th International Colloquium, ICALP 2010, Bordeaux, France, July 6-10, 2010, Proceedings, Part II, volume 6199 of Lecture Notes in Computer Science, pages 527-538. Springer, 2010. URL: http://dx.doi.org/10.1007/978-3-642-14162-1_44.
  11. Leslie Pack Kaelbling, Michael L. Littman, and Andrew W. Moore. Reinforcement learning: A survey. Journal of Artificial Intelligence Research, 4:237-285, 1996. URL: http://dx.doi.org/10.1613/jair.301.
  12. Leonid Khachiyan and Lorant Porkolab. Computing integral points in convex semi-algebraic sets. In 38th Annual Symposium on Foundations of Computer Science, FOCS '97, Miami Beach, Florida, USA, October 19-22, 1997, pages 162-171. IEEE Computer Society, 1997. URL: http://dx.doi.org/10.1109/SFCS.1997.646105.
  13. Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, and James Worrell. On the complexity of equivalence and minimisation for q-weighted automata. Logical Methods in Computer Science, 9(1), 2013. URL: http://dx.doi.org/10.2168/LMCS-9(1:8)2013.
  14. Marta Z. Kwiatkowska, Gethin Norman, David Parker, and Hongyang Qu. Assume-guarantee verification for probabilistic systems. In Javier Esparza and Rupak Majumdar, editors, Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, volume 6015 of Lecture Notes in Computer Science, pages 23-37. Springer, 2010. URL: http://dx.doi.org/10.1007/978-3-642-12002-2_3.
  15. Angus Macintyre and Alex J. Wilkie. On the decidability of the real exponential field. In Piergiorgio Odifreddi, editor, Kreiseliana. About and Around Georg Kreisel, pages 441-467. AK Peters, 1996. Google Scholar
  16. Marvin Lee Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, 1967. Google Scholar
  17. Mehryar Mohri, Fernando Pereira, and Michael Riley. Weighted finite-state transducers in speech recognition. Computer Speech & Language, 16(1):69-88, 2002. URL: http://dx.doi.org/10.1006/csla.2001.0184.
  18. Krishna V. Palem and Lingamneni Avinash. Ten years of building broken chips: The physics and engineering of inexact computing. ACM Transactions on Embedded Computing Systems, 12(2s):87:1-87:23, 2013. URL: http://dx.doi.org/10.1145/2465787.2465789.
  19. Martin L. Puterman. Markov Decision Processes. Wiley-Interscience, 2005. Google Scholar
  20. Michael O. Rabin. Probabilistic automata. Information and Control, 6(3):230-245, 1963. URL: http://dx.doi.org/10.1016/S0019-9958(63)90290-0.
  21. Charles Rackoff. The covering and boundedness problems for vector addition systems. Theoretical Compututer Science, 6:223-231, 1978. URL: http://dx.doi.org/10.1016/0304-3975(78)90036-1.
  22. Stuart J. Russell and Peter Norvig. Artificial Intelligence - A Modern Approach (3. internat. ed.). Pearson Education, 2010. URL: http://vig.pearsoned.com/store/product/1,1207,store-12521_isbn-0136042597,00.html.
  23. Moshe Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In 26th Annual Symposium on Foundations of Computer Science, Portland, Oregon, USA, 21-23 October 1985, pages 327-338. IEEE Computer Society, 1985. URL: http://dx.doi.org/10.1109/SFCS.1985.12.
  24. Andreas Weber and Helmut Seidl. On the degree of ambiguity of finite automata. Theoretical Computer Science, 88(2):325-349, 1991. URL: http://dx.doi.org/10.1016/0304-3975(91)90381-B.
  25. Abuzer Yakaryilmaz and A. C. Cem Say. Unbounded-error quantum computation with small space bounds. Information and Computation, 209(6):873-892, 2011. URL: http://dx.doi.org/10.1016/j.ic.2011.01.008.