Author name cluster

Stefan Kiefer

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

14 papers

2 author rows

MFCS Conference 2025 Conference Paper

The Complexity of Reachability Problems in Strongly Connected Finite Automata

Stefan Kiefer
Andrew Ryzhikov

Several reachability problems in finite automata, such as completeness of NFAs and synchronisation of total DFAs, correspond to fundamental properties of sets of nonnegative matrices. In particular, the two mentioned properties correspond to matrix mortality and ergodicity, which ask whether there exists a product of the input matrices that is equal to, respectively, the zero matrix and a matrix with a column of strictly positive entries only. The case where the input automaton is strongly connected (that is, the corresponding set of nonnegative matrices is irreducible) frequently appears in applications and often admits better properties than the general case. In this paper, we address the existence of such properties from the computational complexity point of view, and develop a versatile technique to show that several NL-complete problems remain NL-complete in the strongly connected case. In particular, we show that deciding if a binary total DFA is synchronising is NL-complete even if it is promised to be strongly connected, and that deciding completeness of a binary unambiguous NFA with very limited nondeterminism is NL-complete under the same promise.

Details

MFCS Conference 2020 Conference Paper

On Affine Reachability Problems

Stefan Jaax
Stefan Kiefer

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.

Details

MFCS Conference 2019 Conference Paper

Efficient Analysis of Unambiguous Automata Using Matrix Semigroup Techniques

Stefan Kiefer
Cas Widdershoven

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

Details

Highlights Conference 2018 Conference Abstract

Efficient analysis of probabilistic systems that accumulate quantities

Stefan Kiefer

ABSTRACT. Probabilistic systems that accumulate quantities such as energy and/or cost are naturally modelled by Markov chains whose transitions are labelled with vectors of numbers. Computing information on the probability distribution of the total accumulated cost is a fundamental problem in this model. The naive way of solving this problem is to encode the accumulated quantities in the state space of the model, incurring an exponential blowup. One can improve on this approach. I will explain how results on Presburger arithmetic, language theory and graph theory lead to more efficient algorithms and verification tools. Joint work with Christoph Haase and Markus Lohrey.

Details

MFCS Conference 2017 Conference Paper

Counting Problems for Parikh Images

Christoph Haase
Stefan Kiefer
Markus Lohrey

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

Details

SODA Conference 2017 Conference Paper

On Rationality of Nonnegative Matrix Factorization

Dmitry Chistikov 0001
Stefan Kiefer
Ines Marusic
Mahsa Shirmohammadi
James Worrell 0001

Nonnegative matrix factorization ( N MF) 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. NMF has a wide variety of applications, including bioinformatics, chemometrics, communication complexity, machine learning, polyhedral combinatorics, among many others. A longstanding open question, posed by Cohen and Rothblum in 1993, is whether every rational matrix M has an NMF with minimal d whose factors W and H are also rational. We answer this question negatively, by exhibiting a matrix M for which W and H require irrational entries. As an application of this result, we show that state minimization of labeled Markov chains can require the introduction of irrational transition probabilities. We complement these irrationality results with an NP- complete version of NMF for which rational numbers suffice.

Details

Highlights Conference 2016 Conference Abstract

Distinguishing Hidden Markov Chains

Stefan Kiefer
A. Prasad Sistla

Hidden Markov Chains (HMCs) are commonly used mathematical models of probabilistic systems. They are employed in various fields such as speech recognition, signal processing, and biological sequence analysis. Motivated by applications in stochastic runtime verification, we consider the problem of distinguishing two given HMCs based on a single observation sequence that one of the HMCs generates. More precisely, given two HMCs and an observation sequence, a distinguishing algorithm is expected to identify the HMC that generates the observation sequence. Two HMCs are called distinguishable if for every epsilon > 0 there is a distinguishing algorithm whose error probability is less than epsilon. We show that one can decide in polynomial time whether two HMCs are distinguishable. Further, we present and analyze two distinguishing algorithms for distinguishable HMCs. The first algorithm makes a decision after processing a fixed number of observations, and it exhibits two-sided error. The second algorithm processes an unbounded number of observations, but the algorithm has only one-sided error. The error probability, for both algorithms, decays exponentially with the number of processed observations. We also provide an algorithm for distinguishing multiple HMCs. We apply our results to stochastic runtime verification, where a monitor should distinguish correct and faulty behaviour of a stochastic system.

Details

Highlights Conference 2016 Conference Abstract

Minimal probabilistic automata have to make irrational choices

Mahsa Shirmohammadi
Dmitry Chistikov
Stefan Kiefer
Ines Marusic
James Worrell

