DROPS

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.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.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}
}

Search Results

Documents authored by Widdershoven, Cas

Linear-Time Model Checking Branching Processes

Abstract

Cite as

Efficient Analysis of Unambiguous Automata Using Matrix Semigroup Techniques

Abstract

Cite as

Thanks for your feedback!

Could not send message