pith. sign in

arxiv: 2606.21976 · v1 · pith:2DHSF4DRnew · submitted 2026-06-20 · 💻 cs.FL

Probabilistic Model Checking via Families of Deterministic and Unambiguous Finite Automata

Christel Baier , Sascha Kl\"uppelholz , Timm Spork This is my paper

Pith reviewed 2026-06-26 11:05 UTC · model grok-4.3

classification 💻 cs.FL
keywords probabilistic model checkingomega-regular propertiesfamilies of deterministic finite automatafamilies of unambiguous finite automatadiscrete-time Markov chainslinear temporal logicautomata-based verification
0
0 comments X

The pith

A polynomial-time algorithm computes the probability that a discrete-time Markov chain satisfies an ω-regular property represented as a family of deterministic finite automata.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes that families of deterministic finite automata can represent ω-regular properties in a form that permits efficient probabilistic verification on discrete-time Markov chains. It supplies the first polynomial-time procedure for calculating the exact satisfaction probability under this representation. The work further defines families of unambiguous finite automata as a strictly more compact model for the same class of languages, shows a single-exponential translation from linear temporal logic into this model, and extends the polynomial-time procedure to the new model whenever its leading automaton component remains deterministic.

Core claim

Families of deterministic finite automata characterize ω-regular languages by processing their ultimately periodic words and admit a polynomial-time algorithm that computes the probability a discrete-time Markov chain satisfies a property expressed in this form. Families of unambiguous finite automata capture the same class of languages, can be exponentially more succinct than both the deterministic variant and unambiguous Büchi automata, support a single-exponential translation from linear temporal logic, and inherit the same polynomial-time checking procedure when the leading automaton is deterministic.

What carries the argument

Families of deterministic finite automata (FDFA) and families of unambiguous finite automata (FUFA), which represent ω-regular languages by a collection of automata that together process ultimately periodic words.

If this is right

  • The satisfaction probability for any ω-regular property given as an FDFA can be obtained in polynomial time.
  • FUFA representations of ω-regular languages can be exponentially smaller than FDFA representations.
  • Linear temporal logic formulas translate into FUFA in single-exponential time.
  • The polynomial-time checking procedure carries over to FUFA specifications whose leading automaton is deterministic.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Verification procedures for probabilistic systems could therefore handle properties previously limited by the size of deterministic ω-automata.
  • The distinction between deterministic and unambiguous components may allow selective use of nondeterminism only where it yields measurable size reductions.
  • Similar polynomial-time procedures might be derivable for other Markovian models if the leading-automaton restriction can be relaxed.

Load-bearing premise

The leading automaton component of an FUFA remains deterministic.

What would settle it

A concrete discrete-time Markov chain together with an FDFA specification whose satisfaction probability cannot be computed in polynomial time.

read the original abstract

Families of deterministic finite automata (FDFA) have been introduced as a concise automaton model that characterizes $\omega$-regular languages by processing their ultimately periodic words. FDFA are known to enjoy many good properties and can be exponentially more succinct than deterministic $\omega$-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 $\omega$-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 $\omega$-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 $\omega$-regular languages. FUFA can be exponentially more succinct than both FDFA and unambiguous B\"uchi 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 0 minor

Summary. The paper claims that families of deterministic finite automata (FDFA) are suitable for probabilistic model checking by providing the first polynomial-time algorithm to compute the probability that a discrete-time Markov chain satisfies an ω-regular property represented as an FDFA. It further introduces families of unambiguous finite automata (FUFA) as an even more succinct model for ω-regular languages, establishes a single-exponential translation from LTL to FUFA (contrasting with a double-exponential lower bound for FDFA), and extends the polynomial-time PMC algorithm to FUFA specifications whose leading automaton is deterministic.

