Document Open Access Logo

Probabilistic Model Checking via Families of Deterministic and Unambiguous Finite Automata

Authors Christel Baier , Sascha Klüppelholz , Timm Spork

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2026.15.pdf
  • Filesize: 1.09 MB
  • 19 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
  • Theory of computation → Verification by model checking
Keywords
  • Families of Finite Automata
  • FDFA
  • Unambiguous Automata
  • Discrete-time Markov Chains
  • Probabilistic Model Checking
  • Verification

Metrics

Abstract

Families of deterministic finite automata (FDFA) have been introduced as a concise automaton model that characterizes ω-regular languages by processing their ultimately periodic words. FDFA are known to enjoy many good properties and can be exponentially more succinct than deterministic ω-automata with Rabin, Streett or parity acceptance. This paper addresses two main questions: (1) Are FDFA suitable for probabilistic model checking purposes? and (2) Is it possible to obtain an even more compact representation of ω-regular languages by allowing the components of an FDFA to be unambiguous instead of deterministic? Question (1) is answered in the affirmative by presenting the first polynomial-time algorithm for computing the probability that a discrete-time Markov chain satisfies an ω-regular property represented as an FDFA. Question (2) is motivated by the fact that unambiguous finite automata may require exponentially fewer states than deterministic ones. This paper introduces a model of families of unambiguous finite automata (FUFA) that captures the class of ω-regular languages. FUFA can be exponentially more succinct than both FDFA and unambiguous Büchi automata, and there is a single-exponential translation from linear temporal logic (LTL) to FUFA. This stands in contrast to a double-exponential lower bound for the translation from LTL to FDFA. Moreover, the polynomial-time probabilistic model checking algorithm for discrete-time Markov chains against FDFA-specifications is extended to the case where the property is represented by an FUFA with a deterministic leading automaton.

Cite As Get BibTex

Christel Baier, Sascha Klüppelholz, and Timm Spork. Probabilistic Model Checking via Families of Deterministic and Unambiguous Finite Automata. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 15:1-15:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CONCUR.2026.15

Author Details

Christel Baier
  • Technische Universität Dresden, Germany
Sascha Klüppelholz
  • Technische Universität Dresden, Germany
Timm Spork
  • Technische Universität Dresden, Germany

Funding

