Document

**Published in:** LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

We consider the Sequential Probability Ratio Test applied to Hidden Markov Models. Given two Hidden Markov Models and a sequence of observations generated by one of them, the Sequential Probability Ratio Test attempts to decide which model produced the sequence. We show relationships between the execution time of such an algorithm and Lyapunov exponents of random matrix systems. Further, we give complexity results about the execution time taken by the Sequential Probability Ratio Test.

Oscar Darwin and Stefan Kiefer. On the Sequential Probability Ratio Test in Hidden Markov Models. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 9:1-9:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{darwin_et_al:LIPIcs.CONCUR.2022.9, author = {Darwin, Oscar and Kiefer, Stefan}, title = {{On the Sequential Probability Ratio Test in Hidden Markov Models}}, booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)}, pages = {9:1--9:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-246-4}, ISSN = {1868-8969}, year = {2022}, volume = {243}, editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.9}, URN = {urn:nbn:de:0030-drops-170728}, doi = {10.4230/LIPIcs.CONCUR.2022.9}, annote = {Keywords: Markov chains, hidden Markov models, probabilistic systems, verification} }

Document

**Published in:** LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

A labelled Markov decision process (MDP) is a labelled Markov chain with nondeterminism; i.e., together with a strategy a labelled MDP induces a labelled Markov chain. Motivated by applications to the verification of probabilistic noninterference in security, we study problems whether there exist strategies such that the labelled MDPs become bisimilarity equivalent/inequivalent. We show that the equivalence problem is decidable; in fact, it is EXPTIME-complete and becomes NP-complete if one of the MDPs is a Markov chain. Concerning the inequivalence problem, we show that (1) it is decidable in polynomial time; (2) if there are strategies for inequivalence then there are memoryless strategies for inequivalence; (3) such memoryless strategies can be computed in polynomial time.

Stefan Kiefer and Qiyi Tang. Strategies for MDP Bisimilarity Equivalence and Inequivalence. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 32:1-32:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{kiefer_et_al:LIPIcs.CONCUR.2022.32, author = {Kiefer, Stefan and Tang, Qiyi}, title = {{Strategies for MDP Bisimilarity Equivalence and Inequivalence}}, booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)}, pages = {32:1--32:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-246-4}, ISSN = {1868-8969}, year = {2022}, volume = {243}, editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.32}, URN = {urn:nbn:de:0030-drops-170955}, doi = {10.4230/LIPIcs.CONCUR.2022.32}, annote = {Keywords: Markov decision processes, Markov chains} }

Document

Track B: Automata, Logic, Semantics, and Theory of Programming

**Published in:** LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)

We use results from communication complexity, both new and old ones, to prove lower bounds for unambiguous finite automata (UFAs). We show three results.
1) Complement: There is a language L recognised by an n-state UFA such that the complement language ̅L requires NFAs with n^Ω̃(log n) states. This improves on a lower bound by Raskin.
2) Union: There are languages L₁, L₂ recognised by n-state UFAs such that the union L₁∪L₂ requires UFAs with n^Ω̃(log n) states.
3) Separation: There is a language L such that both L and ̅L are recognised by n-state NFAs but such that L requires UFAs with n^Ω(log n) states. This refutes a conjecture by Colcombet.

