Showing 1–50 of 82 results for author: Kiefer, S

Minimising the Probabilistic Bisimilarity Distance

Authors: Stefan Kiefer, Qiyi Tang

Abstract: 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. The model is related to interval Markov chains. Motivated by applications to the verification of probabilistic noninterference in security, we study problems of minimising probabilistic bisimilarity distances of labelled MDPs, in pa… ▽ More 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. The model is related to interval Markov chains. Motivated by applications to the verification of probabilistic noninterference in security, we study problems of minimising probabilistic bisimilarity distances of labelled MDPs, in particular, whether there exist strategies such that the probabilistic bisimilarity distance between the induced labelled Markov chains is less than a given rational number, both for memoryless strategies and general strategies. We show that the distance minimisation problem is ExTh(R)-complete for memoryless strategies and undecidable for general strategies. We also study the computational complexity of the qualitative problem about making the distance less than one. This problem is known to be NP-complete for memoryless strategies. We show that it is EXPTIME-complete for general strategies. △ Less

Submitted 28 June, 2024; originally announced June 2024.

Comments: 36 pages, 7 figures, CONCUR 2024

Verification of Population Protocols with Unordered Data

Authors: Steffen van Bergerem, Roland Guttenberg, Sandra Kiefer, Corto Mascle, Nicolas Waldburger, Chana Weil-Kennedy