In this talk, we answer the question of whether, given a probabilistic automaton (PA) with rational transition probabilities, there always exists a minimal equivalent PA that also has rational transition probabilities. The PA and its minimal equivalent PA accept all finite words with equal probabilities. We approach this problem by exhibiting a connection with a longstanding open question concerning nonnegative matrix factorization (NMF). 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. In 1993 Cohen and Rothblum posed the problem of whether a rational matrix M always has an NMF of minimal inner dimension d whose factors W and H are also rational. We answer this question negatively, by exhibiting a matrix for which W and H require irrational entries. As a corollary we obtain a negative answer to the question on rationality of minimal probabilistic automata. This talk is based on the paper titled “On Restricted Nonnegative Matrix Factorization”, that will be presented in ICALP 2016, and the unpublished manuscript titled “Nonnegative Matrix Factorization Requires Irrationality”, that is now online on Arxiv (https: //arxiv. org/abs/1605. 06848v1).

Details

I&C Journal 2014 Journal Article

Language equivalence of probabilistic pushdown automata

Vojtěch Forejt
Petr Jančar
Stefan Kiefer
James Worrell

We study the language equivalence problem for probabilistic pushdown automata (pPDA) and their subclasses. We show that the problem is interreducible with the multiplicity equivalence problem for context-free grammars, the decidability of which has been open for several decades. Interreducibility also holds for pPDA with one control state. In contrast, for the case of a one-letter input alphabet we show that pPDA language equivalence (and hence multiplicity equivalence of context-free grammars) is in PSPACE and at least as hard as the polynomial identity testing problem.

Details DOI

Highlights Conference 2013 Conference Abstract

Bisimilarity of pushdown automata is nonelementary

Michael Benedikt
Stefan Göller
Stefan Kiefer
Andrzej Murawski

Given two pushdown systems, the bisimilarity problem asks whether they are bisimilar. While this problem is known to be decidable our main result states that it is nonelementary, improving EXPTIME-hardness, which was the previously best known lower bound for this problem. Our lower bound result holds for normed pushdown systems as well.

PDF Details

MFCS Conference 2012 Conference Paper

Model Checking Stochastic Branching Processes

Taolue Chen 0001
Klaus Dräger
Stefan Kiefer

Abstract Stochastic branching processes are a classical model for describing random trees, which have applications in numerous fields including biology, physics, and natural language processing. In particular, they have recently been proposed to describe parallel programs with stochastic process creation. In this paper, we consider the problem of model checking stochastic branching process. Given a branching process and a deterministic parity tree automaton, we are interested in computing the probability that the generated random tree is accepted by the automaton. We show that this probability can be compared with any rational number in PSPACE, and with 0 and 1 in polynomial time. In a second part, we suggest a tree extension of the logic PCTL, and develop a PSPACE algorithm for model checking a branching process against a formula of this logic. We also show that the qualitative fragment of this logic can be model checked in polynomial time.

Details

I&C Journal 2012 Journal Article

Space-efficient scheduling of stochastically generated tasks

Tomáš Brázdil
Javier Esparza
Stefan Kiefer
Michael Luttenberger

We study the problem of scheduling tasks for execution by a processor when the tasks can stochastically generate new tasks. Tasks can be of different types, and each type has a fixed, known probability of generating other tasks. We present results on the random variable S σ modeling the maximal space needed by the processor to store the currently active tasks when acting under the scheduler σ. We obtain tail bounds for the distribution of S σ for both offline and online schedulers, and investigate the expected value E [ S σ ].

Details DOI

TCS Journal 2011 Journal Article

Derivation tree analysis for accelerated fixed-point computation

Javier Esparza
Stefan Kiefer
Michael Luttenberger

We show that for several classes of idempotent semirings the least fixed-point of a polynomial system of equations X = f ( X ) is equal to the least fixed-point of a linear system obtained by “linearizing” the polynomials of f in a certain way. Our proofs rely on derivation tree analysis, a proof principle that combines methods from algebra, calculus, and formal language theory, and was first used in Esparza et al. (2007) [10], to show that Newton’s method over commutative and idempotent semirings converges in a linear number of steps. Our results lead to efficient generic algorithms for computing the least fixed-point. We use these algorithms to derive several consequences, including an O ( N 3 ) algorithm for computing the throughput of a context-free grammar (obtained by speeding up the O ( N 4 ) algorithm of Caucal et al. (2007) [7]), and a generalization of Courcelle’s result stating that the downward-closed image of a context-free language is regular (Courcelle, 1991) [8].

Details DOI

STOC Conference 2007 Conference Paper

On the convergence of Newton's method for monotone systems of polynomial equations

Stefan Kiefer
Michael Luttenberger
Javier Esparza

Monotone systems of polynomial equations (MSPEs) are systems of fixed-point equations X 1 = f 1 (X 1 , ..., X n ), ..., X n = f n (X 1 , ..., 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 X = f(X) arises naturally in the analysis of stochastic context-free grammars, recursive Markov chains, and probabilistic pushdown automata. While the Kleene sequence f(0), f(f(0)), ... always converges to the least solution mu.f, if it exists, the number of iterations needed to compute the first i bits of mu.f may grow exponentially in i.Etessami and Yannakakis have recently adapted Newton's iterative method to MSPEs and proved that the Newton sequence converges at least as fast as the Kleene sequence and exponentially faster in many cases.They conjecture that, given an MSPE of size m, the number of Newton iterations needed to obtain i accurate bits of mu.f grows polynomially in i and m. In this paper we show that the number of iterations grows linearly in i for strongly connected MSPEs and may grow exponentially in m for general MSPEs.

Details