Mika Göös, Stefan Kiefer, and Weiqiang Yuan. Lower Bounds for Unambiguous Automata via Communication Complexity. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 126:1-126:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{goos_et_al:LIPIcs.ICALP.2022.126, author = {G\"{o}\"{o}s, Mika and Kiefer, Stefan and Yuan, Weiqiang}, title = {{Lower Bounds for Unambiguous Automata via Communication Complexity}}, booktitle = {49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)}, pages = {126:1--126:13}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-235-8}, ISSN = {1868-8969}, year = {2022}, volume = {229}, editor = {Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.126}, URN = {urn:nbn:de:0030-drops-164679}, doi = {10.4230/LIPIcs.ICALP.2022.126}, annote = {Keywords: Unambiguous automata, communication complexity} }

Document

**Published in:** LIPIcs, Volume 213, 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)

We propose polynomial-time algorithms to minimise labelled Markov chains whose transition probabilities are not known exactly, have been perturbed, or can only be obtained by sampling. Our algorithms are based on a new notion of an approximate bisimulation quotient, obtained by lumping together states that are exactly bisimilar in a slightly perturbed system. We present experiments that show that our algorithms are able to recover the structure of the bisimulation quotient of the unperturbed system.

Stefan Kiefer and Qiyi Tang. Approximate Bisimulation Minimisation. In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 213, pp. 48:1-48:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{kiefer_et_al:LIPIcs.FSTTCS.2021.48, author = {Kiefer, Stefan and Tang, Qiyi}, title = {{Approximate Bisimulation Minimisation}}, booktitle = {41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)}, pages = {48:1--48:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-215-0}, ISSN = {1868-8969}, year = {2021}, volume = {213}, editor = {Boja\'{n}czyk, Miko{\l}aj and Chekuri, Chandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2021.48}, URN = {urn:nbn:de:0030-drops-155599}, doi = {10.4230/LIPIcs.FSTTCS.2021.48}, annote = {Keywords: Markov chains, Behavioural metrics, Bisimulation} }

Document

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

Restarts are used in many computer systems to improve performance. Examples include reloading a webpage, reissuing a request, or restarting a randomized search. The design of restart strategies has been extensively studied by the performance evaluation community. In this paper, we address the problem of designing universal restart strategies, valid for arbitrary finite-state Markov chains, that enforce a given ω-regular property while not knowing the chain. A strategy enforces a property φ if, with probability 1, the number of restarts is finite, and the run of the Markov chain after the last restart satisfies φ. We design a simple "cautious" strategy that solves the problem, and a more sophisticated "bold" strategy with an almost optimal number of restarts.

Javier Esparza, Stefan Kiefer, Jan Křetínský, and Maximilian Weininger. Enforcing ω-Regular Properties in Markov Chains by Restarting. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 5:1-5:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{esparza_et_al:LIPIcs.CONCUR.2021.5, author = {Esparza, Javier and Kiefer, Stefan and K\v{r}et{\'\i}nsk\'{y}, Jan and Weininger, Maximilian}, title = {{Enforcing \omega-Regular Properties in Markov Chains by Restarting}}, booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)}, pages = {5:1--5:22}, 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.5}, URN = {urn:nbn:de:0030-drops-143824}, doi = {10.4230/LIPIcs.CONCUR.2021.5}, annote = {Keywords: Markov chains, omega-regular properties, runtime enforcement} }

Document

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

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

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

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

The Transience objective is not to visit any state infinitely often. While this is not possible in any finite Markov Decision Process (MDP), it can be satisfied in countably infinite ones, e.g., if the transition graph is acyclic.
We prove the following fundamental properties of Transience in countably infinite MDPs.
1) There exist uniformly ε-optimal MD strategies (memoryless deterministic) for Transience, even in infinitely branching MDPs.
2) Optimal strategies for Transience need not exist, even if the MDP is finitely branching. However, if an optimal strategy exists then there is also an optimal MD strategy.
3) If an MDP is universally transient (i.e., almost surely transient under all strategies) then many other objectives have a lower strategy complexity than in general MDPs. E.g., ε-optimal strategies for Safety and co-Büchi and optimal strategies for {0,1,2}-Parity (where they exist) can be chosen MD, even if the MDP is infinitely branching.

Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, and Patrick Totzke. Transience in Countable MDPs. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 11:1-11:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{kiefer_et_al:LIPIcs.CONCUR.2021.11, author = {Kiefer, Stefan and Mayr, Richard and Shirmohammadi, Mahsa and Totzke, Patrick}, title = {{Transience in Countable MDPs}}, booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)}, pages = {11:1--11:15}, 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.11}, URN = {urn:nbn:de:0030-drops-143881}, doi = {10.4230/LIPIcs.CONCUR.2021.11}, annote = {Keywords: Markov decision processes, Parity, Transience} }

Document

**Published in:** LIPIcs, Volume 182, 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)

We consider Hidden Markov Models that emit sequences of observations that are drawn from continuous distributions. For example, such a model may emit a sequence of numbers, each of which is drawn from a uniform distribution, but the support of the uniform distribution depends on the state of the Hidden Markov Model. Such models generalise the more common version where each observation is drawn from a finite alphabet. We prove that one can determine in polynomial time whether two Hidden Markov Models with continuous observations are equivalent.

Oscar Darwin and Stefan Kiefer. Equivalence of Hidden Markov Models with Continuous Observations. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 43:1-43:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{darwin_et_al:LIPIcs.FSTTCS.2020.43, author = {Darwin, Oscar and Kiefer, Stefan}, title = {{Equivalence of Hidden Markov Models with Continuous Observations}}, booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)}, pages = {43:1--43:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-174-0}, ISSN = {1868-8969}, year = {2020}, volume = {182}, editor = {Saxena, Nitin and Simon, Sunil}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.43}, URN = {urn:nbn:de:0030-drops-132845}, doi = {10.4230/LIPIcs.FSTTCS.2020.43}, annote = {Keywords: Markov chains, equivalence, probabilistic systems, verification} }

Document

**Published in:** LIPIcs, Volume 182, 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)

A labelled Markov decision process is a labelled Markov chain with nondeterminism, i.e., together with a strategy a labelled MDP induces a labelled Markov chain. The model is related to interval Markov chains. Motivated by applications of equivalence checking for the verification of anonymity, we study the algorithmic comparison of two labelled MDPs, in particular, whether there exist strategies such that the MDPs become equivalent/inequivalent, both in terms of trace equivalence and in terms of probabilistic bisimilarity. We provide the first polynomial-time algorithms for computing memoryless strategies to make the two labelled MDPs inequivalent if such strategies exist. We also study the computational complexity of qualitative problems about making the total variation distance and the probabilistic bisimilarity distance less than one or equal to one.