Abstract: Population protocols are a well-studied model of distributed computation in which a group of anonymous finite-state agents communicates via pairwise interactions. Together they decide whether their initial configuration, that is, the initial distribution of agents in the states, satisfies a property. As an extension in order to express properties of multisets over an infinite data domain, Blondin… ▽ More Population protocols are a well-studied model of distributed computation in which a group of anonymous finite-state agents communicates via pairwise interactions. Together they decide whether their initial configuration, that is, the initial distribution of agents in the states, satisfies a property. As an extension in order to express properties of multisets over an infinite data domain, Blondin and Ladouceur (ICALP'23) introduced population protocols with unordered data (PPUD). In PPUD, each agent carries a fixed data value, and the interactions between agents depend on whether their data are equal or not. Blondin and Ladouceur also identified the interesting subclass of immediate observation PPUD (IOPPUD), where in every transition one of the two agents remains passive and does not move, and they characterised its expressive power. We study the decidability and complexity of formally verifying these protocols. The main verification problem for population protocols is well-specification, that is, checking whether the given PPUD computes some function. We show that well-specification is undecidable in general. By contrast, for IOPPUD, we exhibit a large yet natural class of problems, which includes well-specification among other classic problems, and establish that these problems are in EXPSPACE. We also provide a lower complexity bound, namely coNEXPTIME-hardness. △ Less

Submitted 1 May, 2024; originally announced May 2024.

Comments: 40 pages, 7 figures, extended version of ICALP 2024 paper

Strategy Complexity of Büchi Objectives in Concurrent Stochastic Games

Authors: Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, Patrick Totzke

Abstract: We study 2-player concurrent stochastic Büchi games on countable graphs. Two players, Max and Min, seek respectively to maximize and minimize the probability of visiting a set of target states infinitely often. We show that there always exist $\varepsilon$-optimal Max strategies that use just a step counter plus 1 bit of public memory. This upper bound holds for all countable graphs, but it is a n… ▽ More We study 2-player concurrent stochastic Büchi games on countable graphs. Two players, Max and Min, seek respectively to maximize and minimize the probability of visiting a set of target states infinitely often. We show that there always exist $\varepsilon$-optimal Max strategies that use just a step counter plus 1 bit of public memory. This upper bound holds for all countable graphs, but it is a new result even for the special case of finite graphs. The upper bound is tight in the sense that Max strategies that use just a step counter, or just finite memory, are not sufficient even on finite game graphs. The upper bound is a consequence of a slightly stronger new result: $\varepsilon$-optimal Max strategies for the combined Büchi and Transience objective require just 1 bit of public memory (but cannot be memoryless). Our proof techniques also yield a closely related result, that $\varepsilon$-optimal Max strategies for the Transience objective alone (which is only meaningful in infinite graphs) can be memoryless. △ Less

Submitted 23 April, 2024; originally announced April 2024.

MSC Class: 91A35; 91A15 ACM Class: G.3

Untangling Gaussian Mixtures

Authors: Eva Fluck, Sandra Kiefer, Christoph Standke

Abstract: Tangles were originally introduced as a concept to formalize regions of high connectivity in graphs. In recent years, they have also been discovered as a link between structural graph theory and data science: when interpreting similarity in data sets as connectivity between points, finding clusters in the data essentially amounts to finding tangles in the underlying graphs. This paper further expl… ▽ More Tangles were originally introduced as a concept to formalize regions of high connectivity in graphs. In recent years, they have also been discovered as a link between structural graph theory and data science: when interpreting similarity in data sets as connectivity between points, finding clusters in the data essentially amounts to finding tangles in the underlying graphs. This paper further explores the potential of tangles in data sets as a means for a formal study of clusters. Real-world data often follow a normal distribution. Accounting for this, we develop a quantitative theory of tangles in data sets drawn from Gaussian mixtures. To this end, we equip the data with a graph structure that models similarity between the points and allows us to apply tangle theory to the data. We provide explicit conditions under which tangles associated with the marginal Gaussian distributions exist asymptotically almost surely. This can be considered as a sufficient formal criterion for the separabability of clusters in the data. △ Less

Submitted 11 March, 2024; originally announced March 2024.

MSC Class: 05C40; 62H30; 68R10

Bounding the Weisfeiler-Leman Dimension via a Depth Analysis of I/R-Trees

Authors: Sandra Kiefer, Daniel Neuen

Abstract: The Weisfeiler-Leman (WL) dimension is an established measure for the inherent descriptive complexity of graphs and relational structures. It corresponds to the number of variables that are needed and sufficient to define the object of interest in a counting version of first-order logic (FO). These bounded-variable counting logics were even candidates to capture graph isomorphism, until a celebrat… ▽ More The Weisfeiler-Leman (WL) dimension is an established measure for the inherent descriptive complexity of graphs and relational structures. It corresponds to the number of variables that are needed and sufficient to define the object of interest in a counting version of first-order logic (FO). These bounded-variable counting logics were even candidates to capture graph isomorphism, until a celebrated construction due to Cai, Fürer, and Immerman [Combinatorica 1992] showed that $Ω(n)$ variables are required to distinguish all non-isomorphic $n$-vertex graphs. Still, very little is known about the precise number of variables required and sufficient to define every $n$-vertex graph. For the bounded-variable (non-counting) FO fragments, Pikhurko, Veith, and Verbitsky [Discret. Appl. Math. 2006] provided an upper bound of $\frac{n+3}{2}$ and showed that it is essentially tight. Our main result yields that, in the presence of counting quantifiers, $\frac{n}{4} + o(n)$ variables suffice. This shows that counting does allow us to save variables when defining graphs. As an application of our techniques, we also show new bounds in terms of the vertex cover number of the graph. To obtain the results, we introduce a new concept called the WL depth of a graph. We use it to analyze branching trees within the Individualization/Refinement (I/R) paradigm from the domain of isomorphism algorithms. We extend the recursive procedure from the I/R paradigm by the possibility of splitting the graphs into independent parts. Then we bound the depth of the obtained branching trees, which translates into bounds on the WL dimension and thereby on the number of variables that suffice to define the graphs. △ Less

Submitted 5 February, 2024; originally announced February 2024.

Comments: 37 pages, 2 figures

Memoryless Strategies in Stochastic Reachability Games

Authors: Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, Patrick Totzke

Abstract: We study concurrent stochastic reachability games played on finite graphs. Two players, Max and Min, seek respectively to maximize and minimize the probability of reaching a set of target states. We prove that Max has a memoryless strategy that is optimal from all states that have an optimal strategy. Our construction provides an alternative proof of this result by Bordais, Bouyer and Le Roux, and… ▽ More We study concurrent stochastic reachability games played on finite graphs. Two players, Max and Min, seek respectively to maximize and minimize the probability of reaching a set of target states. We prove that Max has a memoryless strategy that is optimal from all states that have an optimal strategy. Our construction provides an alternative proof of this result by Bordais, Bouyer and Le Roux, and strengthens it, as we allow Max's action sets to be countably infinite. △ Less

Submitted 24 January, 2024; originally announced January 2024.

Simulating Logspace-Recursion with Logarithmic Quantifier Depth

Authors: Steffen van Bergerem, Martin Grohe, Sandra Kiefer, Luca Oeljeklaus

Abstract: The fixed-point logic LREC= was developed by Grohe et al. (CSL 2011) in the quest for a logic to capture all problems decidable in logarithmic space. It extends FO+C, first-order logic with counting, by an operator that formalises a limited form of recursion. We show that for every LREC=-definable property on relational structures, there is a constant k such that the k-variable fragment of first-o… ▽ More The fixed-point logic LREC= was developed by Grohe et al. (CSL 2011) in the quest for a logic to capture all problems decidable in logarithmic space. It extends FO+C, first-order logic with counting, by an operator that formalises a limited form of recursion. We show that for every LREC=-definable property on relational structures, there is a constant k such that the k-variable fragment of first-order logic with counting quantifiers expresses the property via formulae of logarithmic quantifier depth. This yields that any pair of graphs separable by the property can be distinguished with the k-dimensional Weisfeiler-Leman algorithm in a logarithmic number of iterations. In particular, it implies that a constant dimension of the algorithm identifies every interval graph and every chordal claw-free graph in logarithmically many iterations, since every such graph admits LREC=-definable canonisation. △ Less

Submitted 25 April, 2023; originally announced April 2023.

Refutations of pebble minimization via output languages

Authors: Sandra Kiefer, Lê Thành Dũng Nguyên, Cécilia Pradic

Abstract: Polyregular functions are the class of string-to-string functions definable by pebble transducers, an extension of finite-state automata with outputs and multiple two-way reading heads (pebbles) with a stack discipline. If a polyregular function can be computed with $k$ pebbles, then its output length is bounded by a polynomial of degree $k$ in the input length. But Bojańczyk has shown that the co… ▽ More Polyregular functions are the class of string-to-string functions definable by pebble transducers, an extension of finite-state automata with outputs and multiple two-way reading heads (pebbles) with a stack discipline. If a polyregular function can be computed with $k$ pebbles, then its output length is bounded by a polynomial of degree $k$ in the input length. But Bojańczyk has shown that the converse fails. In this paper, we provide two alternative easier proofs. The first establishes by elementary means that some quadratic polyregular function requires 3 pebbles. The second proof - just as short, albeit less elementary - shows a stronger statement: for every $k$, there exists some polyregular function with quadratic growth whose output language differs from that of any $k$-fold composition of macro tree transducers (and which therefore cannot be computed by a $k$-pebble transducer). Along the way, we also refute a conjectured logical characterization of polyblind functions. △ Less

Submitted 20 June, 2023; v1 submitted 22 January, 2023; originally announced January 2023.

Comments: 20 pages, for submission to Fundamenta Informaticae; this version excludes some of the material in the v1, which may appear in other subsequent papers

Semantic Interactive Learning for Text Classification: A Constructive Approach for Contextual Interactions

Authors: Sebastian Kiefer, Mareike Hoffmann

Abstract: Interactive Machine Learning (IML) shall enable intelligent systems to interactively learn from their end-users, and is quickly becoming more and more important. Although it puts the human in the loop, interactions are mostly performed via mutual explanations that miss contextual information. Furthermore, current model-agnostic IML strategies like CAIPI are limited to 'destructive' feedback, meani… ▽ More Interactive Machine Learning (IML) shall enable intelligent systems to interactively learn from their end-users, and is quickly becoming more and more important. Although it puts the human in the loop, interactions are mostly performed via mutual explanations that miss contextual information. Furthermore, current model-agnostic IML strategies like CAIPI are limited to 'destructive' feedback, meaning they solely allow an expert to prevent a learner from using irrelevant features. In this work, we propose a novel interaction framework called Semantic Interactive Learning for the text domain. We frame the problem of incorporating constructive and contextual feedback into the learner as a task to find an architecture that (a) enables more semantic alignment between humans and machines and (b) at the same time helps to maintain statistical characteristics of the input domain when generating user-defined counterexamples based on meaningful corrections. Therefore, we introduce a technique called SemanticPush that is effective for translating conceptual corrections of humans to non-extrapolating training examples such that the learner's reasoning is pushed towards the desired behavior. In several experiments, we show that our method clearly outperforms CAIPI, a state of the art IML strategy, in terms of Predictive Performance as well as Local Explanation Quality in downstream multi-class classification tasks. △ Less

Submitted 7 September, 2022; originally announced September 2022.

On the Sequential Probability Ratio Test in Hidden Markov Models

Authors: Oscar Darwin, Stefan Kiefer

Abstract: 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 c… ▽ More 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. △ Less

Submitted 5 February, 2023; v1 submitted 28 July, 2022; originally announced July 2022.

Comments: 28 pages, 10 figures, submitted to CONCUR 2022

ACM Class: F.0; G.3

A Study of Weisfeiler-Leman Colorings on Planar Graphs

Authors: Sandra Kiefer, Daniel Neuen

Abstract: The Weisfeiler-Leman (WL) algorithm is a combinatorial procedure that computes colorings on graphs, which can often be used to detect their (non-)isomorphism. Particularly the 1- and 2-dimensional versions 1-WL and 2-WL have received much attention, due to their numerous links to other areas of computer science. Knowing the expressive power of a certain dimension of the algorithm usually amounts… ▽ More The Weisfeiler-Leman (WL) algorithm is a combinatorial procedure that computes colorings on graphs, which can often be used to detect their (non-)isomorphism. Particularly the 1- and 2-dimensional versions 1-WL and 2-WL have received much attention, due to their numerous links to other areas of computer science. Knowing the expressive power of a certain dimension of the algorithm usually amounts to understanding the computed colorings. An increase in the dimension leads to finer computed colorings and, thus, more graphs can be distinguished. For example, on the class of planar graphs, 3-WL solves the isomorphism problem. However, the expressive power of 2-WL on the class is poorly understood (and, in particular, it may even well be that it decides isomorphism). In this paper, we investigate the colorings computed by 2-WL on planar graphs. Towards this end, we analyze the graphs induced by edge color classes in the graph. Based on the obtained classification, we show that for every 3-connected planar graph, it holds that: a) after coloring all pairs with their 2-WL color, the graph has fixing number 1 with respect to 1-WL, or b) there is a 2-WL-definable matching that can be used to transform the graph into a smaller one, or c) 2-WL detects a connected subgraph that is essentially the graph of a Platonic or Archimedean solid, a prism, a cycle, or a bipartite graph K_{2,\ell}. In particular, the graphs from case (a) are identified by 2-WL. △ Less

