Probabilistic Model Checking via Families of Deterministic and Unambiguous Finite Automata

Christel BaierChristel Baier, Sascha KlüppelholzSascha Klüppelholz, Timm SporkTimm Spork

ISBN: 978-3-95977-447-5
ISSN: 1868-8969
Download
DOI Link

Christel Baier, Sascha Klüppelholz, Timm Spork
Probabilistic Model Checking via Families of Deterministic and Unambiguous Finite Automata
In Ana Sokolova, Patrick Totzke, eds., 37th International Conference on Concurrency Theory (CONCUR 2026), volume 391 of Leibniz International Proceedings in Informatics (LIPIcs), 15:1 - 15:19, August 2026. Schloss Dagstuhl- Leibniz-Zentrum für Informatik

Details
Bibtex

KurzfassungAbstract
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.
Projekt:Project: CPEC, CeTI, SECAI
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@InProceedings{baier_et_al:LIPIcs.CONCUR.2026.15,
  author =	{Baier, Christel and Kl\"{u}ppelholz, Sascha and Spork, Timm},
  title =	[[:Vorlage:Probabilistic Model Checking via Families of Deterministic and Unambiguous Finite Automata]],
  booktitle =	{37th International Conference on Concurrency Theory (CONCUR 2026)},
  pages =	{15:1--15:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-447-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{391},
  editor =	{Sokolova, Ana and Totzke, Patrick},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.15},
  URN =		{urn:nbn:de:0030-drops-273461},
  doi =		{10.4230/LIPIcs.CONCUR.2026.15},
  annote =	{Keywords: Families of Finite Automata, FDFA, Unambiguous Automata, Discrete-time Markov Chains, Probabilistic Model Checking, Verification}
}