-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
Fully time-dependent cloud formation from a non-equilibrium gas-phase in exoplanetary atmospheres
Authors:
Sven Kiefer,
Helena Lecoq-Molinos,
Christiane Helling,
Nidhi Bangera,
Leen Decin
Abstract:
Recent observations suggest the presence of clouds in exoplanet atmospheres but have also shown that certain chemical species in the upper atmosphere might not be in chemical equilibrium. The goal of this work is to calculate the two main cloud formation processes, nucleation and bulk growth, consistently from a non-equilibrium gas-phase. The aim is further to explore the interaction between a kin…
▽ More
Recent observations suggest the presence of clouds in exoplanet atmospheres but have also shown that certain chemical species in the upper atmosphere might not be in chemical equilibrium. The goal of this work is to calculate the two main cloud formation processes, nucleation and bulk growth, consistently from a non-equilibrium gas-phase. The aim is further to explore the interaction between a kinetic gas-phase and cloud micro-physics. The cloud formation is modeled using the moment method and kinetic nucleation which are coupled to a gas-phase kinetic rate network. Specifically, the formation of cloud condensation nuclei is derived from cluster rates that include the thermochemical data of (TiO$_2$)$_N$ from N = 1 to 15. The surface growth of 9 bulk Al/Fe/Mg/O/Si/S/Ti binding materials considers the respective gas-phase species through condensation and surface reactions as derived from kinetic disequilibrium. The effect of completeness of rate networks and the time evolution of the cloud particle formation is studied for an example exoplanet HD 209458 b. A consistent, fully time-dependent cloud formation model in chemical disequilibrium with respect to nucleation, bulk growth and the gas-phase is presented and first test cases are studied. This model shows that cloud formation in exoplanet atmospheres is a fast process. This confirms previous findings that the formation of cloud particles is a local process. Tests on selected locations within the atmosphere of the gas-giant HD 209458 b show that the cloud particle number density and volume reach constant values within 1s. The complex kinetic polymer nucleation of TiO$_2$ confirms results from classical nucleation models. The surface reactions of SiO[s] and SiO$_2$[s] can create a catalytic cycle that dissociates H$_2$ to 2 H, resulting in a reduction of the CH$_4$ number densities.
△ Less
Submitted 6 November, 2023;
originally announced November 2023.
-
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.
-
The effect of thermal non-equilibrium on kinetic nucleation
Authors:
Sven Kiefer,
David Gobrecht,
Leen Decin,
Christiane Helling
Abstract:
Nucleation is considered to be the first step in dust and cloud formation in the atmospheres of asymptotic giant branch (AGB) stars, exoplanets, and brown dwarfs. In these environments dust and cloud particles grow to macroscopic sizes when gas phase species condense onto cloud condensation nuclei (CCNs). Understanding the formation processes of CCNs and dust in AGB stars is important because the…
▽ More
Nucleation is considered to be the first step in dust and cloud formation in the atmospheres of asymptotic giant branch (AGB) stars, exoplanets, and brown dwarfs. In these environments dust and cloud particles grow to macroscopic sizes when gas phase species condense onto cloud condensation nuclei (CCNs). Understanding the formation processes of CCNs and dust in AGB stars is important because the species that formed in their outflows enrich the interstellar medium. Although widely used, the validity of chemical and thermal equilibrium conditions is debatable in some of these highly dynamical astrophysical environments. We aim to derive a kinetic nucleation model that includes the effects of thermal non-equilibrium by adopting different temperatures for nucleating species, and to quantify the impact of thermal non-equilibrium on kinetic nucleation. Forward and backward rate coefficients are derived as part of a collisional kinetic nucleation theory ansatz. The endothermic backward rates are derived from the law of mass action in thermal non-equilibrium. We consider elastic collisions as thermal equilibrium drivers. For homogeneous TiO2 nucleation and a gas temperature of 1250 K, we find that differences in the kinetic cluster temperatures as small as 20 K increase the formation of larger TiO2 clusters by over an order of magnitude. An increase in cluster temperature of around 20 K at gas temperatures of 1000 K can reduce the formation of a larger TiO2 cluster by over an order of magnitude. Our results confirm and quantify the prediction of previous thermal non-equilibrium studies. Small thermal non-equilibria can cause a significant change in the synthesis of larger clusters. Therefore, it is important to use kinetic nucleation models that include thermal non-equilibrium to describe the formation of clusters in environments where even small thermal non-equilibria can be present.
△ Less
Submitted 16 February, 2023;
originally announced February 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.
-
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.
-
Spinning up the Surface: Evidence for Planetary Engulfment or Unexpected Angular Momentum Transport?
Authors:
Jamie Tayar,
Facundo D. Moyano,
Melinda Soares-Furtado,
Ana Escorza,
Meridith Joyce,
Sarah L. Martell,
Rafael A. García,
Sylvain N. Breton,
Stéphane Mathis,
Savita Mathur,
Vincent Delsanti,
Sven Kiefer,
Sabine Reffert,
Dominic M. Bowman,
Timothy Van Reeth,
Shreeya Shetye,
Charlotte Gehan,
Samuel K. Grunblatt
Abstract:
In this paper, we report the potential detection of a nonmonotonic radial rotation profile in a low-mass lower-luminosity giant star. For most low- and intermediate-mass stars, the rotation on the main sequence seems to be close to rigid. As these stars evolve into giants, the core contracts and the envelope expands, which should suggest a radial rotation profile with a fast core and a slower enve…
▽ More
In this paper, we report the potential detection of a nonmonotonic radial rotation profile in a low-mass lower-luminosity giant star. For most low- and intermediate-mass stars, the rotation on the main sequence seems to be close to rigid. As these stars evolve into giants, the core contracts and the envelope expands, which should suggest a radial rotation profile with a fast core and a slower envelope and surface. KIC 9267654, however, seems to show a surface rotation rate that is faster than its bulk envelope rotation rate, in conflict with this simple angular momentum conservation argument. We improve the spectroscopic surface constraint, show that the pulsation frequencies are consistent with the previously published core and envelope rotation rates, and demonstrate that the star does not show strong chemical peculiarities. We discuss the evidence against any tidally interacting stellar companion. Finally, we discuss the possible origin of this unusual rotation profile, including the potential ingestion of a giant planet or unusual angular momentum transport by tidal inertial waves triggered by a close substellar companion, and encourage further observational and theoretical efforts.
△ Less
Submitted 2 August, 2022;
originally announced August 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.
-
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.
-
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.
-
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.
-
Exploring the deep atmospheres of HD 209458b and WASP-43b using a non-gray general circulation model
Authors:
Aaron David Schneider,
Ludmila Carone,
Leen Decin,
Uffe Gråe Jørgensen,
Paul Mollière,
Robin Baeyens,
Sven Kiefer,
Christiane Helling
Abstract:
Simulations with a 3D general circulation model (GCM) suggest that one potential driver behind the observed radius inflation in hot Jupiters may be the downward advection of energy from the highly irradiated photosphere into the deeper layers. Here, we compare dynamical heat transport within the non-inflated hot Jupiter WASP-43b and the canonical inflated hot Jupiter HD 209458b, with similar effec…
▽ More
Simulations with a 3D general circulation model (GCM) suggest that one potential driver behind the observed radius inflation in hot Jupiters may be the downward advection of energy from the highly irradiated photosphere into the deeper layers. Here, we compare dynamical heat transport within the non-inflated hot Jupiter WASP-43b and the canonical inflated hot Jupiter HD 209458b, with similar effective temperatures. We investigate to what extent the radiatively driven heating and cooling in the photosphere (at pressures smaller than 1 bar) influence the deeper temperature profile (at pressures between 1 to 700 bar). Our simulations with the new non-gray 3D radiation-hydrodynamical model expeRT/MITgcm show that the deep temperature profile of WASP-43b is associated with a relatively cold adiabat. The deep layers of HD 209458b, however, do not converge and remain nearly unchanged regardless of whether a cold or a hot initial state is used. Furthermore, we show that different flow structures in the deep atmospheric layers arise. There, we find that WASP-43b exhibits a deep equatorial jet, driven by the relatively fast tidally locked rotation of this planet (0.81 days), as compared to HD 209458b (3.47 days). However, by comparing simulations with different rotation periods, we find that the resulting flow structures only marginally influence the temperature evolution in the deep atmosphere, which is almost completely dominated by radiative heating and cooling. Furthermore, we find that the evolution of deeper layers can influence the 3D temperature structure in the photosphere of WASP-43b. Thus, dayside emission spectra of WASP-43b may shed more light onto the dynamical processes occurring at greater depths.
△ Less
Submitted 3 October, 2022; v1 submitted 18 February, 2022;
originally announced February 2022.
-
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.
-
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.
-
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.
-
Direct-drive ocean wave-powered batch reverse osmosis
Authors:
Katie M. Brodersen,
Emily A. Bywater,
Alec M. Lanter,
Hayden H. Schennum,
Kumansh N. Furia,
Maulee K. Sheth,
Nathaniel S. Kiefer,
Brittany K. Cafferty,
Akshay K. Rao,
Jose M. Garcia,
David M. Warsinger
Abstract:
Ocean waves provide a consistent, reliable source of clean energy making them a viable energy source for desalination. Ocean wave energy is useful to coastal communities, especially island nations. However, large capital costs render current wave-powered desalination technologies economically infeasible. This work presents a high efficiency configuration for ocean wave energy powering batch revers…
▽ More
Ocean waves provide a consistent, reliable source of clean energy making them a viable energy source for desalination. Ocean wave energy is useful to coastal communities, especially island nations. However, large capital costs render current wave-powered desalination technologies economically infeasible. This work presents a high efficiency configuration for ocean wave energy powering batch reverse osmosis. The proposed system uses seawater as the working fluid in a hydro-mechanical wave energy converter and replaces the reverse osmosis high-pressure pump with a hydraulic converter for direct-drive coupling. This allows for minimal intermediary power conversions, fewer components, and higher efficiencies. The concept was analyzed with MATLAB to model the transient energy dynamics of the wave energy converter, power take-off system, and desalination load. The fully hydro-mechanical coupling, incorporating energy recovery, could achieve an SEC and LCOW as low as 2.30 kWh/m3 and $1.96, respectively, for different sea states. The results were validated at the sub-system level against existing literature on wave energy models and previous work completed on batch reverse osmosis models, as this system was the first to combine these two technologies. SEC and LCOW values were validated by comparing to known and predicted values for various types of RO systems.
△ Less
Submitted 15 July, 2021;
originally announced July 2021.
-
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.
-
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.
-
Spectral and angular differential imaging with SPHERE/IFS. Assessing the performance of various PCA-based approaches to PSF subtraction
Authors:
S. Kiefer,
A. J. Bohn,
S. P. Quanz,
M. Kenworthy,
T. Stolker
Abstract:
Angular differential imaging (ADI) and spectral differential imaging (SDI) are commonly used for direct detection and characterisation of young, Jovian exoplanets in datasets obtained with the SPHERE/IFS instrument. We compare the performance of ADI, SDI, and three combinations of ADI and SDI to find which technique achieves the highest signal-to-noise ratio (S/N), and we analyse their performance…
▽ More
Angular differential imaging (ADI) and spectral differential imaging (SDI) are commonly used for direct detection and characterisation of young, Jovian exoplanets in datasets obtained with the SPHERE/IFS instrument. We compare the performance of ADI, SDI, and three combinations of ADI and SDI to find which technique achieves the highest signal-to-noise ratio (S/N), and we analyse their performance as functions of integration time, field rotation, and wavelength range. We analyse SPHERE/IFS observations of three known exoplanets, namely Beta Pictoris b, 51 Eridani b, and HR 8799 e, with five differential imaging techniques. We split the datasets into subsets to vary each parameter before the data are processed with each technique. The differential imaging techniques are applied using principal component analysis (PCA). The tests show that a combination of SDI and ADI consistently achieves better results than ADI alone, and using SDI and ADI simultaneously (combined differential imaging; CODI) achieved the best results. The integration time test shows that targets with a separation larger than 0.24 arcsec observed with an integration time of more than 10$^3$s were photon-noise limited. Field rotation shows a strong correlation with S/N for field rotations up to 1 full width at half maximum (FWHM), after which no significant increase in S/N with field rotation is observed. Wavelength range variation shows a general increase in S/N for broader wavelength ranges, but no clear correlation is seen. Spectral information is essential to boost S/N compared to regular ADI. Our results suggest that CODI should be the preferred processing technique to search for new exoplanets with SPHERE/IFS. To optimise direct-imaging observations, the field rotation should exceed 1 FWHM to detect exoplanets at small separations.
△ Less
Submitted 9 June, 2021;
originally announced June 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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.