Submitted 21 June, 2022; originally announced June 2022.

Comments: 53 pages, 15 figures, full version of a paper accepted at ICALP 2022

SpeqNets: Sparsity-aware Permutation-equivariant Graph Networks

Authors: Christopher Morris, Gaurav Rattan, Sandra Kiefer, Siamak Ravanbakhsh

Abstract: While (message-passing) graph neural networks have clear limitations in approximating permutation-equivariant functions over graphs or general relational data, more expressive, higher-order graph neural networks do not scale to large graphs. They either operate on $k$-order tensors or consider all $k$-node subgraphs, implying an exponential dependence on $k$ in memory requirements, and do not adap… ▽ More While (message-passing) graph neural networks have clear limitations in approximating permutation-equivariant functions over graphs or general relational data, more expressive, higher-order graph neural networks do not scale to large graphs. They either operate on $k$-order tensors or consider all $k$-node subgraphs, implying an exponential dependence on $k$ in memory requirements, and do not adapt to the sparsity of the graph. By introducing new heuristics for the graph isomorphism problem, we devise a class of universal, permutation-equivariant graph networks, which, unlike previous architectures, offer a fine-grained control between expressivity and scalability and adapt to the sparsity of the graph. These architectures lead to vastly reduced computation times compared to standard higher-order graph networks in the supervised node- and graph-level classification and regression regime while significantly improving over standard graph neural network and graph kernel architectures in terms of predictive performance. △ Less

Submitted 30 August, 2022; v1 submitted 25 March, 2022; originally announced March 2022.

Comments: ICML 2022, fixed typo in Observation 1

Strategy Complexity of Reachability in Countable Stochastic 2-Player Games

Authors: Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, Patrick Totzke

Abstract: We study countably infinite stochastic 2-player games with reachability objectives. Our results provide a complete picture of the memory requirements of $\varepsilon$-optimal (resp. optimal) strategies. These results depend on the size of the players' action sets and on whether one requires strategies that are uniform (i.e., independent of the start state). Our main result is that $\varepsilon$-… ▽ More We study countably infinite stochastic 2-player games with reachability objectives. Our results provide a complete picture of the memory requirements of $\varepsilon$-optimal (resp. optimal) strategies. These results depend on the size of the players' action sets and on whether one requires strategies that are uniform (i.e., independent of the start state). Our main result is that $\varepsilon$-optimal (resp. optimal) Maximizer strategies require infinite memory if Minimizer is allowed infinite action sets. This lower bound holds even under very strong restrictions. Even in the special case of infinitely branching turn-based reachability games, even if all states allow an almost surely winning Maximizer strategy, strategies with a step counter plus finite private memory are still useless. Regarding uniformity, we show that for Maximizer there need not exist positional (i.e., memoryless) uniformly $\varepsilon$-optimal strategies even in the special case of finite action sets or in finitely branching turn-based games. On the other hand, in games with finite action sets, there always exists a uniformly $\varepsilon$-optimal Maximizer strategy that uses just one bit of public memory. △ Less

Submitted 2 July, 2024; v1 submitted 22 March, 2022; originally announced March 2022.

MSC Class: 91A35; 91A15 ACM Class: G.3

Treelike decompositions for transductions of sparse graphs

Authors: Jan Dreier, Jakub Gajarský, Sandra Kiefer, Michał Pilipczuk, Szymon Toruńczyk

Abstract: We give new decomposition theorems for classes of graphs that can be transduced in first-order logic from classes of sparse graphs -- more precisely, from classes of bounded expansion and from nowhere dense classes. In both cases, the decomposition takes the form of a single colored rooted tree of bounded depth where, in addition, there can be links between nodes that are not related in the tree.… ▽ More We give new decomposition theorems for classes of graphs that can be transduced in first-order logic from classes of sparse graphs -- more precisely, from classes of bounded expansion and from nowhere dense classes. In both cases, the decomposition takes the form of a single colored rooted tree of bounded depth where, in addition, there can be links between nodes that are not related in the tree. The constraint is that the structure formed by the tree and the links has to be sparse. Using the decomposition theorem for transductions of nowhere dense classes, we show that they admit low-shrubdepth covers of size $O(n^\varepsilon)$, where $n$ is the vertex count and $\varepsilon>0$ is any fixed~real. This solves an open problem posed by Gajarský et al. (ACM TOCL '20) and also by Briański et al. (SIDMA '21). △ Less

Submitted 26 January, 2022; originally announced January 2022.

Comments: 39 pages, 2 figures

Approximate Bisimulation Minimisation

Authors: Stefan Kiefer, Qiyi Tang

Abstract: 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 lum** together states that are exactly bisimilar in a slightly perturbed system. We present experiments that show that… ▽ More 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 lum** 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. △ Less

Submitted 1 October, 2021; originally announced October 2021.

Comments: Full version of an FSTTCS'21 paper

Lower Bounds for Unambiguous Automata via Communication Complexity

Authors: Mika Göös, Stefan Kiefer, Weiqiang Yuan

Abstract: We use results from communication complexity, both new and old ones, to prove lower bounds for unambiguous finite automata (UFAs). We show three results. $\textit{Complement:}$ There is a language $L$ recognised by an $n$-state UFA such that the complement language $\overline{L}$ requires NFAs with $n^{\tildeΩ(\log n)}$ states. This improves on a lower bound by Raskin. $\textit{Union:}$ There… ▽ More We use results from communication complexity, both new and old ones, to prove lower bounds for unambiguous finite automata (UFAs). We show three results. $\textit{Complement:}$ There is a language $L$ recognised by an $n$-state UFA such that the complement language $\overline{L}$ requires NFAs with $n^{\tildeΩ(\log n)}$ states. This improves on a lower bound by Raskin. $\textit{Union:}$ There are languages $L_1$, $L_2$ recognised by $n$-state UFAs such that the union $L_1\cup L_2$ requires UFAs with $n^{\tildeΩ(\log n)}$ states. $\textit{Separation:}$ There is a language $L$ such that both $L$ and $\overline{L}$ are recognised by $n$-state NFAs but such that $L$ requires UFAs with $n^{Ω(\log n)}$ states. This refutes a conjecture by Colcombet. △ Less

Submitted 12 February, 2022; v1 submitted 19 September, 2021; originally announced September 2021.

Image-Binary Automata

Authors: Stefan Kiefer, Cas Widdershoven