Stefan Kiefer and Qiyi Tang. Comparing Labelled Markov Decision Processes. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 49:1-49:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{kiefer_et_al:LIPIcs.FSTTCS.2020.49, author = {Kiefer, Stefan and Tang, Qiyi}, title = {{Comparing Labelled Markov Decision Processes}}, booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)}, pages = {49:1--49:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-174-0}, ISSN = {1868-8969}, year = {2020}, volume = {182}, editor = {Saxena, Nitin and Simon, Sunil}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.49}, URN = {urn:nbn:de:0030-drops-132903}, doi = {10.4230/LIPIcs.FSTTCS.2020.49}, annote = {Keywords: Markov decision processes, Markov chains, Behavioural metrics} }

Document

**Published in:** LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

We study countably infinite MDPs with parity objectives. Unlike in finite MDPs, optimal strategies need not exist, and may require infinite memory if they do. We provide a complete picture of the exact strategy complexity of ε-optimal strategies (and optimal strategies, where they exist) for all subclasses of parity objectives in the Mostowski hierarchy. Either MD-strategies, Markov strategies, or 1-bit Markov strategies are necessary and sufficient, depending on the number of colors, the branching degree of the MDP, and whether one considers ε-optimal or optimal strategies. In particular, 1-bit Markov strategies are necessary and sufficient for ε-optimal (resp. optimal) strategies for general parity objectives.

Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, and Patrick Totzke. Strategy Complexity of Parity Objectives in Countable MDPs. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 39:1-39:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{kiefer_et_al:LIPIcs.CONCUR.2020.39, author = {Kiefer, Stefan and Mayr, Richard and Shirmohammadi, Mahsa and Totzke, Patrick}, title = {{Strategy Complexity of Parity Objectives in Countable MDPs}}, booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)}, pages = {39:1--39:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-160-3}, ISSN = {1868-8969}, year = {2020}, volume = {171}, editor = {Konnov, Igor and Kov\'{a}cs, Laura}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.39}, URN = {urn:nbn:de:0030-drops-128513}, doi = {10.4230/LIPIcs.CONCUR.2020.39}, annote = {Keywords: Markov decision processes, Parity objectives, Levy’s zero-one law} }

Document

**Published in:** LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Given two weighted automata, we consider the problem of whether one is big-O of the other, i.e., if the weight of every finite word in the first is not greater than some constant multiple of the weight in the second.
We show that the problem is undecidable, even for the instantiation of weighted automata as labelled Markov chains. Moreover, even when it is known that one weighted automaton is big-O of another, the problem of finding or approximating the associated constant is also undecidable.
Our positive results show that the big-O problem is polynomial-time solvable for unambiguous automata, coNP-complete for unlabelled weighted automata (i.e., when the alphabet is a single character) and decidable, subject to Schanuel’s conjecture, when the language is bounded (i.e., a subset of w_1^* … w_m^* for some finite words w_1,… ,w_m).
On labelled Markov chains, the problem can be restated as a ratio total variation distance, which, instead of finding the maximum difference between the probabilities of any two events, finds the maximum ratio between the probabilities of any two events. The problem is related to ε-differential privacy, for which the optimal constant of the big-O notation is exactly exp(ε).

Dmitry Chistikov, Stefan Kiefer, Andrzej S. Murawski, and David Purser. The Big-O Problem for Labelled Markov Chains and Weighted Automata. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 41:1-41:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{chistikov_et_al:LIPIcs.CONCUR.2020.41, author = {Chistikov, Dmitry and Kiefer, Stefan and Murawski, Andrzej S. and Purser, David}, title = {{The Big-O Problem for Labelled Markov Chains and Weighted Automata}}, booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)}, pages = {41:1--41:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-160-3}, ISSN = {1868-8969}, year = {2020}, volume = {171}, editor = {Konnov, Igor and Kov\'{a}cs, Laura}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.41}, URN = {urn:nbn:de:0030-drops-128534}, doi = {10.4230/LIPIcs.CONCUR.2020.41}, annote = {Keywords: weighted automata, labelled Markov chains, probabilistic systems} }

Document

**Published in:** LIPIcs, Volume 170, 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)

We analyze affine reachability problems in dimensions 1 and 2. We show that the reachability problem for 1-register machines over the integers with affine updates is PSPACE-hard, hence PSPACE-complete, strengthening a result by Finkel et al. that required polynomial updates. Building on recent results on two-dimensional integer matrices, we prove NP-completeness of the mortality problem for 2-dimensional integer matrices with determinants +1 and 0. Motivated by tight connections with 1-dimensional affine reachability problems without control states, we also study the complexity of a number of reachability problems in finitely generated semigroups of 2-dimensional upper-triangular integer matrices.

