Search Results

Documents authored by Klüppelholz, Sascha

Document
DOI: 10.4230/LIPIcs.CONCUR.2026.15
Probabilistic Model Checking via Families of Deterministic and Unambiguous Finite Automata

Authors: Christel Baier, Sascha Klüppelholz, and Timm Spork

Published in: LIPIcs, Volume 391, 37th International Conference on Concurrency Theory (CONCUR 2026)

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

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)

Copy BibTex To Clipboard

@InProceedings{baier_et_al:LIPIcs.CONCUR.2026.15,
  author =	{Baier, Christel and Kl\"{u}ppelholz, Sascha and Spork, Timm},
  title =	{{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}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2016.102
Composition of Stochastic Transition Systems Based on Spans and Couplings

Authors: Daniel Gburek, Christel Baier, and Sascha Klüppelholz

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

Abstract
Conventional approaches for parallel composition of stochastic systems relate probability measures of the individual components in terms of product measures. Such approaches rely on the assumption that components interact stochastically independent, which might be too rigid for modeling real world systems. In this paper, we introduce a parallel-composition operator for stochastic transition systems that is based on couplings of probability measures and does not impose any stochastic assumptions. When composing systems within our framework, the intended dependencies between components can be determined by providing so-called spans and span couplings. We present a congruence result for our operator with respect to a standard notion of bisimilarity and develop a general theory for spans, exploiting deep results from descriptive set theory. As an application of our general approach, we propose a model for stochastic hybrid systems called stochastic hybrid motion automata.
Cite as

Daniel Gburek, Christel Baier, and Sascha Klüppelholz. Composition of Stochastic Transition Systems Based on Spans and Couplings. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 102:1-102:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{gburek_et_al:LIPIcs.ICALP.2016.102,
  author =	{Gburek, Daniel and Baier, Christel and Kl\"{u}ppelholz, Sascha},
  title =	{{Composition of Stochastic Transition Systems Based on Spans and Couplings}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{102:1--102:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.102},
  URN =		{urn:nbn:de:0030-drops-62379},
  doi =		{10.4230/LIPIcs.ICALP.2016.102},
  annote =	{Keywords: Stochastic Transition System, Composition, Stochastic Hybrid Motion Automata, Stochastically Independent, Coupling, Span, Bisimulation, Congruence, Po}
}
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