Abstract: We introduce a certain restriction of weighted automata over the rationals, called image-binary automata. We show that such automata accept the regular languages, can be exponentially more succinct than corresponding NFAs, and allow for polynomial complementation, union, and intersection. This compares favourably with unambiguous automata whose complementation requires a superpolynomial state blow… ▽ More We introduce a certain restriction of weighted automata over the rationals, called image-binary automata. We show that such automata accept the regular languages, can be exponentially more succinct than corresponding NFAs, and allow for polynomial complementation, union, and intersection. This compares favourably with unambiguous automata whose complementation requires a superpolynomial state blowup. We also study an infinite-word version, image-binary Büchi automata. We show that such automata are amenable to probabilistic model checking, similarly to unambiguous Büchi automata. We provide algorithms to translate $k$-ambiguous Büchi automata to image-binary Büchi automata, leading to model-checking algorithms with optimal computational complexity. △ Less

Submitted 28 March, 2022; v1 submitted 2 September, 2021; originally announced September 2021.

Comments: Journal version of paper published at DCFS'21

Linear-Time Model Checking Branching Processes

Authors: Stefan Kiefer, Pavel Semukhin, Cas Widdershoven

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:… ▽ More (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. △ Less

Submitted 4 July, 2021; originally announced July 2021.

Comments: full version of a CONCUR'21 paper

Logarithmic Weisfeiler-Leman Identifies All Planar Graphs

Authors: Martin Grohe, Sandra Kiefer

Abstract: The Weisfeiler-Leman (WL) algorithm is a well-known combinatorial procedure for detecting symmetries in graphs and it is widely used in graph-isomorphism tests. It proceeds by iteratively refining a colouring of vertex tuples. The number of iterations needed to obtain the final output is crucial for the parallelisability of the algorithm. We show that there is a constant k such that every planar… ▽ More The Weisfeiler-Leman (WL) algorithm is a well-known combinatorial procedure for detecting symmetries in graphs and it is widely used in graph-isomorphism tests. It proceeds by iteratively refining a colouring of vertex tuples. The number of iterations needed to obtain the final output is crucial for the parallelisability of the algorithm. We show that there is a constant k such that every planar graph can be identified (that is, distinguished from every non-isomorphic graph) by the k-dimensional WL algorithm within a logarithmic number of iterations. This generalises a result due to Verbitsky (STACS 2007), who proved the same for 3-connected planar graphs. The number of iterations needed by the k-dimensional WL algorithm to identify a graph corresponds to the quantifier depth of a sentence that defines the graph in the (k+1)-variable fragment C^{k+1} of first-order logic with counting quantifiers. Thus, our result implies that every planar graph is definable with a C^{k+1}-sentence of logarithmic quantifier depth. △ Less

Submitted 30 June, 2021; originally announced June 2021.

Comments: 21 pages, 2 figures, accepted at ICALP 2021

On Complementing Unambiguous Automata and Graphs With Many Cliques and Cocliques

Authors: Emil Indzhev, Stefan Kiefer

Abstract: We show that for any unambiguous finite automaton with $n$ states there exists an unambiguous finite automaton with $\sqrt{n+1} \cdot 2^{n/2}$ states that recognizes the complement language. This builds and improves upon a similar result by Jirásek et al. [Int. J. Found. Comput. Sci. 29 (5) (2018)]. Our improvement is based on a reduction to and an analysis of a problem from extremal graph theory:… ▽ More We show that for any unambiguous finite automaton with $n$ states there exists an unambiguous finite automaton with $\sqrt{n+1} \cdot 2^{n/2}$ states that recognizes the complement language. This builds and improves upon a similar result by Jirásek et al. [Int. J. Found. Comput. Sci. 29 (5) (2018)]. Our improvement is based on a reduction to and an analysis of a problem from extremal graph theory: we show that for any graph with $n$ vertices, the product of the number of its cliques with the number of its cocliques (independent sets) is bounded by $(n+1) 2^n$. △ Less

Submitted 15 March, 2022; v1 submitted 16 May, 2021; originally announced May 2021.

Comments: version implementing referees' suggestions

Responsibility and verification: Importance value in temporal logics

Authors: Corto Mascle, Christel Baier, Florian Funke, Simon Jantsch, Stefan Kiefer

Abstract: 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 values to verification as a means to evaluate how important a part of a system is. The importance of a component is measured by giving its control to an adversary, alone or along with other components, and testing wheth… ▽ More 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 values to verification as a means to evaluate how important a part of a system is. The importance of a component is measured by giving its control to an adversary, alone or along with other components, and testing whether the system can still fulfill the specification. We study this idea in the framework of model-checking with various classical types of linear-time specification, and propose several ways to transpose it to branching ones. We also provide tight complexity bounds in almost every case. △ Less

Submitted 20 April, 2021; v1 submitted 12 February, 2021; originally announced February 2021.

Comments: 23 pages, 11 figures, full version of a conference paper accepted at LICS'21

Transience in Countable MDPs

Authors: Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, Patrick Totzke

Abstract: The Transience objective is not to visit any state infinitely often. While this is not possible in 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 T… ▽ More The Transience objective is not to visit any state infinitely often. While this is not possible in 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. △ Less

Submitted 4 July, 2021; v1 submitted 26 December, 2020; originally announced December 2020.

Online Monitoring $ω$-Regular Properties in Unknown Markov Chains

Authors: Javier Esparza, Stefan Kiefer, Jan Kretinsky, Maximilian Weininger

Abstract: We study runtime monitoring of $ω$-regular properties. We consider a simple setting in which a run of an unknown finite-state Markov chain $\mathcal M$ is monitored against a fixed but arbitrary $ω$-regular specification $\varphi$. The purpose of monitoring is to keep aborting runs that are "unlikely" to satisfy the specification until $\mathcal M$ executes a correct run. We design controllers for… ▽ More We study runtime monitoring of $ω$-regular properties. We consider a simple setting in which a run of an unknown finite-state Markov chain $\mathcal M$ is monitored against a fixed but arbitrary $ω$-regular specification $\varphi$. The purpose of monitoring is to keep aborting runs that are "unlikely" to satisfy the specification until $\mathcal M$ executes a correct run. We design controllers for the reset action that (assuming that $\varphi$ has positive probability) satisfy the following property w.p.1: the number of resets is finite, and the run executed by $\mathcal M$ after the last reset satisfies $\varphi$. △ Less

Submitted 16 October, 2020; originally announced October 2020.

Equivalence of Hidden Markov Models with Continuous Observations

Authors: Oscar Darwin, Stefan Kiefer

Abstract: 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 fro… ▽ More 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. △ Less

Submitted 27 September, 2020; originally announced September 2020.

Comments: 17 pages, 9 figures, Submitted to FSTTCS 2020

ACM Class: F.0; G.3

Comparing Labelled Markov Decision Processes

Authors: Stefan Kiefer, Qiyi Tang

Abstract: 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 s… ▽ More 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. △ Less

Submitted 24 September, 2020; originally announced September 2020.

Comments: 35 pages, 7 figures

Notes on Equivalence and Minimization of Weighted Automata

Authors: Stefan Kiefer

Abstract: This set of notes re-proves known results on weighted automata (over a field, also known as multiplicity automata). The text offers a unified view on theorems and proofs that have appeared in the literature over decades and were written in different styles and contexts. None of the results reported here are claimed to be new. The content centres around fundamentals of equivalence and minimization,… ▽ More This set of notes re-proves known results on weighted automata (over a field, also known as multiplicity automata). The text offers a unified view on theorems and proofs that have appeared in the literature over decades and were written in different styles and contexts. None of the results reported here are claimed to be new. The content centres around fundamentals of equivalence and minimization, with an emphasis on algorithmic aspects. The presentation is minimalistic. No attempt has been made to motivate the material. Weighted automata are viewed from a linear-algebra angle. As a consequence, the proofs, which are meant to be succinct, but complete and almost self-contained, rely mainly on elementary linear algebra. △ Less

Submitted 2 September, 2020; originally announced September 2020.

Convolutional neural network based deep-learning architecture for intraprostatic tumour contouring on PSMA PET images in patients with primary prostate cancer

Authors: Dejan Kostyszyn, Tobias Fechter, Nico Bartl, Anca L. Grosu, Christian Gratzke, August Sigle, Michael Mix, Juri Ruf, Thomas F. Fassbender, Selina Kiefer, Alisa S. Bettermann, Nils H. Nicolay, Simon Spohn, Maria U. Kramer, Peter Bronsert, Hongqian Guo, Xuefeng Qiu, Feng Wang, Christoph Henkenberens, Rudolf A. Werner, Dimos Baltas, Philipp T. Meyer, Thorsten Derlin, Mengxia Chen, Constantinos Zamboglou

Abstract: Accurate delineation of the intraprostatic gross tumour volume (GTV) is a prerequisite for treatment approaches in patients with primary prostate cancer (PCa). Prostate-specific membrane antigen positron emission tomography (PSMA-PET) may outperform MRI in GTV detection. However, visual GTV delineation underlies interobserver heterogeneity and is time consuming. The aim of this study was to develo… ▽ More Accurate delineation of the intraprostatic gross tumour volume (GTV) is a prerequisite for treatment approaches in patients with primary prostate cancer (PCa). Prostate-specific membrane antigen positron emission tomography (PSMA-PET) may outperform MRI in GTV detection. However, visual GTV delineation underlies interobserver heterogeneity and is time consuming. The aim of this study was to develop a convolutional neural network (CNN) for automated segmentation of intraprostatic tumour (GTV-CNN) in PSMA-PET. Methods: The CNN (3D U-Net) was trained on [68Ga]PSMA-PET images of 152 patients from two different institutions and the training labels were generated manually using a validated technique. The CNN was tested on two independent internal (cohort 1: [68Ga]PSMA-PET, n=18 and cohort 2: [18F]PSMA-PET, n=19) and one external (cohort 3: [68Ga]PSMA-PET, n=20) test-datasets. Accordance between manual contours and GTV-CNN was assessed with Dice-Sørensen coefficient (DSC). Sensitivity and specificity were calculated for the two internal test-datasets by using whole-mount histology. Results: Median DSCs for cohorts 1-3 were 0.84 (range: 0.32-0.95), 0.81 (range: 0.28-0.93) and 0.83 (range: 0.32-0.93), respectively. Sensitivities and specificities for GTV-CNN were comparable with manual expert contours: 0.98 and 0.76 (cohort 1) and 1 and 0.57 (cohort 2), respectively. Computation time was around 6 seconds for a standard dataset. Conclusion: The application of a CNN for automated contouring of intraprostatic GTV in [68Ga]PSMA- and [18F]PSMA-PET images resulted in a high concordance with expert contours and in high sensitivities and specificities in comparison with histology reference. This robust, accurate and fast technique may be implemented for treatment concepts in primary PCa. The trained model and the study's source code are available in an open source repository. △ Less

Submitted 7 August, 2020; originally announced August 2020.

The Big-O Problem

Authors: Dmitry Chistikov, Stefan Kiefer, Andrzej S. Murawski, David Purser

Abstract: 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 bi… ▽ More 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^*\dots w_m^*$ for some finite words $w_1,\dots,w_m$) or when the automaton has finite ambiguity. 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 $\varepsilon$-differential privacy, for which the optimal constant of the big-O notation is exactly $\exp(\varepsilon)$. △ Less