Stefan Jaax and Stefan Kiefer. On Affine Reachability Problems. In 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 170, pp. 48:1-48:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{jaax_et_al:LIPIcs.MFCS.2020.48, author = {Jaax, Stefan and Kiefer, Stefan}, title = {{On Affine Reachability Problems}}, booktitle = {45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)}, pages = {48:1--48:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-159-7}, ISSN = {1868-8969}, year = {2020}, volume = {170}, editor = {Esparza, Javier and Kr\'{a}l', Daniel}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2020.48}, URN = {urn:nbn:de:0030-drops-127148}, doi = {10.4230/LIPIcs.MFCS.2020.48}, annote = {Keywords: Counter Machines, Matrix Semigroups, Reachability} }

Document

Invited Talk

**Published in:** LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)

Markov decision processes (MDPs) are a standard model for dynamic systems that exhibit both stochastic and nondeterministic behavior. For MDPs with finite state space it is known that for a wide range of objectives there exist optimal strategies that are memoryless and deterministic. In contrast, if the state space is infinite, optimal strategies may not exist, and optimal or ε-optimal strategies may require (possibly infinite) memory. In this paper we consider qualitative objectives: reachability, safety, (co-)Büchi, and other parity objectives. We aim at giving an introduction to a collection of techniques that allow for the construction of strategies with little or no memory in countably infinite MDPs.

Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, Patrick Totzke, and Dominik Wojtczak. How to Play in Infinite MDPs (Invited Talk). In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 3:1-3:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{kiefer_et_al:LIPIcs.ICALP.2020.3, author = {Kiefer, Stefan and Mayr, Richard and Shirmohammadi, Mahsa and Totzke, Patrick and Wojtczak, Dominik}, title = {{How to Play in Infinite MDPs}}, booktitle = {47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)}, pages = {3:1--3:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-138-2}, ISSN = {1868-8969}, year = {2020}, volume = {168}, editor = {Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.3}, URN = {urn:nbn:de:0030-drops-124103}, doi = {10.4230/LIPIcs.ICALP.2020.3}, annote = {Keywords: Markov decision processes} }

Document

Track B: Automata, Logic, Semantics, and Theory of Programming

**Published in:** LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)

Let n be a positive integer and M a set of rational n × n-matrices such that M generates a finite multiplicative semigroup. We show that any matrix in the semigroup is a product of matrices in M whose length is at most 2^{n (2 n + 3)} g(n)^{n+1} ∈ 2^{O(n² log n)}, where g(n) is the maximum order of finite groups over rational n × n-matrices. This result implies algorithms with an elementary running time for deciding finiteness of weighted automata over the rationals and for deciding reachability in affine integer vector addition systems with states with the finite monoid property.

Georgina Bumpus, Christoph Haase, Stefan Kiefer, Paul-Ioan Stoienescu, and Jonathan Tanner. On the Size of Finite Rational Matrix Semigroups. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 115:1-115:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{bumpus_et_al:LIPIcs.ICALP.2020.115, author = {Bumpus, Georgina and Haase, Christoph and Kiefer, Stefan and Stoienescu, Paul-Ioan and Tanner, Jonathan}, title = {{On the Size of Finite Rational Matrix Semigroups}}, booktitle = {47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)}, pages = {115:1--115:13}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-138-2}, ISSN = {1868-8969}, year = {2020}, volume = {168}, editor = {Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.115}, URN = {urn:nbn:de:0030-drops-125226}, doi = {10.4230/LIPIcs.ICALP.2020.115}, annote = {Keywords: Matrix semigroups, Burnside problem, weighted automata, vector addition systems} }

Document

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

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

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

Document

Track B: Automata, Logic, Semantics, and Theory of Programming

**Published in:** LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)

Value iteration is a fundamental algorithm for solving Markov Decision Processes (MDPs). It computes the maximal n-step payoff by iterating n times a recurrence equation which is naturally associated to the MDP. At the same time, value iteration provides a policy for the MDP that is optimal on a given finite horizon n. In this paper, we settle the computational complexity of value iteration. We show that, given a horizon n in binary and an MDP, computing an optimal policy is EXPTIME-complete, thus resolving an open problem that goes back to the seminal 1987 paper on the complexity of MDPs by Papadimitriou and Tsitsiklis. To obtain this main result, we develop several stepping stones that yield results of an independent interest. For instance, we show that it is EXPTIME-complete to compute the n-fold iteration (with n in binary) of a function given by a straight-line program over the integers with max and + as operators. We also provide new complexity results for the bounded halting problem in linear-update counter machines.

Nikhil Balaji, Stefan Kiefer, Petr Novotný, Guillermo A. Pérez, and Mahsa Shirmohammadi. On the Complexity of Value Iteration (Track B: Automata, Logic, Semantics, and Theory of Programming). In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 102:1-102:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{balaji_et_al:LIPIcs.ICALP.2019.102, author = {Balaji, Nikhil and Kiefer, Stefan and Novotn\'{y}, Petr and P\'{e}rez, Guillermo A. and Shirmohammadi, Mahsa}, title = {{On the Complexity of Value Iteration}}, booktitle = {46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)}, pages = {102:1--102:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-109-2}, ISSN = {1868-8969}, year = {2019}, volume = {132}, editor = {Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.102}, URN = {urn:nbn:de:0030-drops-106782}, doi = {10.4230/LIPIcs.ICALP.2019.102}, annote = {Keywords: Markov decision processes, Value iteration, Formal verification} }

Document

Track B: Automata, Logic, Semantics, and Theory of Programming

**Published in:** LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)

We study countably infinite Markov decision processes with Büchi objectives, which ask to visit a given subset F of states infinitely often. A question left open by T.P. Hill in 1979 [Theodore Preston Hill, 1979] is whether there always exist epsilon-optimal Markov strategies, i.e., strategies that base decisions only on the current state and the number of steps taken so far. We provide a negative answer to this question by constructing a non-trivial counterexample. On the other hand, we show that Markov strategies with only 1 bit of extra memory are sufficient.

Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, and Patrick Totzke. Büchi Objectives in Countable MDPs (Track B: Automata, Logic, Semantics, and Theory of Programming). In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 119:1-119:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{kiefer_et_al:LIPIcs.ICALP.2019.119, author = {Kiefer, Stefan and Mayr, Richard and Shirmohammadi, Mahsa and Totzke, Patrick}, title = {{B\"{u}chi Objectives in Countable MDPs}}, booktitle = {46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)}, pages = {119:1--119:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-109-2}, ISSN = {1868-8969}, year = {2019}, volume = {132}, editor = {Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.119}, URN = {urn:nbn:de:0030-drops-106959}, doi = {10.4230/LIPIcs.ICALP.2019.119}, annote = {Keywords: Markov decision processes} }

Document

**Published in:** LIPIcs, Volume 126, 36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019)

Let n be a natural number and M a set of n x n-matrices over the nonnegative integers such that M generates a finite multiplicative monoid. We show that if the zero matrix 0 is a product of matrices in M, then there are M_1, ..., M_{n^5} in M with M_1 *s M_{n^5} = 0. This result has applications in automata theory and the theory of codes. Specifically, if X subset Sigma^* is a finite incomplete code, then there exists a word w in Sigma^* of length polynomial in sum_{x in X} |x| such that w is not a factor of any word in X^*. This proves a weak version of Restivo’s conjecture.

Stefan Kiefer and Corto Mascle. On Finite Monoids over Nonnegative Integer Matrices and Short Killing Words. In 36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 126, pp. 43:1-43:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{kiefer_et_al:LIPIcs.STACS.2019.43, author = {Kiefer, Stefan and Mascle, Corto}, title = {{On Finite Monoids over Nonnegative Integer Matrices and Short Killing Words}}, booktitle = {36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019)}, pages = {43:1--43:13}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-100-9}, ISSN = {1868-8969}, year = {2019}, volume = {126}, editor = {Niedermeier, Rolf and Paul, Christophe}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2019.43}, URN = {urn:nbn:de:0030-drops-102823}, doi = {10.4230/LIPIcs.STACS.2019.43}, annote = {Keywords: matrix semigroups, unambiguous automata, codes, Restivo’s conjecture} }

Document

**Published in:** LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

We study selective monitors for labelled Markov chains. Monitors observe the outputs that are generated by a Markov chain during its run, with the goal of identifying runs as correct or faulty. A monitor is selective if it skips observations in order to reduce monitoring overhead. We are interested in monitors that minimize the expected number of observations. We establish an undecidability result for selectively monitoring general Markov chains. On the other hand, we show for non-hidden Markov chains (where any output identifies the state the Markov chain is in) that simple optimal monitors exist and can be computed efficiently, based on DFA language equivalence. These monitors do not depend on the precise transition probabilities in the Markov chain. We report on experiments where we compute these monitors for several open-source Java projects.

Radu Grigore and Stefan Kiefer. Selective Monitoring. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 20:1-20:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{grigore_et_al:LIPIcs.CONCUR.2018.20, author = {Grigore, Radu and Kiefer, Stefan}, title = {{Selective Monitoring}}, booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)}, pages = {20:1--20:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-087-3}, ISSN = {1868-8969}, year = {2018}, volume = {118}, editor = {Schewe, Sven and Zhang, Lijun}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.20}, URN = {urn:nbn:de:0030-drops-95586}, doi = {10.4230/LIPIcs.CONCUR.2018.20}, annote = {Keywords: runtime monitoring, probabilistic systems, Markov chains, automata, language equivalence} }

Document

**Published in:** LIPIcs, Volume 107, 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)

We prove results on the decidability and complexity of computing the total variation distance (equivalently, the L_1-distance) of hidden Markov models (equivalently, labelled Markov chains). This distance measures the difference between the distributions on words that two hidden Markov models induce. The main results are: (1) it is undecidable whether the distance is greater than a given threshold; (2) approximation is #P-hard and in PSPACE.

Stefan Kiefer. On Computing the Total Variation Distance of Hidden Markov Models. In 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 107, pp. 130:1-130:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{kiefer:LIPIcs.ICALP.2018.130, author = {Kiefer, Stefan}, title = {{On Computing the Total Variation Distance of Hidden Markov Models}}, booktitle = {45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)}, pages = {130:1--130:13}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-076-7}, ISSN = {1868-8969}, year = {2018}, volume = {107}, editor = {Chatzigiannakis, Ioannis and Kaklamanis, Christos and Marx, D\'{a}niel and Sannella, Donald}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2018.130}, URN = {urn:nbn:de:0030-drops-91344}, doi = {10.4230/LIPIcs.ICALP.2018.130}, annote = {Keywords: Labelled Markov Chains, Hidden Markov Models, Distance, Decidability, Complexity} }

Document

**Published in:** LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

Given finite-state automata (or context-free grammars) A,B over the same alphabet and a Parikh vector p, we study the complexity of deciding whether the number of words in the language of A with Parikh image p is greater than the number of such words in the language of B. Recently, this problem turned out to be tightly related to the cost problem for weighted Markov chains. We classify the complexity according to whether A and B are deterministic, the size of the alphabet, and the encoding of p (binary or unary).

Christoph Haase, Stefan Kiefer, and Markus Lohrey. Counting Problems for Parikh Images. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 12:1-12:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{haase_et_al:LIPIcs.MFCS.2017.12, author = {Haase, Christoph and Kiefer, Stefan and Lohrey, Markus}, title = {{Counting Problems for Parikh Images}}, booktitle = {42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)}, pages = {12:1--12:13}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-046-0}, ISSN = {1868-8969}, year = {2017}, volume = {83}, editor = {Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.12}, URN = {urn:nbn:de:0030-drops-80597}, doi = {10.4230/LIPIcs.MFCS.2017.12}, annote = {Keywords: Parikh images, finite automata, counting problems} }

Document

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

Nonnegative matrix factorization (NMF) is the problem of decomposing a given nonnegative n*m matrix M into a product of a nonnegative n*d matrix W and a nonnegative d*m matrix H. Restricted NMF requires in addition that the column spaces of M and W coincide.
Finding the minimal inner dimension d is known to be NP-hard, both for NMF and restricted NMF. We show that restricted NMF is closely related to a question about the nature of minimal probabilistic automata, posed by Paz in his seminal 1971 textbook. We use this connection to answer Paz's question negatively, thus falsifying a positive answer claimed in 1974.
Furthermore, we investigate whether a rational matrix M always has a restricted NMF of minimal inner dimension whose factors W and H are also rational. We show that this holds for matrices M of rank at most 3 and we exhibit a rank-4 matrix for which W and H require irrational entries.

Dmitry Chistikov, Stefan Kiefer, Ines Marusic, Mahsa Shirmohammadi, and James Worrell. On Restricted Nonnegative Matrix Factorization. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 103:1-103:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{chistikov_et_al:LIPIcs.ICALP.2016.103, author = {Chistikov, Dmitry and Kiefer, Stefan and Marusic, Ines and Shirmohammadi, Mahsa and Worrell, James}, title = {{On Restricted Nonnegative Matrix Factorization}}, booktitle = {43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)}, pages = {103:1--103:14}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.103}, URN = {urn:nbn:de:0030-drops-62389}, doi = {10.4230/LIPIcs.ICALP.2016.103}, annote = {Keywords: nonnegative matrix factorization, nonnegative rank, probabilistic automata, labelled Markov chains, minimization} }

Document

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

Herman's self-stabilization algorithm, introduced 25 years ago, is a well-studied synchronous randomized protocol for enabling a ring of N processes collectively holding any odd number of tokens to reach a stable state in which a single token remains. Determining the worst-case expected time to stabilization is the central outstanding open problem about this protocol. It is known that there is a constant h such that any initial configuration has expected stabilization time at most hN2. Ten years ago, McIver and Morgan established a lower bound of 4/27 ~ 0.148 for h, achieved with three equally-spaced tokens, and conjectured this to be the optimal value of h. A series of papers over the last decade gradually reduced the upper bound on h, with the present record (achieved in 2014) standing at approximately 0.156. In this paper, we prove McIver and Morgan's conjecture and establish that h = 4/27 is indeed optimal.

Maria Bruna, Radu Grigore, Stefan Kiefer, Joël Ouaknine, and James Worrell. Proving the Herman-Protocol Conjecture. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 104:1-104:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{bruna_et_al:LIPIcs.ICALP.2016.104, author = {Bruna, Maria and Grigore, Radu and Kiefer, Stefan and Ouaknine, Jo\"{e}l and Worrell, James}, title = {{Proving the Herman-Protocol Conjecture}}, booktitle = {43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)}, pages = {104:1--104:12}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.104}, URN = {urn:nbn:de:0030-drops-62393}, doi = {10.4230/LIPIcs.ICALP.2016.104}, annote = {Keywords: randomized protocols, self-stabilization, Lyapunov function, expected time} }

Document

**Published in:** LIPIcs, Volume 18, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)

We study the bisimilarity problem for probabilistic pushdown automata (pPDA) and subclasses thereof. Our definition of pPDA allows both probabilistic and non-deterministic branching, generalising the classical notion of pushdown automata (without epsilon-transitions). Our first contribution is a general construction that reduces checking bisimilarity of probabilistic transition systems to checking bisimilarity of non-deterministic transition systems. This construction directly yields decidability of bisimilarity for pPDA, as well as an elementary upper bound for the bisimilarity problem on the subclass of probabilistic basic process algebras, i.e., single-state pPDA. We further show that, with careful analysis, the general reduction can be used to prove an EXPTIME upper bound for bisimilarity of probabilistic visibly pushdown automata. Here we also provide a matching lower bound, establishing EXPTIME-completeness. Finally we prove that deciding bisimilarity of probabilistic one-counter automata, another subclass of pPDA, is PSPACE-complete. Here we use a more specialised argument to obtain optimal complexity bounds.

Vojtech Forejt, Petr Jancar, Stefan Kiefer, and James Worrell. Bisimilarity of Probabilistic Pushdown Automata. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 448-460, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{forejt_et_al:LIPIcs.FSTTCS.2012.448, author = {Forejt, Vojtech and Jancar, Petr and Kiefer, Stefan and Worrell, James}, title = {{Bisimilarity of Probabilistic Pushdown Automata}}, booktitle = {IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)}, pages = {448--460}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-47-7}, ISSN = {1868-8969}, year = {2012}, volume = {18}, editor = {D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.448}, URN = {urn:nbn:de:0030-drops-38800}, doi = {10.4230/LIPIcs.FSTTCS.2012.448}, annote = {Keywords: bisimilarity, probabilistic systems, pushdown automata} }

Document

**Published in:** LIPIcs, Volume 14, 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)

Queueing networks are gaining attraction for the performance analysis of parallel computer systems. A Jackson network is a set of interconnected servers, where the completion of a job at server i may result in the creation of a new job for server j. We propose to extend Jackson networks by "branching" and by "control" features. Both extensions are new and substantially expand the modelling power of Jackson networks. On the other hand, the extensions raise computational questions, particularly concerning the stability of the networks, i.e, the ergodicity of the underlying Markov chain. We show for our extended model that it is decidable in polynomial time if there exists a controller that achieves stability. Moreover, if such a controller exists, one can efficiently compute a static randomized controller which stabilizes the network in a very strong sense; in particular, all moments of the queue sizes are finite.

Tomáš Brázdil and Stefan Kiefer. Stabilization of Branching Queueing Networks. In 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 14, pp. 507-518, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{brazdil_et_al:LIPIcs.STACS.2012.507, author = {Br\'{a}zdil, Tom\'{a}\v{s} and Kiefer, Stefan}, title = {{Stabilization of Branching Queueing Networks}}, booktitle = {29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)}, pages = {507--518}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-35-4}, ISSN = {1868-8969}, year = {2012}, volume = {14}, editor = {D\"{u}rr, Christoph and Wilke, Thomas}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2012.507}, URN = {urn:nbn:de:0030-drops-34133}, doi = {10.4230/LIPIcs.STACS.2012.507}, annote = {Keywords: continuous-time Markov decision processes, infinite-state systems, performance analysis} }

Document

**Published in:** LIPIcs, Volume 5, 27th International Symposium on Theoretical Aspects of Computer Science (2010)

We study systems of equations of the form $X_1 = f_1(X_1, \ldots, X_n), \ldots, X_n = f_n(X_1, \ldots, X_n)$ where each $f_i$ is a polynomial with nonnegative coefficients that add up to~$1$. The least nonnegative solution, say~$\mu$, of such equation systems is central to problems from various areas, like physics, biology, computational linguistics and probabilistic program verification. We give a simple and strongly polynomial algorithm to decide whether $\mu=(1,\ldots,1)$ holds. Furthermore, we present an algorithm that computes reliable sequences of lower and upper bounds on~$\mu$, converging linearly to~$\mu$.
Our algorithm has these features despite using inexact arithmetic for efficiency. We report on experiments that show the performance of our algorithms.

Javier Esparza, Andreas Gaiser, and Stefan Kiefer. Computing Least Fixed Points of Probabilistic Systems of Polynomials. In 27th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 5, pp. 359-370, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{esparza_et_al:LIPIcs.STACS.2010.2468, author = {Esparza, Javier and Gaiser, Andreas and Kiefer, Stefan}, title = {{Computing Least Fixed Points of Probabilistic Systems of Polynomials}}, booktitle = {27th International Symposium on Theoretical Aspects of Computer Science}, pages = {359--370}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-16-3}, ISSN = {1868-8969}, year = {2010}, volume = {5}, editor = {Marion, Jean-Yves and Schwentick, Thomas}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2010.2468}, URN = {urn:nbn:de:0030-drops-24685}, doi = {10.4230/LIPIcs.STACS.2010.2468}, annote = {Keywords: Computing fixed points, numerical approximation, stochastic models, branching processes} }