Significance. If the polynomial-time PMC procedure and the succinctness claims hold, the work would meaningfully advance automata-based verification of ω-regular properties on DTMCs by leveraging more compact representations than standard deterministic ω-automata. The single-exponential LTL-to-FUFA translation and the extension to FUFA with deterministic leading components would be notable strengths, as they address known succinctness gaps while preserving algorithmic tractability.

major comments (1)
  1. [Abstract] Abstract: the central claim of a 'first polynomial-time algorithm' for PMC against FDFA (and its extension to FUFA) is asserted without any derivation steps, construction details, complexity analysis, or proof outline in the supplied text. This is load-bearing for the primary contribution and prevents verification of the claimed complexity bound.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their review. The abstract is a high-level summary; the full manuscript contains the explicit construction, product automaton, complexity analysis (O(|Q|·|M|·|A|)), and correctness proof for the polynomial-time PMC procedure. We address the single major comment below.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the central claim of a 'first polynomial-time algorithm' for PMC against FDFA (and its extension to FUFA) is asserted without any derivation steps, construction details, complexity analysis, or proof outline in the supplied text. This is load-bearing for the primary contribution and prevents verification of the claimed complexity bound.

    Authors: The supplied abstract is intentionally concise. The complete derivation appears in the body: Section 4 defines the product of a DTMC with an FDFA (leading DFA plus family of DFAs), reduces the problem to solving a linear system whose size is polynomial in the input, and proves the resulting probability is computed in polynomial time. Section 5 extends the same construction to FUFAs whose leading automaton is deterministic. We are happy to append a one-sentence proof sketch to the abstract in the revised version. revision: partial

Circularity Check

0 steps flagged

No significant circularity; derivation rests on standard automata constructions and new algorithm presentation

full rationale

The abstract and available text present a new polynomial-time PMC algorithm for FDFA properties on DTMCs and an extension to FUFA with deterministic leading automaton. No equations, reductions, or self-citations are shown that would make any claimed probability or translation equivalent to its inputs by construction. The work introduces FUFA as a new model and contrasts its succinctness with FDFA and other automata, without load-bearing reliance on prior self-citations or fitted parameters renamed as predictions. The derivation chain appears self-contained against external automata theory benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Based on the abstract alone, the work relies on standard automata-theoretic background (closure properties of ω-regular languages, existence of ultimately periodic words) rather than new free parameters or invented entities; no ad-hoc constants or postulated objects are mentioned.

axioms (1)
  • domain assumption ω-regular languages are characterized by families of deterministic finite automata processing ultimately periodic words
    Invoked in the opening definition of FDFA and the claim that they characterize ω-regular languages.

pith-pipeline@v0.9.1-grok · 5812 in / 1249 out tokens · 20491 ms · 2026-06-26T11:05:44.876940+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