Submitted 14 March, 2022; v1 submitted 15 July, 2020; originally announced July 2020.

Comments: Extended version of the CONCUR 2020 paper "The Big-O Problem for Labelled Markov Chains and Weighted Automata": https://doi.org/10.4230/LIPIcs.CONCUR.2020.41

Journal ref: Logical Methods in Computer Science, Volume 18, Issue 1 (March 15, 2022) lmcs:7343

Strategy Complexity of Parity Objectives in Countable MDPs

Authors: Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, Patrick Totzke

Abstract: 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 $\varepsilon$-optimal strategies (and optimal strategies, where they exist) for all subclasses of parity objectives in the Mostowski hierarchy. Either MD-strategies, Markov st… ▽ More 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 $\varepsilon$-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 $\varepsilon$-optimal or optimal strategies. In particular, 1-bit Markov strategies are necessary and sufficient for $\varepsilon$-optimal (resp. optimal) strategies for general parity objectives. △ Less

Submitted 7 July, 2020; originally announced July 2020.

Comments: This is the full version of a paper presented at CONCUR 2020

The Iteration Number of Colour Refinement

Authors: Sandra Kiefer, Brendan D. McKay

Abstract: The Colour Refinement procedure and its generalisation to higher dimensions, the Weisfeiler-Leman algorithm, are central subroutines in approaches to the graph isomorphism problem. In an iterative fashion, Colour Refinement computes a colouring of the vertices of its input graph. A trivial upper bound on the iteration number of Colour Refinement on graphs of order n is n-1. We show that this bou… ▽ More The Colour Refinement procedure and its generalisation to higher dimensions, the Weisfeiler-Leman algorithm, are central subroutines in approaches to the graph isomorphism problem. In an iterative fashion, Colour Refinement computes a colouring of the vertices of its input graph. A trivial upper bound on the iteration number of Colour Refinement on graphs of order n is n-1. We show that this bound is tight. More precisely, we prove via explicit constructions that there are infinitely many graphs G on which Colour Refinement takes |G|-1 iterations to stabilise. Modifying the infinite families that we present, we show that for every natural number n >= 10, there are graphs on n vertices on which Colour Refinement requires at least n-2 iterations to reach stabilisation. △ Less

Submitted 20 May, 2020; originally announced May 2020.

Comments: 22 pages, 3 figures, full version of a paper accepted at ICALP 2020

On the Size of Finite Rational Matrix Semigroups

Authors: Georgina Bumpus, Christoph Haase, Stefan Kiefer, Paul-Ioan Stoienescu, Jonathan Tanner

Abstract: Let $n$ be a positive integer and $\mathcal M$ a set of rational $n \times n$-matrices such that $\mathcal M$ generates a finite multiplicative semigroup. We show that any matrix in the semigroup is a product of matrices in $\mathcal M$ whose length is at most $2^{n (2 n + 3)} g(n)^{n+1} \in 2^{O(n^2 \log n)}$, where $g(n)$ is the maximum order of finite groups over rational $n \times n$-matrices.… ▽ More Let $n$ be a positive integer and $\mathcal M$ a set of rational $n \times n$-matrices such that $\mathcal M$ generates a finite multiplicative semigroup. We show that any matrix in the semigroup is a product of matrices in $\mathcal M$ whose length is at most $2^{n (2 n + 3)} g(n)^{n+1} \in 2^{O(n^2 \log n)}$, where $g(n)$ is the maximum order of finite groups over rational $n \times 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. △ Less

