2 Search Results for "Widdershoven, Cas"

Document
DOI: 10.4230/LIPIcs.CONCUR.2021.6
Linear-Time Model Checking Branching Processes

Authors: Stefan Kiefer, Pavel Semukhin, and Cas Widdershoven

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract
(Multi-type) branching processes are a natural and well-studied model for generating random infinite trees. Branching processes feature both nondeterministic and probabilistic branching, generalizing both transition systems and Markov chains (but not generally Markov decision processes). We study the complexity of model checking branching processes against linear-time omega-regular specifications: is it the case almost surely that every branch of a tree randomly generated by the branching process satisfies the omega-regular specification? The main result is that for LTL specifications this problem is in PSPACE, subsuming classical results for transition systems and Markov chains, respectively. The underlying general model-checking algorithm is based on the automata-theoretic approach, using unambiguous Büchi automata.
Cite as

Stefan Kiefer, Pavel Semukhin, and Cas Widdershoven. Linear-Time Model Checking Branching Processes. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 6:1-6:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{kiefer_et_al:LIPIcs.CONCUR.2021.6,
  author =	{Kiefer, Stefan and Semukhin, Pavel and Widdershoven, Cas},
  title =	{{Linear-Time Model Checking Branching Processes}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{6:1--6:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.6},
  URN =		{urn:nbn:de:0030-drops-143834},
  doi =		{10.4230/LIPIcs.CONCUR.2021.6},
  annote =	{Keywords: model checking, Markov chains, branching processes, automata, computational complexity}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2019.82
Efficient Analysis of Unambiguous Automata Using Matrix Semigroup Techniques

Authors: Stefan Kiefer and Cas Widdershoven

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)

Abstract
We introduce a novel technique to analyse unambiguous Büchi automata quantitatively, and apply this to the model checking problem. It is based on linear-algebra arguments that originate from the analysis of matrix semigroups with constant spectral radius. This method can replace a combinatorial procedure that dominates the computational complexity of the existing procedure by Baier et al. We analyse the complexity in detail, showing that, in terms of the set Q of states of the automaton, the new algorithm runs in time O(|Q|^4), improving on an efficient implementation of the combinatorial algorithm by a factor of |Q|.
Cite as

Stefan Kiefer and Cas Widdershoven. Efficient Analysis of Unambiguous Automata Using Matrix Semigroup Techniques. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 82:1-82:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{kiefer_et_al:LIPIcs.MFCS.2019.82,
  author =	{Kiefer, Stefan and Widdershoven, Cas},
  title =	{{Efficient Analysis of Unambiguous Automata Using Matrix Semigroup Techniques}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{82:1--82:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.82},
  URN =		{urn:nbn:de:0030-drops-110269},
  doi =		{10.4230/LIPIcs.MFCS.2019.82},
  annote =	{Keywords: Algorithms, Automata, Markov Chains, Matrix Semigroups}
}
  • Refine by Author
  • 2 Kiefer, Stefan
  • 2 Widdershoven, Cas
  • 1 Semukhin, Pavel

  • Refine by Classification
  • 2 Theory of computation → Automata over infinite objects
  • 1 Theory of computation → Design and analysis of algorithms
  • 1 Theory of computation → Verification by model checking

  • Refine by Keyword
  • 1 Algorithms
  • 1 Automata
  • 1 Markov Chains
  • 1 Markov chains
  • 1 Matrix Semigroups
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2019
  • 1 2021

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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