38 extracted references · 18 canonical work pages · 1 internal anchor

  1. [1]

    Principles of Model Checking , publisher =

    Christel Baier and Joost. Principles of Model Checking , publisher =. 2008 , isbn =

    2008

  2. [2]

    Saturation Problems for Families of Automata , booktitle =

    Bohn, Le\'. Saturation Problems for Families of Automata , booktitle =. 2025 , volume =

    2025

  3. [3]

    Families of

    Dana Angluin and Udi Boker and Dana Fisman , doi =. Families of. Logical Methods in Computer Science , issn =. 2018 , month =

    2018

  4. [4]

    Ultimately periodic words of rational -languages , doi =

    Calbrix, Hugues and Nivat, Maurice and Podelski, Andreas , editor =. Ultimately periodic words of rational -languages , doi =. Mathematical. 1994 , pages =

    1994

  5. [5]

    Learning regular omega languages , volume =

    Angluin, Dana and Fisman, Dana , month = oct, year =. Learning regular omega languages , volume =. doi:10.1016/j.tcs.2016.07.031 , journal =

    work page doi:10.1016/j.tcs.2016.07.031 2016

  6. [6]

    A Novel Learning Algorithm for B\"uchi Automata based on Family of DFA s and Classification Trees

    Li, Yong and Chen, Yu-Fang and Zhang, Lijun and Liu, Depeng. A Novel Learning Algorithm for B\"uchi Automata based on Family of DFA s and Classification Trees. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017). 2017. doi:10.1007/978-3-662-54577-5_12

    work page doi:10.1007/978-3-662-54577-5_12 2017

  7. [7]

    A Novel Family of Finite Automata for Recognizing and Learning -Regular Languages

    Li, Yong and Schewe, Sven and Tang, Qiyi. A Novel Family of Finite Automata for Recognizing and Learning -Regular Languages. Automated Technology for Verification and Analysis. 2023. doi:10.1007/978-3-031-45329-8_3

    work page doi:10.1007/978-3-031-45329-8_3 2023

  8. [8]

    and Snell, J

    Kemeny, John G. and Snell, J. Laurie , series=. Finite. 1976 , publisher=

    1976

  9. [9]

    Lower Bounds for Unambiguous Automata via Communication Complexity , booktitle =

    G\". Lower Bounds for Unambiguous Automata via Communication Complexity , booktitle =. 2022 , volume =

    2022

  10. [10]

    Richard B\" u chi

    Symposium on Decision Problems: On a Decision Method in Restricted Second Order Arithmetic , editor =. 1966 , booktitle =. doi:https://doi.org/10.1016/S0049-237X(09)70564-6 , author =

    work page doi:10.1016/s0049-237x(09)70564-6 1966

  11. [11]

    45th International Colloquium on Automata, Languages, and Programming (ICALP 2018) , pages =

    Raskin, Mikhail , title =. 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018) , pages =. 2018 , volume =

    2018

  12. [12]

    Unambiguity in Automata Theory , booktitle =

    Colcombet, Thomas , editor =. Unambiguity in Automata Theory , booktitle =. 2015 , doi =

    2015

  13. [13]

    Stearns, R. E. and Hunt III, H. B. , title =. SIAM Journal on Computing , volume =. 1985 , doi =

    1985

  14. [14]

    Markov chains and unambiguous automata , volume =

    Baier, Christel and Kiefer, Stefan and Klein, Joachim and Müller, David and Worrell, James , month = sep, year =. Markov chains and unambiguous automata , volume =. doi:10.1016/j.jcss.2023.03.005 , journal =

    work page doi:10.1016/j.jcss.2023.03.005 2023

  15. [15]

    Translating

    Li, Jianlin , note =. Translating

  16. [16]

    Fisman, Dana , title =

  17. [17]

    Chandra and Dexter C

    Chandra, Ashok K. and Kozen, Dexter C. and Stockmeyer, Larry J. , title =. 1981 , issue_date =. doi:10.1145/322234.322243 , journal =

    work page doi:10.1145/322234.322243 1981

  18. [18]

    A Unified Translation of Linear Temporal Logic to -Automata , year =

    Esparza, Javier and K. A Unified Translation of Linear Temporal Logic to -Automata , year =. doi:10.1145/3417995 , journal =

    work page doi:10.1145/3417995

  19. [19]

    From LTL and Limit-Deterministic B \"u chi Automata to Deterministic Parity Automata

    Esparza, Javier and K r et \'i nsk \'y , Jan and Raskin, Jean-Fran c ois and Sickert, Salomon. From LTL and Limit-Deterministic B \"u chi Automata to Deterministic Parity Automata. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017). 2017. doi:10.1007/978-3-662-54577-5_25

    work page doi:10.1007/978-3-662-54577-5_25 2017

  20. [20]

    1977 , publisher =

    Pnueli, Amir , title =. 1977 , publisher =. doi:10.1109/SFCS.1977.32 , booktitle =

    work page doi:10.1109/sfcs.1977.32 1977

  21. [21]

    and Zhang, Lijun

    Li, Yong and Tsay, Yih-Kuen and Turrini, Andrea and Vardi, Moshe Y. and Zhang, Lijun. Congruence Relations for B \"u chi Automata. Formal Methods (FM 2021). 2021. doi:10.1007/978-3-030-90870-6_25

    work page doi:10.1007/978-3-030-90870-6_25 2021

  22. [22]

    Descriptional Complexity of

    Leung, Hing , month = jan, year =. Descriptional Complexity of. doi:10.1142/S0129054105003418 , journal =

    work page doi:10.1142/s0129054105003418

  23. [23]

    1978 , school =

    Succinctness of Descriptions of Context-Free, Regular, and Finite Languages , author =. 1978 , school =

    1978

  24. [24]

    The complexity of probabilistic verification , volume =. J. ACM , author =. 1995 , pages =. doi:10.1145/210332.210339 , number =

    work page doi:10.1145/210332.210339 1995

  25. [25]

    Facets of Synthesis: Revisiting Church 's Problem

    Thomas, Wolfgang. Facets of Synthesis: Revisiting Church 's Problem. Foundations of Software Science and Computational Structures (FoSSaCS 2009). 2009. doi:10.1007/978-3-642-00596-1_1

    work page doi:10.1007/978-3-642-00596-1_1 2009

  26. [26]

    and Rosner, R

    Pnueli, A. and Rosner, R. , title =. 1989 , publisher =. doi:10.1145/75277.75293 , booktitle =

    work page doi:10.1145/75277.75293 1989

  27. [27]

    Vardi and Pierre Wolper , title =

    Moshe Y. Vardi and Pierre Wolper , title =. Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986) , year =

    1986

  28. [28]

    CoRR , volume =

    Thomas Wilke , title =. CoRR , volume =. 2016 , doi =

    2016

  29. [29]

    2002 , doi =

    Automata, Logics, and Infinite Games , subtitle =. 2002 , doi =

    2002

  30. [30]

    , title =

    Kupferman, Orna and Vardi, Moshe Y. , title =. 2005 , issue_date =. doi:10.1145/1055686.1055689 , journal =

    work page doi:10.1145/1055686.1055689 2005

  31. [31]

    , booktitle=

    Vardi, Moshe Y. , booktitle=. Automatic verification of probabilistic concurrent finite state programs , year=

  32. [32]

    CoRR , volume =

    Michael Benedikt and Rastislav Lenhardt and James Worrell , title =. CoRR , volume =. 2014 , doi =

    2014

  33. [33]

    SIAM Journal on Computing , author =

    Separating Exponentially Ambiguous Finite Automata from Polynomially Ambiguous Finite Automata , volume =. SIAM Journal on Computing , author =. 1998 , pages =. doi:10.1137/S0097539793252092 , number =

    work page doi:10.1137/s0097539793252092 1998

  34. [34]

    On Finitely Ambiguous

    Löding, Christof and Pirogov, Anton , editor =. On Finitely Ambiguous. 2018 , pages =. doi:10.1007/978-3-319-98654-8_41 , booktitle =

    work page doi:10.1007/978-3-319-98654-8_41 2018

  35. [35]

    CNET, Paris , volume=

    Complementation is more difficult with automata on infinite words , author=. CNET, Paris , volume=

  36. [36]

    Optimal Bounds for Transformations of -Automata , doi =

    Löding, Christof , editor =. Optimal Bounds for Transformations of -Automata , doi =. Foundations of. 1999 , pages =

    1999

  37. [37]

    , booktitle=

    Piterman, N. , booktitle=. From Nondeterministic. 2006 , pages=

    2006

  38. [38]

    Characterizing LTL Formulas by Examples

    Cate, Balder ten and Fisman, Dana and Ohayon, Roi and Sestic, Patrik , month = apr, year =. Characterizing. doi:10.48550/arXiv.2604.22097 , publisher =

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.2604.22097