Submitted 24 April, 2020; v1 submitted 9 September, 2019; originally announced September 2019.

ACM Class: G.2.0; F.4.3

The Power of the Weisfeiler-Leman Algorithm to Decompose Graphs

Authors: Sandra Kiefer, Daniel Neuen

Abstract: The Weisfeiler-Leman procedure is a widely-used technique for graph isomorphism testing that works by iteratively computing an isomorphism-invariant coloring of vertex tuples. Meanwhile, a fundamental tool in structural graph theory, which is often exploited in approaches to tackle the graph isomorphism problem, is the decomposition into 2- and 3-connected components. We prove that the 2-dimensi… ▽ More The Weisfeiler-Leman procedure is a widely-used technique for graph isomorphism testing that works by iteratively computing an isomorphism-invariant coloring of vertex tuples. Meanwhile, a fundamental tool in structural graph theory, which is often exploited in approaches to tackle the graph isomorphism problem, is the decomposition into 2- and 3-connected components. We prove that the 2-dimensional Weisfeiler-Leman algorithm implicitly computes the decomposition of a graph into its 3-connected components. This implies that the dimension of the algorithm needed to distinguish two given non-isomorphic graphs is at most the dimension required to distinguish non-isomorphic 3-connected components of the graphs (assuming dimension at least 2). To obtain our decomposition result, we show that, for k >= 2, the k-dimensional algorithm distinguishes k-separators, i.e., k-tuples of vertices that separate the graph, from other vertex k-tuples. As a byproduct, we also obtain insights about the connectivity of constituent graphs of association schemes. In an application of the results, we show the new upper bound of k on the Weisfeiler-Leman dimension of the class of graphs of treewidth at most k. Using a construction by Cai, Fürer, and Immerman, we also provide a new lower bound that is asymptotically tight up to a factor of 2. △ Less

Submitted 22 September, 2021; v1 submitted 14 August, 2019; originally announced August 2019.

Comments: 48 pages, 6 figures, full version of a paper accepted at MFCS 2019. Added Definition 5.4 and Theorem 5.6 to formalise the notions and arguments. New appendix contains extended proofs for Theorems 5.6 and 5.7. Results remain unchanged

Journal ref: SIAM J. Discret. Math. 36(1): 252-298 (2022)

Efficient Analysis of Unambiguous Automata Using Matrix Semigroup Techniques

Authors: Stefan Kiefer, Cas Widdershoven

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 analy… ▽ More 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|$. △ Less

Submitted 24 June, 2019; originally announced June 2019.

Comments: Technical report for an MFCS'19 paper

String-to-String Interpretations with Polynomial-Size Output

Authors: Mikołaj Bojańczyk, Sandra Kiefer, Nathan Lhote

Abstract: String-to-string MSO interpretations are like Courcelle's MSO transductions, except that a single output position can be represented using a tuple of input positions instead of just a single input position. In particular, the output length is polynomial in the input length, as opposed to MSO transductions, which have output of linear length. We show that string-to-string MSO interpretations are ex… ▽ More String-to-string MSO interpretations are like Courcelle's MSO transductions, except that a single output position can be represented using a tuple of input positions instead of just a single input position. In particular, the output length is polynomial in the input length, as opposed to MSO transductions, which have output of linear length. We show that string-to-string MSO interpretations are exactly the polyregular functions. The latter class has various characterizations, one of which is that it consists of the string-to-string functions recognized by pebble transducers. Our main result implies the surprising fact that string-to-string MSO interpretations are closed under composition. △ Less

Submitted 30 May, 2019; originally announced May 2019.

Comments: 35 pages, full version of a paper accepted for the 46th International Colloquium on Automata, Languages and Programming (ICALP 2019)

On Affine Reachability Problems

Authors: Stefan Jaax, Stefan Kiefer

Abstract: 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-dime… ▽ More 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. △ Less

Submitted 2 July, 2020; v1 submitted 13 May, 2019; originally announced May 2019.

MSC Class: 20H25 ACM Class: F.1.3

Büchi Objectives in Countable MDPs

Authors: Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, Patrick Totzke

Abstract: We study countably infinite Markov decision processes with Büchi objectives, which ask to visit a given subset of states infinitely often. A question left open by T.P. Hill in 1979 is whether there always exist $\varepsilon$-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 b… ▽ More We study countably infinite Markov decision processes with Büchi objectives, which ask to visit a given subset of states infinitely often. A question left open by T.P. Hill in 1979 is whether there always exist $\varepsilon$-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. △ Less

Submitted 30 April, 2019; v1 submitted 25 April, 2019; originally announced April 2019.

Comments: full version of an ICALP'19 paper. This update only fixes some typesetting issues

A Linear Upper Bound on the Weisfeiler-Leman Dimension of Graphs of Bounded Genus

Authors: Martin Grohe, Sandra Kiefer

Abstract: The Weisfeiler-Leman (WL) dimension of a graph is a measure for the inherent descriptive complexity of the graph. While originally derived from a combinatorial graph isomorphism test called the Weisfeiler-Leman algorithm, the WL dimension can also be characterised in terms of the number of variables that is required to describe the graph up to isomorphism in first-order logic with counting quantif… ▽ More The Weisfeiler-Leman (WL) dimension of a graph is a measure for the inherent descriptive complexity of the graph. While originally derived from a combinatorial graph isomorphism test called the Weisfeiler-Leman algorithm, the WL dimension can also be characterised in terms of the number of variables that is required to describe the graph up to isomorphism in first-order logic with counting quantifiers. It is known that the WL dimension is upper-bounded for all graphs that exclude some fixed graph as a minor (Grohe, JACM 2012). However, the bounds that can be derived from this general result are astronomic. Only recently, it was proved that the WL dimension of planar graphs is at most 3 (Kiefer, Ponomarenko, and Schweitzer, LICS 2017). In this paper, we prove that the WL dimension of graphs embeddable in a surface of Euler genus $g$ is at most $4g+3$. For the WL dimension of graphs embeddable in an orientable surface of Euler genus $g$, our approach yields an upper bound of $2g+3$. △ Less

Submitted 15 April, 2019; originally announced April 2019.

Comments: 47 pages, 5 figures

On Nonnegative Integer Matrices and Short Killing Words

Authors: Stefan Kiefer, Corto Mascle

Abstract: Let $n$ be a natural number and $\mathcal{M}$ a set of $n \times n$-matrices over the nonnegative integers such that the joint spectral radius of $\mathcal{M}$ is at most one. We show that if the zero matrix $0$ is a product of matrices in $\mathcal{M}$, then there are $M_1, \ldots, M_{n^5} \in \mathcal{M}$ with $M_1 \cdots M_{n^5} = 0$. This result has applications in automata theory and the theo… ▽ More Let $n$ be a natural number and $\mathcal{M}$ a set of $n \times n$-matrices over the nonnegative integers such that the joint spectral radius of $\mathcal{M}$ is at most one. We show that if the zero matrix $0$ is a product of matrices in $\mathcal{M}$, then there are $M_1, \ldots, M_{n^5} \in \mathcal{M}$ with $M_1 \cdots M_{n^5} = 0$. This result has applications in automata theory and the theory of codes. Specifically, if $X \subset Σ^*$ is a finite incomplete code, then there exists a word $w \in Σ^*$ 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. △ Less