This work was partly funded by the DFG grant 389792660 as part of TRR 248 (Foundations of Perspicuous Software Systems, see https://perspicuous-computing.science), the Cluster of Excellence EXC 2050/2 (CeTI, project ID 390696704, as part of Germany’s Excellence Strategy), and by the BMFTR (Federal Ministry of Research, Technology and Space) in DAAD project 57616814 (SECAI, School of Embedded and Composite AI) as part of the program Konrad Zuse Schools of Excellence in Artificial Intelligence.

Acknowledgements

We thank Dana Fisman for telling us about the double-exponential lower bound for the translation from LTL to FDFA, Jianlin Li for providing us with a copy of [Li, 2018], and Robin Ziemek for many interesting discussions on the topic.

References

  1. Dana Angluin, Udi Boker, and Dana Fisman. Families of DFAs as acceptors of ω-regular languages. Logical Methods in Computer Science, Volume 14, Issue 1, February 2018. URL: https://doi.org/10.23638/LMCS-14(1:15)2018.
  2. Dana Angluin and Dana Fisman. Learning regular omega languages. Theoretical Computer Science, 650:57-72, October 2016. URL: https://doi.org/10.1016/j.tcs.2016.07.031.
  3. Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. MIT Press, 2008. Google Scholar
  4. Christel Baier, Stefan Kiefer, Joachim Klein, David Müller, and James Worrell. Markov chains and unambiguous automata. Journal of Computer and System Sciences, 136:113-134, September 2023. URL: https://doi.org/10.1016/j.jcss.2023.03.005.
  5. Christel Baier, Sascha Klüppelholz, and Timm Spork. Probabilistic model checking via families of deterministic and unambiguous finite automata, 2026. URL: https://doi.org/10.48550/arXiv.2606.21976.
  6. Michael Benedikt, Rastislav Lenhardt, and James Worrell. Model checking Markov chains against unambiguous Büchi automata. CoRR, abs/1405.4560, 2014. URL: https://doi.org/10.48550/arXiv.1405.4560.
  7. León Bohn, Yong Li, Christof Löding, and Sven Schewe. Saturation problems for families of automata. In Keren Censor-Hillel, Fabrizio Grandoni, Joël Ouaknine, and Gabriele Puppis, editors, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025), volume 334 of Leibniz International Proceedings in Informatics (LIPIcs), pages 146:1-146:19, Dagstuhl, Germany, 2025. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ICALP.2025.146.
  8. J. Richard Büchi. Symposium on decision problems: On a decision method in restricted second order arithmetic. In Ernest Nagel, Patrick Suppes, and Alfred Tarski, editors, Logic, Methodology and Philosophy of Science, volume 44 of Studies in Logic and the Foundations of Mathematics, pages 1-11. Elsevier, 1966. URL: https://doi.org/10.1016/S0049-237X(09)70564-6.
  9. Hugues Calbrix, Maurice Nivat, and Andreas Podelski. Ultimately periodic words of rational ω-languages. In Stephen Brookes, Michael Main, Austin Melton, Michael Mislove, and David Schmidt, editors, Mathematical Foundations of Programming Semantics (MFPS 1993), volume 802 of Lecture Notes in Computer Science (LNCS), pages 554-566, Berlin, Heidelberg, 1994. Springer. URL: https://doi.org/10.1007/3-540-58027-1_27.
  10. Balder ten Cate, Dana Fisman, Roi Ohayon, and Patrik Sestic. Characterizing LTL Formulas by Examples, April 2026. URL: https://doi.org/10.48550/arXiv.2604.22097.
  11. Ashok K. Chandra, Dexter C. Kozen, and Larry J. Stockmeyer. Alternation. J. ACM, 28(1):114-133, January 1981. URL: https://doi.org/10.1145/322234.322243.
  12. Thomas Colcombet. Unambiguity in automata theory. In Jeffrey Shallit and Alexander Okhotin, editors, Descriptional Complexity of Formal Systems (DCFS 2015), volume 9118 of Lecture Notes in Computer Science (LNCS), pages 3-18. Springer International Publishing, Cham, 2015. URL: https://doi.org/10.1007/978-3-319-19225-3_1.
  13. Costas Courcoubetis and Mihalis Yannakakis. The complexity of probabilistic verification. J. ACM, 42(4):857-907, July 1995. URL: https://doi.org/10.1145/210332.210339.
  14. Javier Esparza, Jan Křetínský, Jean-François Raskin, and Salomon Sickert. From LTL and limit-deterministic Büchi automata to deterministic parity automata. In Axel Legay and Tiziana Margaria, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017), volume 10205 of Lecture Notes in Computer Science (LNCS), pages 426-442, Berlin, Heidelberg, 2017. Springer. URL: https://doi.org/10.1007/978-3-662-54577-5_25.
  15. Javier Esparza, Jan Křetínský, and Salomon Sickert. A unified translation of linear temporal logic to ω-automata. J. ACM, 67(6), October 2020. URL: https://doi.org/10.1145/3417995.
  16. Dana Fisman. Personal communication, 2024. Google Scholar
  17. Mika Göös, Stefan Kiefer, and Weiqiang Yuan. Lower bounds for unambiguous automata via communication complexity. In Mikołaj Bojańczyk, Emanuela Merelli, and David P. Woodruff, editors, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022), volume 229 of Leibniz International Proceedings in Informatics (LIPIcs), pages 126:1-126:13, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ICALP.2022.126.
  18. Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors. Automata, Logics, and Infinite Games, volume 2500 of Lecture Notes in Computer Science (LNCS). Springer, Berlin, Heidelberg, 2002. URL: https://doi.org/10.1007/3-540-36387-4.
  19. John G. Kemeny and J. Laurie Snell. Finite Markov Chains. Undergraduate Texts in Mathematics (UTM). Springer New York, 1976. Google Scholar
  20. Orna Kupferman and Moshe Y. Vardi. From linear time to branching time. ACM Trans. Comput. Logic, 6(2):273-294, April 2005. URL: https://doi.org/10.1145/1055686.1055689.
  21. Hing Leung. Separating exponentially ambiguous finite automata from polynomially ambiguous finite automata. SIAM Journal on Computing, 27(4):1073-1082, August 1998. URL: https://doi.org/10.1137/S0097539793252092.
  22. Hing Leung. Descriptional complexity of NFA of different ambiguity. International Journal of Foundations of Computer Science, 16:975-984, January 2004. URL: https://doi.org/10.1142/S0129054105003418.
  23. Jianlin Li. Translating LTL to FDFA and FDFA model checking. Bachelor’s thesis. Nanjing University of Aeronautics and Astronautics, 2018. Google Scholar
  24. Yong Li, Yu-Fang Chen, Lijun Zhang, and Depeng Liu. A novel learning algorithm for Büchi automata based on family of DFAs and classification trees. In Axel Legay and Tiziana Margaria, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017), volume 10205 of Lecture Notes in Computer Science (LNCS), pages 208-226, Berlin, Heidelberg, 2017. Springer. URL: https://doi.org/10.1007/978-3-662-54577-5_12.
  25. Yong Li, Sven Schewe, and Qiyi Tang. A novel family of finite automata for recognizing and learning ω-regular languages. In Étienne André and Jun Sun, editors, Automated Technology for Verification and Analysis, volume 14215 of Lecture Notes in Computer Science (LNCS), pages 53-73, Cham, 2023. Springer Nature Switzerland. URL: https://doi.org/10.1007/978-3-031-45329-8_3.
  26. Yong Li, Yih-Kuen Tsay, Andrea Turrini, Moshe Y. Vardi, and Lijun Zhang. Congruence relations for Büchi automata. In Marieke Huisman, Corina Păsăreanu, and Naijun Zhan, editors, Formal Methods (FM 2021), volume 13047 of Lecture Notes in Computer Science (LNCS), pages 465-482, Cham, 2021. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-90870-6_25.
  27. Christof Löding. Optimal bounds for transformations of ω-automata. In C. Pandu Rangan, V. Raman, and R. Ramanujam, editors, Foundations of Software Technology and Theoretical Computer Science (FSTTCS 1999), volume 1738 of Lecture Notes in Computer Science (LNCS), pages 97-109, Berlin, Heidelberg, 1999. Springer. URL: https://doi.org/10.1007/3-540-46691-6_8.
  28. Christof Löding and Anton Pirogov. On finitely ambiguous Büchi automata. In Mizuho Hoshi and Shinnosuke Seki, editors, Developments in Language Theory (DLT 2018), volume 11088 of Lecture Notes in Computer Science (LNCS), pages 503-515, Cham, 2018. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-98654-8_41.
  29. Max Michel. Complementation is more difficult with automata on infinite words. CNET, Paris, 15, 1988. Google Scholar
  30. N. Piterman. From nondeterministic Büchi and Streett automata to deterministic parity automata. In 21st Annual IEEE Symposium on Logic in Computer Science (LICS 2006), pages 255-264, 2006. URL: https://doi.org/10.1109/LICS.2006.28.
  31. A. Pnueli and R. Rosner. On the synthesis of a reactive module. In Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1989), pages 179-190, New York, NY, USA, 1989. Association for Computing Machinery. URL: https://doi.org/10.1145/75277.75293.
  32. Amir Pnueli. The temporal logic of programs. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), pages 46-57, USA, 1977. IEEE Computer Society. URL: https://doi.org/10.1109/SFCS.1977.32.
  33. Mikhail Raskin. A superpolynomial lower bound for the size of non-deterministic complement of an unambiguous automaton. In Ioannis Chatzigiannakis, Christos Kaklamanis, Dániel Marx, and Donald Sannella, editors, 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018), volume 107 of Leibniz International Proceedings in Informatics (LIPIcs), pages 138:1-138:11, Dagstuhl, Germany, 2018. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ICALP.2018.138.
  34. Erik Meineche Schmidt. Succinctness of Descriptions of Context-Free, Regular, and Finite Languages. PhD thesis, University of Aarhus, 1978. Google Scholar
  35. R. E. Stearns and H. B. Hunt III. On the equivalence and containment problems for unambiguous regular expressions, regular grammars and finite automata. SIAM Journal on Computing, 14(3):598-611, 1985. URL: https://doi.org/10.1137/0214044.
  36. Wolfgang Thomas. Facets of synthesis: Revisiting Church’s problem. In Luca de Alfaro, editor, Foundations of Software Science and Computational Structures (FoSSaCS 2009), volume 5504 of Lecture Notes in Computer Science (LNCS), pages 1-14, Berlin, Heidelberg, 2009. Springer. URL: https://doi.org/10.1007/978-3-642-00596-1_1.
  37. Moshe Y. Vardi. Automatic verification of probabilistic concurrent finite state programs. In 26th Annual Symposium on Foundations of Computer Science (FOCS 1985), pages 327-338, 1985. URL: https://doi.org/10.1109/SFCS.1985.12.
  38. Moshe Y. Vardi and Pierre Wolper. An automata-theoretic approach to automatic program verification (preliminary report). In Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986), pages 332-344. IEEE Computer Society Press, June 1986. Google Scholar
  39. Thomas Wilke. ω-Automata. CoRR, abs/1609.03062, 2016. URL: https://doi.org/10.48550/arXiv.1609.03062.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact