52 citations · 146 across the 41 of their papers we have counts for
14 papers · 1 filter
Linear-Time Model Checking Branching Processes
Stefan Kiefer, Pavel Semukhin, Cas Widdershoven
(Multi-type) branching processes are a natural and well-studied model for generating random infinite trees. Branching processes feature both nondeterministic and probabilistic bran…
Responsibility and verification: Importance value in temporal logics
Corto Mascle, Christel Baier, Florian Funke +2
We aim at measuring the influence of the nondeterministic choices of a part of a system on its ability to satisfy a specification. For this purpose, we apply the concept of Shapley…
Equivalence of Hidden Markov Models with Continuous Observations
Oscar Darwin, Stefan Kiefer
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…
Strategy Complexity of Parity Objectives in Countable MDPs
Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi +1
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…
Game Characterization of Probabilistic Bisimilarity, and Applications to Pushdown Automata
Vojtěch Forejt, Petr Jančar, Stefan Kiefer +1
We study the bisimilarity problem for probabilistic pushdown automata (pPDA) and subclasses thereof. Our definition of pPDA allows both probabilistic and non-deterministic branchin…
Parity Objectives in Countable MDPs
Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi +1
We study countably infinite MDPs with parity objectives, and special cases with a bounded number of colors in the Mostowski hierarchy (including reachability, safety, Buchi and co-…