Submitted 26 February, 2021; v1 submitted 2 August, 2018; originally announced August 2018.

Comments: This version has been accepted by the SIAM Journal on Discrete Mathematics (SIDMA). The article extends the STACS'19 paper as follows. (1) The main result has been generalized to monoids generated by finite sets whose joint spectral radius is at most 1. (2) The use of Carpi's theorem is avoided. (3) A more precise result is offered on Restivo's conjecture for finite codes

On the Complexity of Value Iteration

Authors: Nikhil Balaji, Stefan Kiefer, Petr Novotný, Guillermo A. Pérez, Mahsa Shirmohammadi

Abstract: 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.… ▽ More 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 EXP-complete, thus resolving an open problem that goes back to the seminal 1987 paper on the complexity of MDPs by Papadimitriou and Tsitsiklis. As a step** stone, we show that it is EXP-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. △ Less

Submitted 27 April, 2019; v1 submitted 13 July, 2018; originally announced July 2018.

Comments: Full version of an ICALP'19 paper

Selective Monitoring

Authors: Radu Grigore, Stefan Kiefer

Abstract: 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… ▽ More 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. △ Less

Submitted 2 July, 2018; v1 submitted 15 June, 2018; originally announced June 2018.

Comments: CONCUR 2018

On Computing the Total Variation Distance of Hidden Markov Models

Authors: Stefan Kiefer

Abstract: 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 thresho… ▽ More 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. △ Less

Submitted 17 April, 2018; originally announced April 2018.

Comments: Technical report for an ICALP'18 paper

Game Characterization of Probabilistic Bisimilarity, and Applications to Pushdown Automata

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

Abstract: 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). We first show a general characterization of probabilistic bisimilarity in terms of two-player games, which naturally reduces checki… ▽ More 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). We first show a general characterization of probabilistic bisimilarity in terms of two-player games, which naturally reduces checking bisimilarity of probabilistic labelled transition systems to checking bisimilarity of standard (non-deterministic) labelled transition systems. This reduction can be easily implemented in the framework of pPDA, allowing to use known results for standard (non-probabilistic) PDA and their subclasses. A direct use of the reduction incurs an exponential increase of complexity, which does not matter in deriving decidability of bisimilarity for pPDA due to the non-elementary complexity of the problem. In the cases of probabilistic one-counter automata (pOCA), of probabilistic visibly pushdown automata (pvPDA), and of probabilistic basic process algebras (i.e., single-state pPDA) we show that an implicit use of the reduction can avoid the complexity increase; we thus get PSPACE, EXPTIME, and 2-EXPTIME upper bounds, respectively, like for the respective non-probabilistic versions. The bisimilarity problems for OCA and vPDA are known to have matching lower bounds (thus being PSPACE-complete and EXPTIME-complete, respectively); we show that these lower bounds also hold for fully probabilistic versions that do not use non-determinism. △ Less

Submitted 14 November, 2018; v1 submitted 16 November, 2017; originally announced November 2017.

Journal ref: Logical Methods in Computer Science, Volume 14, Issue 4 (November 15, 2018) lmcs:4077

The Weisfeiler-Leman Dimension of Planar Graphs is at most 3

Authors: Sandra Kiefer, Ilia Ponomarenko, Pascal Schweitzer

Abstract: We prove that the Weisfeiler-Leman (WL) dimension of the class of all finite planar graphs is at most 3. In particular, every finite planar graph is definable in first-order logic with counting using at most 4 variables. The previously best known upper bounds for the dimension and number of variables were 14 and 15, respectively. First we show that, for dimension 3 and higher, the WL-algorithm c… ▽ More We prove that the Weisfeiler-Leman (WL) dimension of the class of all finite planar graphs is at most 3. In particular, every finite planar graph is definable in first-order logic with counting using at most 4 variables. The previously best known upper bounds for the dimension and number of variables were 14 and 15, respectively. First we show that, for dimension 3 and higher, the WL-algorithm correctly tests isomorphism of graphs in a minor-closed class whenever it determines the orbits of the automorphism group of any arc-colored 3-connected graph belonging to this class. Then we prove that, apart from several exceptional graphs (which have WL-dimension at most 2), the individualization of two correctly chosen vertices of a colored 3-connected planar graph followed by the 1-dimensional WL-algorithm produces the discrete vertex partition. This implies that the 3-dimensional WL-algorithm determines the orbits of a colored 3-connected planar graph. As a byproduct of the proof, we get a classification of the 3-connected planar graphs with fixing number 3. △ Less

Submitted 24 August, 2017; originally announced August 2017.

Comments: 34 pages, 3 figures, extended version of LICS 2017 paper

MSC Class: 03B70 ACM Class: F.4.1; F.2.2

On Strong Determinacy of Countable Stochastic Games

Authors: Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, Dominik Wojtczak

Abstract: We study 2-player turn-based perfect-information stochastic games with countably infinite state space. The players aim at maximizing/minimizing the probability of a given event (i.e., measurable set of infinite plays), such as reachability, Büchi, omega-regular or more general objectives. These games are known to be weakly determined, i.e., they have value. However, strong determinacy of thresho… ▽ More We study 2-player turn-based perfect-information stochastic games with countably infinite state space. The players aim at maximizing/minimizing the probability of a given event (i.e., measurable set of infinite plays), such as reachability, Büchi, omega-regular or more general objectives. These games are known to be weakly determined, i.e., they have value. However, strong determinacy of threshold objectives (given by an event and a threshold $c \in [0,1]$) was open in many cases: is it always the case that the maximizer or the minimizer has a winning strategy, i.e., one that enforces, against all strategies of the other player, that the objective is satisfied with probability $\ge c$ (resp. $< c$)? We show that almost-sure objectives (where $c=1$) are strongly determined. This vastly generalizes a previous result on finite games with almost-sure tail objectives. On the other hand we show that $\ge 1/2$ (co-)Büchi objectives are not strongly determined, not even if the game is finitely branching. Moreover, for almost-sure reachability and almost-sure Büchi objectives in finitely branching games, we strengthen strong determinacy by showing that one of the players must have a memoryless deterministic (MD) winning strategy. △ Less

Submitted 17 April, 2017; originally announced April 2017.

Comments: 13 pages

MSC Class: 91A15 ACM Class: G.3

Journal ref: LICS 2017

Parity Objectives in Countable MDPs

Authors: Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, Dominik Wojtczak