Document

**Published in:** LIPIcs, Volume 4, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2009)

We investigate the problem of evaluating memory consumption for systems modelled by probabilistic pushdown automata (pPDA). The space needed by a runof a pPDA is the maximal height reached by the stack during the run. Theproblem is motivated by the investigation of depth-first computations that playan important role for space-efficient schedulings of multithreaded programs.
We study the computation of both the distribution of the memory consumption and its expectation. For the distribution, we show that a naive method incurs anexponential blow-up, and that it can be avoided using linear equation systems.We also suggest a possibly even faster approximation method.Given~$\varepsilon>0$, these methods allow to compute bounds on the memoryconsumption that are exceeded with a probability of at most~$\varepsilon$.
For the expected memory consumption, we show that whether it is infinite can be decided in polynomial time for stateless pPDA (pBPA) and in polynomial space for pPDA. We also provide an iterative method for approximating theexpectation. We show how to compute error bounds of our approximation methodand analyze its convergence speed. We prove that our method convergeslinearly, i.e., the number of accurate bits of the approximation is a linear function of the number of iterations.

Tomas Brazdil, Javier Esparza, and Stefan Kiefer. On the Memory Consumption of Probabilistic Pushdown Automata. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 4, pp. 49-60, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{brazdil_et_al:LIPIcs.FSTTCS.2009.2306, author = {Brazdil, Tomas and Esparza, Javier and Kiefer, Stefan}, title = {{On the Memory Consumption of Probabilistic Pushdown Automata}}, booktitle = {IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science}, pages = {49--60}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-13-2}, ISSN = {1868-8969}, year = {2009}, volume = {4}, editor = {Kannan, Ravi and Narayan Kumar, K.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2009.2306}, URN = {urn:nbn:de:0030-drops-23067}, doi = {10.4230/LIPIcs.FSTTCS.2009.2306}, annote = {Keywords: Pushdown automata, probabilistic systems, verification} }

Document

**Published in:** LIPIcs, Volume 1, 25th International Symposium on Theoretical Aspects of Computer Science (2008)

Monotone systems of polynomial equations (MSPEs) are systems of
fixed-point equations $X_1 = f_1(X_1, ldots, X_n),$ $ldots, X_n =
f_n(X_1, ldots, X_n)$ where each $f_i$ is a polynomial with
positive real coefficients. The question of computing the least
non-negative solution of a given MSPE $vec X = vec f(vec X)$
arises naturally in the analysis of stochastic models such as
stochastic context-free grammars, probabilistic pushdown automata,
and back-button processes. Etessami and Yannakakis have recently
adapted Newton's iterative method to MSPEs. In a previous paper we
have proved the existence of a threshold $k_{vec f}$ for strongly
connected MSPEs, such that after $k_{vec f}$ iterations of
Newton's method each new iteration computes at least 1 new bit of
the solution. However, the proof was purely existential. In this
paper we give an upper bound for $k_{vec f}$ as a function of the
minimal component of the least fixed-point $muvec f$ of $vec
f(vec X)$. Using this result we show that $k_{vec f}$ is at most
single exponential resp. linear for strongly connected MSPEs
derived from probabilistic pushdown automata resp. from
back-button processes. Further, we prove the existence of a
threshold for arbitrary MSPEs after which each new iteration
computes at least $1/w2^h$ new bits of the solution, where $w$ and
$h$ are the width and height of the DAG of strongly connected
components.

Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Convergence Thresholds of Newton's Method for Monotone Polynomial Equations. In 25th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 1, pp. 289-300, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{esparza_et_al:LIPIcs.STACS.2008.1351, author = {Esparza, Javier and Kiefer, Stefan and Luttenberger, Michael}, title = {{Convergence Thresholds of Newton's Method for Monotone Polynomial Equations}}, booktitle = {25th International Symposium on Theoretical Aspects of Computer Science}, pages = {289--300}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-06-4}, ISSN = {1868-8969}, year = {2008}, volume = {1}, editor = {Albers, Susanne and Weil, Pascal}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2008.1351}, URN = {urn:nbn:de:0030-drops-13516}, doi = {10.4230/LIPIcs.STACS.2008.1351}, annote = {Keywords: Newton's Method, Fixed-Point Equations, Formal Verification of Software, Probabilistic Pushdown Systems} }

X

Feedback for Dagstuhl Publishing

Feedback submitted

Please try again later or send an E-mail