Abstract: 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-Buchi). In finite MDPs there always exist optimal memoryless deterministic (MD) strategies for parity objectives, but this does not generally hold for countably infinite MDPs. In particular, optimal strategies need not… ▽ More 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-Buchi). In finite MDPs there always exist optimal memoryless deterministic (MD) strategies for parity objectives, but this does not generally hold for countably infinite MDPs. In particular, optimal strategies need not exist. For countable infinite MDPs, we provide a complete picture of the memory requirements of optimal (resp., $ε$-optimal) strategies for all objectives in the Mostowski hierarchy. In particular, there is a strong dichotomy between two different types of objectives. For the first type, optimal strategies, if they exist, can be chosen MD, while for the second type optimal strategies require infinite memory. (I.e., for all objectives in the Mostowski hierarchy, if finite-memory randomized strategies suffice then also MD strategies suffice.) Similarly, some objectives admit $ε$-optimal MD-strategies, while for others $ε$-optimal strategies require infinite memory. Such a dichotomy also holds for the subclass of countably infinite MDPs that are finitely branching, though more objectives admit MD-strategies here. △ Less

Submitted 17 April, 2017; v1 submitted 14 April, 2017; originally announced April 2017.

On Restricted Nonnegative Matrix Factorization

Authors: Dmitry Chistikov, Stefan Kiefer, Ines Marušić, Mahsa Shirmohammadi, James Worrell

Abstract: Nonnegative matrix factorization (NMF) is the problem of decomposing a given nonnegative $n \times m$ matrix $M$ into a product of a nonnegative $n \times d$ matrix $W$ and a nonnegative $d \times 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… ▽ More Nonnegative matrix factorization (NMF) is the problem of decomposing a given nonnegative $n \times m$ matrix $M$ into a product of a nonnegative $n \times d$ matrix $W$ and a nonnegative $d \times 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. △ Less

Submitted 23 May, 2016; originally announced May 2016.

Comments: Full version of an ICALP'16 paper

Nonnegative Matrix Factorization Requires Irrationality

Authors: Dmitry Chistikov, Stefan Kiefer, Ines Marušić, Mahsa Shirmohammadi, James Worrell

Abstract: Nonnegative matrix factorization (NMF) is the problem of decomposing a given nonnegative $n \times m$ matrix $M$ into a product of a nonnegative $n \times d$ matrix $W$ and a nonnegative $d \times m$ matrix $H$. A longstanding open question, posed by Cohen and Rothblum in 1993, is whether a rational matrix $M$ always has an NMF of minimal inner dimension $d$ whose factors $W$ and $H$ are also rati… ▽ More Nonnegative matrix factorization (NMF) is the problem of decomposing a given nonnegative $n \times m$ matrix $M$ into a product of a nonnegative $n \times d$ matrix $W$ and a nonnegative $d \times m$ matrix $H$. A longstanding open question, posed by Cohen and Rothblum in 1993, is 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. △ Less

Submitted 22 March, 2017; v1 submitted 22 May, 2016; originally announced May 2016.

Comments: Journal version, to appear in the SIAM Journal on Applied Algebra and Geometry (SIAGA)

Upper Bounds on the Quantifier Depth for Graph Differentiation in First-Order Logic

Authors: Sandra Kiefer, Pascal Schweitzer

Abstract: We show that on graphs with n vertices, the 2-dimensional Weisfeiler-Leman algorithm requires at most O(n^2/log(n)) iterations to reach stabilization. This in particular shows that the previously best, trivial upper bound of O(n^2) is asymptotically not tight. In the logic setting, this translates to the statement that if two graphs of size n can be distinguished by a formula in first-order logic… ▽ More We show that on graphs with n vertices, the 2-dimensional Weisfeiler-Leman algorithm requires at most O(n^2/log(n)) iterations to reach stabilization. This in particular shows that the previously best, trivial upper bound of O(n^2) is asymptotically not tight. In the logic setting, this translates to the statement that if two graphs of size n can be distinguished by a formula in first-order logic with counting with 3 variables (i.e., in C3), then they can also be distinguished by a C3-formula that has quantifier depth at most O(n^2/log(n)). To prove the result we define a game between two players that enables us to decouple the causal dependencies between the processes happening simultaneously over several iterations of the algorithm. This allows us to treat large color classes and small color classes separately. As part of our proof we show that for graphs with bounded color class size, the number of iterations until stabilization is at most linear in the number of vertices. This also yields a corresponding statement in first-order logic with counting. Similar results can be obtained for the respective logic without counting quantifiers, i.e., for the logic L3. △ Less

Submitted 26 May, 2019; v1 submitted 11 May, 2016; originally announced May 2016.

ACM Class: F.4.1

Journal ref: Logical Methods in Computer Science, Volume 15, Issue 2 (May 30, 2019) lmcs:4015

Markov Chains and Unambiguous Automata

Authors: Christel Baier, Stefan Kiefer, Joachim Klein, David Müller, James Worrell

Abstract: Unambiguous automata are nondeterministic automata in which every word has at most one accepting run. In this paper we give a polynomial-time algorithm for model checking discrete-time Markov chains against ω-regular specifications represented as unambiguous automata. We furthermore show that the complexity of this model checking problem lies in NC: the subclass of P comprising those problems solv… ▽ More Unambiguous automata are nondeterministic automata in which every word has at most one accepting run. In this paper we give a polynomial-time algorithm for model checking discrete-time Markov chains against ω-regular specifications represented as unambiguous automata. We furthermore show that the complexity of this model checking problem lies in NC: the subclass of P comprising those problems solvable in poly-logarithmic parallel time. These complexity bounds match the known bounds for model checking Markov chains against specifications given as deterministic automata, notwithstanding the fact that unambiguous automata can be exponentially more succinct than deterministic automata. We report on an implementation of our procedure, including an experiment in which the implementation is used to model check LTL formulas on Markov chains. △ Less

Submitted 7 April, 2023; v1 submitted 3 May, 2016; originally announced May 2016.

Comments: 38 pages, accepted at JCSS. The first version (v1), 50 pages, is the full version of a paper accepted at CAV 2016

ACM Class: D.2.4; F.3.1

Efficient Quantile Computation in Markov Chains via Counting Problems for Parikh Images

Authors: Christoph Haase, Stefan Kiefer, Markus Lohrey

Abstract: A cost Markov chain is a Markov chain whose transitions are labelled with non-negative integer costs. A fundamental problem on this model, with applications in the verification of stochastic systems, is to compute information about the distribution of the total cost accumulated in a run. This includes the probability of large total costs, the median cost, and other quantiles. While expectations ca… ▽ More A cost Markov chain is a Markov chain whose transitions are labelled with non-negative integer costs. A fundamental problem on this model, with applications in the verification of stochastic systems, is to compute information about the distribution of the total cost accumulated in a run. This includes the probability of large total costs, the median cost, and other quantiles. While expectations can be computed in polynomial time, previous work has demonstrated that the computation of cost quantiles is harder but can be done in PSPACE. In this paper we show that cost quantiles in cost Markov chains can be computed in the counting hierarchy, thus providing evidence that computing those quantiles is likely not PSPACE-hard. We obtain this result by exhibiting a tight link to a problem in formal language theory: counting the number of words that are both accepted by a given automaton and have a given Parikh image. Motivated by this link, we comprehensively investigate the complexity of the latter problem. Among other techniques, we rely on the so-called BEST theorem for efficiently computing the number of Eulerian circuits in a directed graph. △ Less

Submitted 18 January, 2016; originally announced January 2016.

ACM Class: F.4.2; G.3