Showing 1–50 of 76 results for author: Haase, C

An efficient quantifier elimination procedure for Presburger arithmetic

Authors: Christoph Haase, Shankara Narayanan Krishna, Khushraj Madnani, Om Swostik Mishra, Georg Zetzsche

Abstract: All known quantifier elimination procedures for Presburger arithmetic require doubly exponential time for eliminating a single block of existentially quantified variables. It has even been claimed in the literature that this upper bound is tight. We observe that this claim is incorrect and develop, as the main result of this paper, a quantifier elimination procedure eliminating a block of existent… ▽ More All known quantifier elimination procedures for Presburger arithmetic require doubly exponential time for eliminating a single block of existentially quantified variables. It has even been claimed in the literature that this upper bound is tight. We observe that this claim is incorrect and develop, as the main result of this paper, a quantifier elimination procedure eliminating a block of existentially quantified variables in singly exponential time. As corollaries, we can establish the precise complexity of numerous problems. Examples include deciding (i) monadic decomposability for existential formulas, (ii) whether an existential formula defines a well-quasi ordering or, more generally, (iii) certain formulas of Presburger arithmetic with Ramsey quantifiers. Moreover, despite the exponential blowup, our procedure shows that under mild assumptions, even NP upper bounds for decision problems about quantifier-free formulas can be transferred to existential formulas. The technical basis of our results is a kind of small model property for parametric integer programming that generalizes the seminal results by von zur Gathen and Sieveking on small integer points in convex polytopes. △ Less

Submitted 2 May, 2024; originally announced May 2024.

Comments: Accepted for publication at ICALP 2024

On Layered Area-Proportional Rectangle Contact Representations

Authors: Carolina Haase, Philipp Kindermann

Abstract: A pair $\langle G_0, G_1 \rangle$ of graphs admits a mutual witness proximity drawing $\langle Γ_0, Γ_1 \rangle$ when: (i) $Γ_i$ represents $G_i$, and (ii) there is an edge $(u,v)$ in $Γ_i$ if and only if there is no vertex $w$ in $Γ_{1-i}$ that is ``too close'' to both $u$ and $v$ ($i=0,1$). In this paper, we consider infinitely many definitions of closeness by adopting the $β$-proximity rule for… ▽ More A pair $\langle G_0, G_1 \rangle$ of graphs admits a mutual witness proximity drawing $\langle Γ_0, Γ_1 \rangle$ when: (i) $Γ_i$ represents $G_i$, and (ii) there is an edge $(u,v)$ in $Γ_i$ if and only if there is no vertex $w$ in $Γ_{1-i}$ that is ``too close'' to both $u$ and $v$ ($i=0,1$). In this paper, we consider infinitely many definitions of closeness by adopting the $β$-proximity rule for any $β\in [1,\infty]$ and study pairs of isomorphic trees that admit a mutual witness $β$-proximity drawing. Specifically, we show that every two isomorphic trees admit a mutual witness $β$-proximity drawing for any $β\in [1,\infty]$. The constructive technique can be made ``robust'': For some tree pairs we can suitably prune linearly many leaves from one of the two trees and still retain their mutual witness $β$-proximity drawability. Notably, in the special case of isomorphic caterpillars and $β=1$, we construct linearly separable mutual witness Gabriel drawings. △ Less

Submitted 25 November, 2023; originally announced November 2023.

Comments: Appears in the Proceedings of the 18th International Conference and Workshops on Algorithms and Computation (WALCOM 2024)

Reachability in Fixed VASS: Expressiveness and Lower Bounds

Authors: Andrei Draghici, Christoph Haase, Andrew Ryzhikov

Abstract: The recent years have seen remarkable progress in establishing the complexity of the reachability problem for vector addition systems with states (VASS), equivalently known as Petri nets. Existing work primarily considers the case in which both the VASS as well as the initial and target configurations are part of the input. In this paper, we investigate the reachability problem in the setting wher… ▽ More The recent years have seen remarkable progress in establishing the complexity of the reachability problem for vector addition systems with states (VASS), equivalently known as Petri nets. Existing work primarily considers the case in which both the VASS as well as the initial and target configurations are part of the input. In this paper, we investigate the reachability problem in the setting where the VASS is fixed and only the initial configuration is variable. We show that fixed VASS fully express arithmetic on initial segments of the natural numbers. It follows that there is a very weak reduction from any fixed such number-theoretic predicate (e.g. primality or square-freeness) to reachability in fixed VASS where configurations are presented in unary. If configurations are given in binary, we show that there is a fixed VASS with five counters whose reachability problem is PSPACE-hard. △ Less

Submitted 25 October, 2023; originally announced October 2023.

Decoding Emotional Experiences in Dyadic Conversations of Married Couples: Leveraging Semantic Similarity through Sentence Embedding

Authors: Chen-Wei Yu, Yun-Shiuan Chuang, Alexandros N. Lotsos, Claudia M. Haase

Abstract: Recent advancements in Natural Language Processing (NLP) have highlighted the potential of sentence embeddings in measuring semantic similarity (hereafter similarity). Yet, whether this approach can be used to analyze real-world dyadic interactions and predict people's emotional experiences in response to these interactions remains largely uncharted. To bridge this gap, the present study analyzes… ▽ More Recent advancements in Natural Language Processing (NLP) have highlighted the potential of sentence embeddings in measuring semantic similarity (hereafter similarity). Yet, whether this approach can be used to analyze real-world dyadic interactions and predict people's emotional experiences in response to these interactions remains largely uncharted. To bridge this gap, the present study analyzes verbal conversations of 50 married couples who engage in naturalistic 10-minute conflict and 10-minute positive conversations. Transformer-based model General Text Embeddings-Large is employed to obtain the embeddings of the utterances from each speaker. The overall similarity of the conversations is then quantified by the average cosine similarity between the embeddings of adjacent utterances. Results show that lower similarity is associated with greater positive emotional experiences in the positive (but not conflict) conversation. Follow-up analyses show that (a) findings remain stable when controlling for marital satisfaction and the number of utterance pairs and (b) the similarity measure is valid in capturing critical features of a dyadic conversation. The present study underscores the potency of sentence embeddings in understanding links between interpersonal dynamics and individual emotional experiences, paving the way for innovative applications of NLP tools in affective and relationship science. △ Less

Submitted 25 February, 2024; v1 submitted 22 September, 2023; originally announced September 2023.

LDP polygons and the number 12 revisited

Authors: Ulrike Bücking, Christian Haase, Karin Schaller, Jan-Hendrik de Wiljes

Abstract: We give a combinatorial proof of a lattice point identity involving a lattice polygon and its dual, generalizing the formula $area(Δ) + area(Δ^*) = 6$ for reflexive $Δ$. The identity is equivalent to the stringy Libgober-Wood identity for toric log del Pezzo surfaces. We give a combinatorial proof of a lattice point identity involving a lattice polygon and its dual, generalizing the formula $area(Δ) + area(Δ^*) = 6$ for reflexive $Δ$. The identity is equivalent to the stringy Libgober-Wood identity for toric log del Pezzo surfaces. △ Less

Submitted 5 September, 2023; originally announced September 2023.

Comments: 20 pages, 8 figures

MSC Class: 52B20 (Primary) 14M25; 11F20; 32J15 (Secondary)

Mutual Witness Proximity Drawings of Isomorphic Trees

Authors: Carolina Haase, Philipp Kindermann, William J. Lenhart, Giuseppe Liotta

Abstract: A pair $\langle G_0, G_1 \rangle$ of graphs admits a mutual witness proximity drawing $\langle Γ_0, Γ_1 \rangle$ when: (i) $Γ_i$ represents $G_i$, and (ii) there is an edge $(u,v)$ in $Γ_i$ if and only if there is no vertex $w$ in $Γ_{1-i}$ that is ``too close'' to both $u$ and $v$ ($i=0,1$). In this paper, we consider infinitely many definitions of closeness by adopting the $β$-proximity rule for… ▽ More A pair $\langle G_0, G_1 \rangle$ of graphs admits a mutual witness proximity drawing $\langle Γ_0, Γ_1 \rangle$ when: (i) $Γ_i$ represents $G_i$, and (ii) there is an edge $(u,v)$ in $Γ_i$ if and only if there is no vertex $w$ in $Γ_{1-i}$ that is ``too close'' to both $u$ and $v$ ($i=0,1$). In this paper, we consider infinitely many definitions of closeness by adopting the $β$-proximity rule for any $β\in [1,\infty]$ and study pairs of isomorphic trees that admit a mutual witness $β$-proximity drawing. Specifically, we show that every two isomorphic trees admit a mutual witness $β$-proximity drawing for any $β\in [1,\infty]$. The constructive technique can be made ``robust'': For some tree pairs we can suitably prune linearly many leaves from one of the two trees and still retain their mutual witness $β$-proximity drawability. Notably, in the special case of isomorphic caterpillars and $β=1$, we construct linearly separable mutual witness Gabriel drawings. △ Less

Submitted 4 September, 2023; originally announced September 2023.

Comments: Appears in the Proceedings of the 31st International Symposium on Graph Drawing and Network Visualization (GD 2023)

Integer Programming with GCD Constraints

Authors: Rémy Defossez, Christoph Haase, Alessio Mansutti, Guillermo A. Perez

Abstract: We study the non-linear extension of integer programming with greatest common divisor constraints of the form $\gcd(f,g) \sim d$, where $f$ and $g$ are linear polynomials, $d$ is a positive integer, and $\sim$ is a relation among $\leq, =, \neq$ and $\geq$. We show that the feasibility problem for these systems is in NP, and that an optimal solution minimizing a linear objective function, if it ex… ▽ More We study the non-linear extension of integer programming with greatest common divisor constraints of the form $\gcd(f,g) \sim d$, where $f$ and $g$ are linear polynomials, $d$ is a positive integer, and $\sim$ is a relation among $\leq, =, \neq$ and $\geq$. We show that the feasibility problem for these systems is in NP, and that an optimal solution minimizing a linear objective function, if it exists, has polynomial bit length. To show these results, we identify an expressive fragment of the existential theory of the integers with addition and divisibility that admits solutions of polynomial bit length. It was shown by Lipshitz [Trans. Am. Math. Soc., 235, pp. 271-283, 1978] that this theory adheres to a local-to-global principle in the following sense: a formula $Φ$ is equi-satisfiable with a formula $Ψ$ in this theory such that $Ψ$ has a solution if and only if $Ψ$ has a solution modulo every prime $p$. We show that in our fragment, only a polynomial number of primes of polynomial bit length need to be considered, and that the solutions modulo prime numbers can be combined to yield a solution to $Φ$ of polynomial bit length. As a technical by-product, we establish a Chinese-remainder-type theorem for systems of congruences and non-congruences showing that solution sizes do not depend on the magnitude of the moduli of non-congruences. △ Less

Submitted 25 August, 2023; originally announced August 2023.

Semënov Arithmetic, Affine VASS, and String Constraints

Authors: Andrei Draghici, Christoph Haase, Florin Manea

Abstract: We study extensions of Semënov arithmetic, the first-order theory of the structure $(\mathbb{N}, +, 2^x)$. It is well-knonw that this theory becomes undecidable when extended with regular predicates over tuples of number strings, such as the Büchi $V_2$-predicate. We therefore restrict ourselves to the existential theory of Semënov arithmetic and show that this theory is decidable in EXPSPACE when… ▽ More We study extensions of Semënov arithmetic, the first-order theory of the structure $(\mathbb{N}, +, 2^x)$. It is well-knonw that this theory becomes undecidable when extended with regular predicates over tuples of number strings, such as the Büchi $V_2$-predicate. We therefore restrict ourselves to the existential theory of Semënov arithmetic and show that this theory is decidable in EXPSPACE when extended with arbitrary regular predicates over tuples of number strings. Our approach relies on a reduction to the language emptiness problem for a restricted class of affine vector addition systems with states, which we show decidable in EXPSPACE. As an application of our results, we settle an open problem from the literature and show decidability of a class of string constraints involving length constraints. △ Less

Submitted 26 June, 2023; originally announced June 2023.

Comments: 19 pages, one figure

Universal quantification makes automatic structures hard to decide

Authors: Christoph Haase, Radosław Piórkowski

Abstract: Automatic structures are structures whose universe and relations can be represented as regular languages. It follows from the standard closure properties of regular languages that the first-order theory of an automatic structure is decidable. While existential quantifiers can be eliminated in linear time by application of a homomorphism, universal quantifiers are commonly eliminated via the identi… ▽ More Automatic structures are structures whose universe and relations can be represented as regular languages. It follows from the standard closure properties of regular languages that the first-order theory of an automatic structure is decidable. While existential quantifiers can be eliminated in linear time by application of a homomorphism, universal quantifiers are commonly eliminated via the identity $\forall{x}. Φ\equiv \neg (\exists{x}. \neg Φ)$. If $Φ$ is represented in the standard way as an NFA, a priori this approach results in a doubly exponential blow-up. However, the recent literature has shown that there are classes of automatic structures for which universal quantifiers can be eliminated by different means without this blow-up by treating them as first-class citizens and not resorting to double complementation. While existing lower bounds for some classes of automatic structures show that a singly exponential blow-up is unavoidable when eliminating a universal quantifier, it is not known whether there may be better approaches that avoid the naïve doubly exponential blow-up, perhaps at least in restricted settings. In this paper, we answer this question negatively and show that there is a family of NFA representing automatic relations for which the minimal NFA recognising the language after eliminating a single universal quantifier is doubly exponential, and deciding whether this language is empty is \expspace-complete. The techniques underlying our \expspace lower bound further enable us to establish new lower bounds for some fragments of Büchi arithmetic with a fixed number of quantifier alternations. △ Less

Submitted 13 May, 2024; v1 submitted 17 June, 2023; originally announced June 2023.

Minimum Wage Pass-through to Wholesale and Retail Prices: Evidence from Cannabis Scanner Data

Authors: Carl Hase

Abstract: A growing empirical literature finds that firms pass the cost of minimum wage hikes onto consumers via higher retail prices. Yet, little is known about minimum wage effects on wholesale prices and whether retailers face a wholesale cost shock in addition to the labor cost shock. I exploit the vertically disintegrated market structure of Washington state's legal recreational cannabis industry to in… ▽ More A growing empirical literature finds that firms pass the cost of minimum wage hikes onto consumers via higher retail prices. Yet, little is known about minimum wage effects on wholesale prices and whether retailers face a wholesale cost shock in addition to the labor cost shock. I exploit the vertically disintegrated market structure of Washington state's legal recreational cannabis industry to investigate minimum wage pass-through to wholesale and retail prices. In a difference-in-differences with continuous treatment framework, I utilize scanner data on $6 billion of transactions across the supply chain and leverage geographic variation in firms' minimum wage exposure across six minimum wage hikes between 2018 and 2021. When ignoring wholesale cost effects, I find retail pass-through elasticities consistent with existing literature -- yet retail pass-through elasticities more than double once wholesale cost effects are accounted for. Retail markups do not adjust to the wholesale cost shock, indicating a full pass-through of the wholesale cost shock to retail prices. The results highlight the importance of analyzing the entire supply chain when evaluating the product market effects of minimum wage hikes. △ Less

Submitted 9 October, 2023; v1 submitted 18 March, 2023; originally announced March 2023.

Lower Bounds on the Depth of Integral ReLU Neural Networks via Lattice Polytopes

Authors: Christian Haase, Christoph Hertrich, Georg Loho

Abstract: We prove that the set of functions representable by ReLU neural networks with integer weights strictly increases with the network depth while allowing arbitrary width. More precisely, we show that $\lceil\log_2(n)\rceil$ hidden layers are indeed necessary to compute the maximum of $n$ numbers, matching known upper bounds. Our results are based on the known duality between neural networks and Newto… ▽ More We prove that the set of functions representable by ReLU neural networks with integer weights strictly increases with the network depth while allowing arbitrary width. More precisely, we show that $\lceil\log_2(n)\rceil$ hidden layers are indeed necessary to compute the maximum of $n$ numbers, matching known upper bounds. Our results are based on the known duality between neural networks and Newton polytopes via tropical geometry. The integrality assumption implies that these Newton polytopes are lattice polytopes. Then, our depth lower bounds follow from a parity argument on the normalized volume of faces of such polytopes. △ Less

Submitted 24 February, 2023; originally announced February 2023.

Comments: ICLR 2023 conference paper

Fine Polyhedral Adjunction Theory

Authors: Sofía Garzón Mora, Christian Haase

Abstract: Originally introduced by Fine and Reid in the study of plurigenera of toric hypersurfaces, the Fine interior of a lattice polytope got recently into the focus of research. It is has been used for constructing canonical models in the sense of Mori Theory [arXiv:2008.05814]. Based on the Fine interior, we propose here a modification of the original adjoint polytopes as defined in [arXiv:1105.2415],… ▽ More Originally introduced by Fine and Reid in the study of plurigenera of toric hypersurfaces, the Fine interior of a lattice polytope got recently into the focus of research. It is has been used for constructing canonical models in the sense of Mori Theory [arXiv:2008.05814]. Based on the Fine interior, we propose here a modification of the original adjoint polytopes as defined in [arXiv:1105.2415], by defining the Fine adjoint polytope $P^{F(s)}$ of $P$ as consisting of the points in $P$ that have lattice distance at least $s$ to all valid inequalities for $P$. We obtain a Fine Polyhedral Adjunction Theory that is, in many respects, better behaved than its original analogue. Many existing results in Polyhedral Adjunction Theory carry over, some with stronger conclusions, as decomposing polytopes into Cayley sums, and most with simpler, more natural proofs as in the case of the finiteness of the Fine spectrum. △ Less

Submitted 8 February, 2023; originally announced February 2023.

Comments: 10 pages, 3 figures

MSC Class: 52B20 (Primary) 14M25; 14C20 (Secondary)

On the finite generation of valuation semigroups on toric surfaces

Authors: Klaus Altmann, Christian Haase, Alex Küronya, Karin Schaller, Lena Walter

Abstract: We provide a combinatorial criterion for the finite generation of a valuation semigroup associated with an ample divisor on a smooth toric surface and a non-toric valuation of maximal rank. As an application, we construct a lattice polytope such that none of the valuation semigroups of the associated polarized toric variety coming from one-parameter subgroups and centered at a non-toric point are… ▽ More We provide a combinatorial criterion for the finite generation of a valuation semigroup associated with an ample divisor on a smooth toric surface and a non-toric valuation of maximal rank. As an application, we construct a lattice polytope such that none of the valuation semigroups of the associated polarized toric variety coming from one-parameter subgroups and centered at a non-toric point are finitely generated. △ Less

Submitted 7 May, 2024; v1 submitted 13 September, 2022; originally announced September 2022.

Comments: 22 pages, 13 figures

MSC Class: 14C20; 14M25; 52B20

Journal ref: Épijournal de Géométrie Algébrique, Volume 8 (2024), Article no. 6

METL: a modern ETL pipeline with a dynamic map** matrix

Authors: Christian Haase, Timo Röseler, Mattias Seidel

Abstract: Modern ETL streaming pipelines extract data from various sources and forward it to multiple consumers, such as data warehouses (DW) and analytical systems that leverage machine learning (ML). However, the increasing number of systems that are connected to such pipelines requires new solutions for data integration. The canonical (or common) data model (CDM) offers such an integration. It is particu… ▽ More Modern ETL streaming pipelines extract data from various sources and forward it to multiple consumers, such as data warehouses (DW) and analytical systems that leverage machine learning (ML). However, the increasing number of systems that are connected to such pipelines requires new solutions for data integration. The canonical (or common) data model (CDM) offers such an integration. It is particular useful for integrating microservice systems into ETL pipelines. (Villaca et al 2020, Oliveira et al 2019) However, a map** to a CDM is complex. (Lemcke et al 2012) There are three complexity problems, namely the size of the required map** matrix, the automation of updates of the matrix in response to changes in the extraction sources and the time efficiency of the map**. In this paper, we present a new solution for these problems. More precisely, we present a new dynamic map** matrix (DMM), which is based on permutation matrices that are obtained by block-partitioning the full map** matrix. We show that the DMM can be used for automated updates in response to schema changes, for parallel computation in near real-time and for highly efficient compacting. For the solution, we draw on research into matrix partitioning (Quinn 2004) and dynamic networks (Haase et al 2021). The DMM has been implemented into an app called Message ETL (METL). METL is the key part of a new ETL streaming pipeline at EOS that conducts the transformation to a CDM. The ETL pipeline is based on Kafka-streams. It extracts data from more than 80 microservices with log-based Change Data Capture (CDC) with Debezium and loads the data to a DW and an ML platform. EOS is part of the Otto-Group, the second-largest e-commerce provider in Europe. △ Less

Submitted 31 March, 2022; v1 submitted 19 March, 2022; originally announced March 2022.

Comments: version 6: clean up

SCoT: Sense Clustering over Time: a tool for the analysis of lexical change

Authors: Christian Haase, Saba Anwar, Seid Muhie Yimam, Alexander Friedrich, Chris Biemann

Abstract: We present Sense Clustering over Time (SCoT), a novel network-based tool for analysing lexical change. SCoT represents the meanings of a word as clusters of similar words. It visualises their formation, change, and demise. There are two main approaches to the exploration of dynamic networks: the discrete one compares a series of clustered graphs from separate points in time. The continuous one ana… ▽ More We present Sense Clustering over Time (SCoT), a novel network-based tool for analysing lexical change. SCoT represents the meanings of a word as clusters of similar words. It visualises their formation, change, and demise. There are two main approaches to the exploration of dynamic networks: the discrete one compares a series of clustered graphs from separate points in time. The continuous one analyses the changes of one dynamic network over a time-span. SCoT offers a new hybrid solution. First, it aggregates time-stamped documents into intervals and calculates one sense graph per discrete interval. Then, it merges the static graphs to a new type of dynamic semantic neighbourhood graph over time. The resulting sense clusters offer uniquely detailed insights into lexical change over continuous intervals with model transparency and provenance. SCoT has been successfully used in a European study on the changing meaning of `crisis'. △ Less

Submitted 18 March, 2022; originally announced March 2022.

Comments: Update of https://aclanthology.org/2021.eacl-demos.23/

Journal ref: https://aclanthology.org/2021.eacl-demos.23/

Control of Electrochemical Corrosion Properties by Influencing Mn Partitioning through Intercritically Annealing of Medium-Mn Steel

Authors: René Daniel Pütz, Tarek Allam, Junmiao Wang, Jakub Nowak, Christian Haase, Stefanie Sandlöbes-Haut, Ulrich Krupp, Daniela Zander

Abstract: Medium-Mn steels exhibit excellent mechanical properties and lower production costs compared to high-Mn steels, which makes them a potential material for future application in the automotive industry. Intercritical annealing (ICA) after cold rolling allows to control the stacking fault energy (SFE) of austenite, the fraction of ferrite and reverted austenite, and the element partitioning (especial… ▽ More Medium-Mn steels exhibit excellent mechanical properties and lower production costs compared to high-Mn steels, which makes them a potential material for future application in the automotive industry. Intercritical annealing (ICA) after cold rolling allows to control the stacking fault energy (SFE) of austenite, the fraction of ferrite and reverted austenite, and the element partitioning (especially Mn). Although Mn deteriorates the corrosion behavior of Fe-Mn-Al alloys, the influence of austenite fraction and element partitioning of Mn on the electrochemical corrosion behavior has not been investigated yet. Therefore, the electrochemical corrosion behavior in 0.1 M H2SO4 of X6MnAl12-3, which was intercritically annealed for 2 h at 550 °C, 600 °C and 700 °C, was investigated by potentiodynamic polarization (PDP), electrochemical impedance spectroscopy (EIS) and mass spectroscopy with inductively coupled plasma (ICP-MS). Additionally, specimens after 1 h and 24 h of immersion were examined via SEM to visualize the corrosion damage. The ICA specimens showed a selective dissolution of reverted austenite due to its micro-galvanic coupling with the adjacent ferrite. The severity of the micro-galvanic coupling can be reduced by decreasing the interface area as well as the chemical gradient of mainly Mn between ferrite and reverted austenite by ICA. △ Less

Submitted 18 October, 2021; originally announced October 2021.

Comments: 23 pages, 14 Figures, 4 Tables

Classifier construction in Boolean networks using algebraic methods

Authors: Robert Schwieger, Matías R. Bender, Heike Siebert, Christian Haase

Abstract: We investigate how classifiers for Boolean networks (BNs) can be constructed and modified under constraints. A typical constraint is to observe only states in attractors or even more specifically steady states of BNs. Steady states of BNs are one of the most interesting features for application. Large models can possess many steady states. In the typical scenario motivating this paper we start fro… ▽ More We investigate how classifiers for Boolean networks (BNs) can be constructed and modified under constraints. A typical constraint is to observe only states in attractors or even more specifically steady states of BNs. Steady states of BNs are one of the most interesting features for application. Large models can possess many steady states. In the typical scenario motivating this paper we start from a Boolean model with a given classification of the state space into phenotypes defined by high-level readout components. In order to link molecular biomarkers with experimental design, we search for alternative components suitable for the given classification task. This is useful for modelers of regulatory networks for suggesting experiments and measurements based on their models. It can also help to explain causal relations between components and phenotypes. To tackle this problem we need to use the structure of the BN and the constraints. This calls for an algebraic approach. Indeed we demonstrate that this problem can be reformulated into the language of algebraic geometry. While already interesting in itself, this allows us to use Groebner bases to construct an algorithm for finding such classifiers. We demonstrate the usefulness of this algorithm as a proof of concept on a model with 25 components. △ Less

Submitted 19 August, 2021; originally announced August 2021.

Comments: Appeared in the Proceedings of the 18th International Conference on Computational Methods in Systems Biology (CMSB 2020)

Journal ref: Computational Methods in Systems Biology, Lecture Notes in Computer Science, 2020

Competitive equilibrium always exists for combinatorial auctions with graphical pricing schemes

Authors: Marie-Charlotte Brandenburg, Christian Haase, Ngoc Mai Tran

Abstract: We show that a competitive equilibrium always exists in combinatorial auctions with anonymous graphical valuations and pricing, using discrete geometry. This is an intuitive and easy-to-construct class of valuations that can model both complementarity and substitutes, and to our knowledge, it is the first class besides gross substitutes that have guaranteed competitive equilibrium. We prove throug… ▽ More We show that a competitive equilibrium always exists in combinatorial auctions with anonymous graphical valuations and pricing, using discrete geometry. This is an intuitive and easy-to-construct class of valuations that can model both complementarity and substitutes, and to our knowledge, it is the first class besides gross substitutes that have guaranteed competitive equilibrium. We prove through counter-examples that our result is tight, and we give explicit algorithms for constructive competitive pricing vectors. We also give extensions to multi-unit combinatorial auctions (also known as product-mix auctions). Combined with theorems on graphical valuations and pricing equilibrium of Candogan, Ozdagar and Parrilo, our results indicate that quadratic pricing is a highly practical method to run combinatorial auctions. △ Less

Submitted 5 November, 2021; v1 submitted 19 July, 2021; originally announced July 2021.

Comments: 24 pages, 5 figures

MSC Class: 91B26; 14T90; 52B20

Unsupervised Instance Selection with Low-Label, Supervised Learning for Outlier Detection

Authors: Trent J. Bradberry, Christopher H. Hase, LeAnna Kent, Joel A. Góngora

Abstract: The laborious process of labeling data often bottlenecks projects that aim to leverage the power of supervised machine learning. Active Learning (AL) has been established as a technique to ameliorate this condition through an iterative framework that queries a human annotator for labels of instances with the most uncertain class assignment. Via this mechanism, AL produces a binary classifier train… ▽ More The laborious process of labeling data often bottlenecks projects that aim to leverage the power of supervised machine learning. Active Learning (AL) has been established as a technique to ameliorate this condition through an iterative framework that queries a human annotator for labels of instances with the most uncertain class assignment. Via this mechanism, AL produces a binary classifier trained on less labeled data but with little, if any, loss in predictive performance. Despite its advantages, AL can have difficulty with class-imbalanced datasets and results in an inefficient labeling process. To address these drawbacks, we investigate our unsupervised instance selection (UNISEL) technique followed by a Random Forest (RF) classifier on 10 outlier detection datasets under low-label conditions. These results are compared to AL performed on the same datasets. Further, we investigate the combination of UNISEL and AL. Results indicate that UNISEL followed by an RF performs comparably to AL with an RF and that the combination of UNISEL and AL demonstrates superior performance. The practical implications of these findings in terms of time savings and generalizability afforded by UNISEL are discussed. △ Less

Submitted 17 March, 2022; v1 submitted 26 April, 2021; originally announced April 2021.

Comments: 16 pages, 4 figures

MSC Class: 62H30; 68T10

Presburger arithmetic with threshold counting quantifiers is easy

Authors: Dmitry Chistikov, Christoph Haase, Alessio Mansutti

Abstract: We give a quantifier elimination procedures for the extension of Presburger arithmetic with a unary threshold counting quantifier $\exists^{\ge c} y$ that determines whether the number of different $y$ satisfying some formula is at least $c \in \mathbb N$, where $c$ is given in binary. Using a standard quantifier elimination procedure for Presburger arithmetic, the resulting theory is easily seen… ▽ More We give a quantifier elimination procedures for the extension of Presburger arithmetic with a unary threshold counting quantifier $\exists^{\ge c} y$ that determines whether the number of different $y$ satisfying some formula is at least $c \in \mathbb N$, where $c$ is given in binary. Using a standard quantifier elimination procedure for Presburger arithmetic, the resulting theory is easily seen to be decidable in 4ExpTime. Our main contribution is to develop a novel quantifier-elimination procedure for a more general counting quantifier that decides this theory in 3ExpTime, meaning that it is no harder to decide than standard Presburger arithmetic. As a side result, we obtain an improved quantifier elimination procedure for Presburger arithmetic with counting quantifiers as studied by Schweikardt [ACM Trans. Comput. Log., 6(3), pp. 634-671, 2005], and a 3ExpTime quantifier-elimination procedure for Presburger arithmetic extended with a generalised modulo counting quantifier. △ Less

Submitted 8 March, 2021; originally announced March 2021.

On the Expressiveness of Büchi Arithmetic

Authors: Christoph Haase, Jakub Różycki

Abstract: We show that the existential fragment of Büchi arithmetic is strictly less expressive than full Büchi arithmetic of any base, and moreover establish that its $Σ_2$-fragment is already expressively complete. Furthermore, we show that regular languages of polynomial growth are definable in the existential fragment of Büchi arithmetic. We show that the existential fragment of Büchi arithmetic is strictly less expressive than full Büchi arithmetic of any base, and moreover establish that its $Σ_2$-fragment is already expressively complete. Furthermore, we show that regular languages of polynomial growth are definable in the existential fragment of Büchi arithmetic. △ Less

Submitted 2 March, 2021; v1 submitted 24 October, 2020; originally announced October 2020.

ACM Class: F.4.1; F.4.3

Directed Reachability for Infinite-State Systems

Authors: Michael Blondin, Christoph Haase, Philip Offtermatt

Abstract: Numerous tasks in program analysis and synthesis reduce to deciding reachability in possibly infinite graphs such as those induced by Petri nets. However, the Petri net reachability problem has recently been shown to require non-elementary time, which raises questions about the practical applicability of Petri nets as target models. In this paper, we introduce a novel approach for efficiently semi… ▽ More Numerous tasks in program analysis and synthesis reduce to deciding reachability in possibly infinite graphs such as those induced by Petri nets. However, the Petri net reachability problem has recently been shown to require non-elementary time, which raises questions about the practical applicability of Petri nets as target models. In this paper, we introduce a novel approach for efficiently semi-deciding the reachability problem for Petri nets in practice. Our key insight is that computationally lightweight over-approximations of Petri nets can be used as distance oracles in classical graph exploration algorithms such as A* and greedy best-first search. We provide and evaluate a prototype implementation of our approach that outperforms existing state-of-the-art tools, sometimes by orders of magnitude, and which is also competitive with domain-specific tools on benchmarks coming from program synthesis and concurrent program analysis. △ Less

Submitted 15 October, 2020; originally announced October 2020.

Comments: 29 pages, 13 figures

Toric Newton-Okounkov functions with an application to the rationality of certain Seshadri constants on surfaces

Authors: Christian Haase, Alex Küronya, Lena Walter

Abstract: We initiate a combinatorial study of Newton-Okounkov functions on toric varieties with an eye on the rationality of asymptotic invariants of line bundles. In the course of our efforts we identify a combinatorial condition which ensures a controlled behavior of the appropriate Newton-Okounkov function on a toric surface. Our approach yields the rationality of many Seshadri constants that have not b… ▽ More We initiate a combinatorial study of Newton-Okounkov functions on toric varieties with an eye on the rationality of asymptotic invariants of line bundles. In the course of our efforts we identify a combinatorial condition which ensures a controlled behavior of the appropriate Newton-Okounkov function on a toric surface. Our approach yields the rationality of many Seshadri constants that have not been settled before. △ Less

Submitted 19 January, 2021; v1 submitted 10 August, 2020; originally announced August 2020.

Comments: 52 pages, 37 figures; significant revision of section 5

MSC Class: 14C20; 14M25; 52B20

3D aspects of materials design for metals and alloys

Authors: Ulrich Krupp, Christian Haase, Wenwen Song, Wolfgang Bleck, Katrin Jahns

Abstract: Nowadays, most structural integrity concepts rely on simplified isotropic ma-terial data that are used within continuum mechanics modeling approaches. In contrast, modern casting and forming processes yield complex microstruc-tures coming along with pronounced gradients in the material's properties in various length scales. By means of additive manufacturing. bionics-inspired structures can be per… ▽ More Nowadays, most structural integrity concepts rely on simplified isotropic ma-terial data that are used within continuum mechanics modeling approaches. In contrast, modern casting and forming processes yield complex microstruc-tures coming along with pronounced gradients in the material's properties in various length scales. By means of additive manufacturing. bionics-inspired structures can be perfectly adapted to the space-resolved load distribution. Specific temperature control during solidification or heat treatment allow for usage of anisotropy and precipitation effects for materials optimization down to the atomic length scale. The present paper shows the significance and practical application of a three-dimensional correlation between the material's microstructure and its technical properties. △ Less

Submitted 24 September, 2019; originally announced September 2019.

Comments: in German

Affine Extensions of Integer Vector Addition Systems with States

Authors: Michael Blondin, Christoph Haase, Filip Mazowiecki, Mikhail Raskin

Abstract: We study the reachability problem for affine $\mathbb{Z}$-VASS, which are integer vector addition systems with states in which transitions perform affine transformations on the counters. This problem is easily seen to be undecidable in general, and we therefore restrict ourselves to affine $\mathbb{Z}$-VASS with the finite-monoid property (afmp-$\mathbb{Z}$-VASS). The latter have the property that… ▽ More We study the reachability problem for affine $\mathbb{Z}$-VASS, which are integer vector addition systems with states in which transitions perform affine transformations on the counters. This problem is easily seen to be undecidable in general, and we therefore restrict ourselves to affine $\mathbb{Z}$-VASS with the finite-monoid property (afmp-$\mathbb{Z}$-VASS). The latter have the property that the monoid generated by the matrices appearing in their affine transformations is finite. The class of afmp-$\mathbb{Z}$-VASS encompasses classical operations of counter machines such as resets, permutations, transfers and copies. We show that reachability in an afmp-$\mathbb{Z}$-VASS reduces to reachability in a $\mathbb{Z}$-VASS whose control-states grow linearly in the size of the matrix monoid. Our construction shows that reachability relations of afmp-$\mathbb{Z}$-VASS are semilinear, and in particular enables us to show that reachability in $\mathbb{Z}$-VASS with transfers and $\mathbb{Z}$-VASS with copies is PSPACE-complete. We then focus on the reachability problem for affine $\mathbb{Z}$-VASS with monogenic monoids: (possibly infinite) matrix monoids generated by a single matrix. We show that, in a particular case, the reachability problem is decidable for this class, disproving a conjecture about affine $\mathbb{Z}$-VASS with infinite matrix monoids we raised in a preliminary version of this paper. We complement this result by presenting an affine $\mathbb{Z}$-VASS with monogenic matrix monoid and undecidable reachability relation. △ Less

Submitted 19 July, 2021; v1 submitted 26 September, 2019; originally announced September 2019.

Journal ref: Logical Methods in Computer Science, Volume 17, Issue 3 (July 20, 2021) lmcs:5797

Application-oriented strain-hardening engineering of high-manganese steels

Authors: Christian Haase, Franz Roters, Angela Quadfasel

Abstract: The outstanding mechanical properties of high-manganese steels (HMnS) are a result of their high strain-hardenability. That is facilitated by strong suppression of dynamic recovery, predominant planar glide, and the activation of additional deformation mechanisms, such as transformation-induced plasticity (TRIP) and twinning-induced plasticity (TWIP). However, depending on the final application, s… ▽ More The outstanding mechanical properties of high-manganese steels (HMnS) are a result of their high strain-hardenability. That is facilitated by strong suppression of dynamic recovery, predominant planar glide, and the activation of additional deformation mechanisms, such as transformation-induced plasticity (TRIP) and twinning-induced plasticity (TWIP). However, depending on the final application, strongly differing requirements on the mechanical properties of HMnS are of relevance. In order to design HMnS for specific applications, multi-scale material simulation under consideration of the processing conditions that allows for prediction of the final mechanical properties is required, i.e. strain-hardening engineering based on integrated computational materials engineering (ICME). In this work, we present an approach that employs alloy selection by stacking-fault energy calculations, which enables activation/suppression of specific deformation mechanisms. Tailored manufacturing, e.g. by thermo-mechanical treatment, severe plastic deformation or additive manufacturing, provides possibilities to make use of the strain-hardenability during and after processing to define the mechanical properties. A computational approach for alloy and process design will be discussed. △ Less

Submitted 18 September, 2019; originally announced September 2019.

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

Algebraic Hyperbolicity for Surfaces in Toric Threefolds

Authors: Christian Haase, Nathan Ilten

Abstract: Adapting focal loci techniques used by Chiantini and Lopez, we provide lower bounds on the genera of curves contained in very general surfaces in Gorenstein toric threefolds. We illustrate the utility of these bounds by obtaining results on algebraic hyperbolicity of very general surfaces in toric threefolds. Adapting focal loci techniques used by Chiantini and Lopez, we provide lower bounds on the genera of curves contained in very general surfaces in Gorenstein toric threefolds. We illustrate the utility of these bounds by obtaining results on algebraic hyperbolicity of very general surfaces in toric threefolds. △ Less

Submitted 7 December, 2019; v1 submitted 6 March, 2019; originally announced March 2019.

Comments: 24 pages, 5 figures; v2 minor revisions

Report number: BCSim-2018-s09

Thermo-micro-mechanical simulation of bulk metal forming processes

Authors: S. Amir H. Motaman, Konstantin Schacht, Christian Haase, Ulrich Prahl

Abstract: The newly proposed microstructural constitutive model for polycrystal viscoplasticity in cold and warm regimes (Motaman and Prahl, 2019), is implemented as a microstructural solver via user-defined material subroutine in a finite element (FE) software. Addition of the microstructural solver to the default thermal and mechanical solvers of a standard FE package enabled coupled thermo-micro-mechanic… ▽ More The newly proposed microstructural constitutive model for polycrystal viscoplasticity in cold and warm regimes (Motaman and Prahl, 2019), is implemented as a microstructural solver via user-defined material subroutine in a finite element (FE) software. Addition of the microstructural solver to the default thermal and mechanical solvers of a standard FE package enabled coupled thermo-micro-mechanical or thermal-microstructural-mechanical (TMM) simulation of cold and warm bulk metal forming processes. The microstructural solver, which incrementally calculates the evolution of microstructural state variables (MSVs) and their correlation to the thermal and mechanical variables, is implemented based on the constitutive theory of isotropic hypoelasto-viscoplastic (HEVP) finite (large) strain/deformation. The numerical integration and algorithmic procedure of the FE implementation are explained in detail. Then, the viability of this approach is shown for (TMM-) FE simulation of an industrial multistep warm forging. △ Less

Submitted 20 February, 2019; v1 submitted 27 October, 2018; originally announced October 2018.

Journal ref: https://doi.org/10.1016/j.ijsolstr.2019.05.028

Ehrhart-equivalent $\boldsymbol 3$-polytopes are equidecomposable

Authors: Jakob Erbe, Christian Haase, Francisco Santos

Abstract: We show that if two lattice $3$-polytopes $P$ and $P'$ have the same Ehrhart function then they are $\operatorname{GL}_3({\mathbb Z})$-equidecomposable; that is, they can be partitioned into relatively open simplices $U_1,\dots, U_k$ and $U'_1,\dots,U'_k$ such that $U_i$ and $U'_i$ are unimodularly equivalent, for each $i$. We show that if two lattice $3$-polytopes $P$ and $P'$ have the same Ehrhart function then they are $\operatorname{GL}_3({\mathbb Z})$-equidecomposable; that is, they can be partitioned into relatively open simplices $U_1,\dots, U_k$ and $U'_1,\dots,U'_k$ such that $U_i$ and $U'_i$ are unimodularly equivalent, for each $i$. △ Less

Submitted 25 July, 2018; originally announced July 2018.

Comments: 11 pages

MSC Class: 52B10; 52B20; 52B45

Journal ref: Proc. Amer. Math. Soc. 147 (2019), 5373-5383

Levelness of Order Polytopes

Authors: Christian Haase, Florian Kohl, Akiyoshi Tsuchiya

Abstract: Since their introduction by Stanley~\cite{StanleyOrderPoly} order polytopes have been intriguing mathematicians as their geometry can be used to examine (algebraic) properties of finite posets. In this paper, we follow this route to examine the levelness property of order polytopes. The levelness property was also introduced by Stanley~\cite{Stanley-CM-complexes} and it generalizes the Gorenstein… ▽ More Since their introduction by Stanley~\cite{StanleyOrderPoly} order polytopes have been intriguing mathematicians as their geometry can be used to examine (algebraic) properties of finite posets. In this paper, we follow this route to examine the levelness property of order polytopes. The levelness property was also introduced by Stanley~\cite{Stanley-CM-complexes} and it generalizes the Gorenstein property. This property has been recently characterized by Miyazaki~\cite{Miyazaki} for the case of order polytopes. We provide an alternative characterization using weighted digraphs. Using this characterization, we give a new infinite family of level posets and show that determining levelness is in $\operatorname{co-NP}$. This family can be used to create infinitely many examples illustrating that the levelness property can not be characterized by the $h^{\ast}$-vector. We then turn to the more general family of alcoved polytopes. We give a characterization for levelness of alcoved polytopes using the Minkowski sum. Then we study several cases when the product of two polytopes is level. In particular, we provide an example where the product of two level polytopes is not level. △ Less

Submitted 8 May, 2018; originally announced May 2018.

Comments: 30 pages, 7 Figures, comments and feedback very welcome!

MSC Class: 05; 13

Journal ref: SIAM Journal on Discrete Mathematics 34 (2020), 1261--1280

Smooth centrally symmetric polytopes in dimension 3 are IDP

Authors: Matthias Beck, Christian Haase, Akihiro Higashitani, Johannes Hofscheier, Katharina Jochemko, Lukas Katthän, Mateusz Michałek

Abstract: In 1997 Oda conjectured that every smooth lattice polytope has the integer decomposition property. We prove Oda's conjecture for centrally symmetric $3$-dimensional polytopes, by showing they are covered by lattice parallelepipeds and unimodular simplices. In 1997 Oda conjectured that every smooth lattice polytope has the integer decomposition property. We prove Oda's conjecture for centrally symmetric $3$-dimensional polytopes, by showing they are covered by lattice parallelepipeds and unimodular simplices. △ Less

Submitted 4 July, 2018; v1 submitted 3 February, 2018; originally announced February 2018.

Comments: 7 pages, 3 figures; revised version following the helpful comments of the referees

MSC Class: 52B20 (Primary); 52B10; 52B12 (Secondary)

Journal ref: Ann. Comb. 23 (2019), no. 2, 255-262

Influence of deformation and annealing twinning on the microstructure and texture evolution of face-centered cubic high-entropy alloys

Authors: Christian Haase, Luis A Barrales-Mora

Abstract: The influence of the physical mechanisms activated during deformation and annealing on the microstructure and texture evolution as well as on the mechanical properties in the equiatomic CoCrFeMnNi high-entropy alloy (HEA) were investigated. A combination of cold rolling and annealing was used to investigate the HEA in the deformed, recovered, partially recrystallized, and fully recrystallized stat… ▽ More The influence of the physical mechanisms activated during deformation and annealing on the microstructure and texture evolution as well as on the mechanical properties in the equiatomic CoCrFeMnNi high-entropy alloy (HEA) were investigated. A combination of cold rolling and annealing was used to investigate the HEA in the deformed, recovered, partially recrystallized, and fully recrystallized states. Detailed microstructure and texture analysis was performed by electron backscatter diffraction, transmission electron microscopy, and X-ray diffraction. The mechanical properties were evaluated using uniaxial tensile testing. A specific focus of this investigation was put on studying the influence of deformation and annealing twinning on the material behavior. It was substantiated that during cold rolling deformation, twinning facilitates the transition from the Cu-type to the Brass-type texture, whereas annealing-twinning leads to a strong modification of the texture formed during recrystallization. The formation of specific twin orientations and the randomization of the recrystallization texture were proven by experiments as well as by cellular automaton simulations. During tension of the cold-rolled and annealed material high work-hardenability was observed. We attribute this behavior primarily to the dominance of planar dislocation slip and reduced tendency for dynamic recovery, since deformation twinning was observed to activate only in the non-recrystallized grains and thus, contributed minimally to the overall plasticity. The correlation between deformation/annealing twinning and the material behavior was discussed in detail. △ Less

Submitted 5 December, 2017; originally announced December 2017.

Maximum Number of Modes of Gaussian Mixtures

Authors: Carlos Améndola, Alexander Engström, Christian Haase

Abstract: Gaussian mixture models are widely used in Statistics. A fundamental aspect of these distributions is the study of the local maxima of the density, or modes. In particular, it is not known how many modes a mixture of $k$ Gaussians in $d$ dimensions can have. We give a brief account of this problem's history. Then, we give improved lower bounds and the first upper bound on the maximum number of mod… ▽ More Gaussian mixture models are widely used in Statistics. A fundamental aspect of these distributions is the study of the local maxima of the density, or modes. In particular, it is not known how many modes a mixture of $k$ Gaussians in $d$ dimensions can have. We give a brief account of this problem's history. Then, we give improved lower bounds and the first upper bound on the maximum number of modes, provided it is finite. △ Less

Submitted 18 April, 2019; v1 submitted 16 February, 2017; originally announced February 2017.

Comments: 14 pages, 5 figures. Final version, to appear in Information and Inference

MSC Class: 62E10 (primary); 62H05 (secondary)

Discrete Mixed Volume and Hodge-Deligne Numbers

Authors: Sandra Di Rocco, Christian Haase, Benjamin Nill

Abstract: Generalizing the famous Bernstein-Kushnirenko Theorem, Khovanskii proved in 1978 a combinatorial formula for the arithmetic genus of the compactification of a generic complete intersection associated to a family of lattice polytopes. Recently, an analogous combinatorial formula, called the discrete mixed volume, was introduced by Bihan and shown to be nonnegative. By making a footnote of Khovanski… ▽ More Generalizing the famous Bernstein-Kushnirenko Theorem, Khovanskii proved in 1978 a combinatorial formula for the arithmetic genus of the compactification of a generic complete intersection associated to a family of lattice polytopes. Recently, an analogous combinatorial formula, called the discrete mixed volume, was introduced by Bihan and shown to be nonnegative. By making a footnote of Khovanskii in his paper explicit, we interpret this invariant as the (motivic) arithmetic genus of the non-compact generic complete intersection associated to the family of lattice polytopes. △ Less

Submitted 28 September, 2016; originally announced September 2016.

Comments: 7 pages

MSC Class: 52B20 (primary); 14M25; 32S35 (secondary)

The Finiteness Threshold Width of Lattice Polytopes

Authors: Mónica Blanco, Christian Haase, Jan Hofmann, Francisco Santos

Abstract: We prove that in each dimension $d$ there is a constant $w^\infty(d)\in \mathbb{N}$ such that for every $n\in \mathbb{N}$ all but finitely many $d$-polytopes with $n$ lattice points have width at most $w^\infty(d)$. We call $w^\infty(d)$ the finiteness threshold width and show that $d-2 \le w^\infty(d)\le O^*\left( d^{4/3}\right)$. Blanco and Santos determined the value $w^\infty(3)=1$. Here, we… ▽ More We prove that in each dimension $d$ there is a constant $w^\infty(d)\in \mathbb{N}$ such that for every $n\in \mathbb{N}$ all but finitely many $d$-polytopes with $n$ lattice points have width at most $w^\infty(d)$. We call $w^\infty(d)$ the finiteness threshold width and show that $d-2 \le w^\infty(d)\le O^*\left( d^{4/3}\right)$. Blanco and Santos determined the value $w^\infty(3)=1$. Here, we establish $w^\infty(4)=2$. This implies, in particular, that there are only finitely many empty $4$-simplices of width larger than two. The main tool in our proofs is the study of $d$-dimensional lifts of hollow $(d-1)$-polytopes. △ Less

Submitted 4 January, 2021; v1 submitted 4 July, 2016; originally announced July 2016.

Comments: 21 pages, 10 figures; changes from previous version: several edits suggested by anonymous referees; this version has been accepted in Trans. of the Amer. Math. Soc

MSC Class: 52B20; 52B10 ACM Class: G.2.1

Journal ref: Transactions of the Amer. Math. Soc. Ser. B 8 (April 2021), 399-419

A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One

Authors: Stefan Göller, Christoph Haase, Ranko Lazić, Patrick Totzke

Abstract: Branching VASS (BVASS) generalise vector addition systems with states by allowing for special branching transitions that can non-deterministically distribute a counter value between two control states. A run of a BVASS consequently becomes a tree, and reachability is to decide whether a given configuration is the root of a reachability tree. This paper shows P-completeness of reachability in BVASS… ▽ More Branching VASS (BVASS) generalise vector addition systems with states by allowing for special branching transitions that can non-deterministically distribute a counter value between two control states. A run of a BVASS consequently becomes a tree, and reachability is to decide whether a given configuration is the root of a reachability tree. This paper shows P-completeness of reachability in BVASS in dimension one, the first decidability result for reachability in a subclass of BVASS known so far. Moreover, we show that coverability and boundedness in BVASS in dimension one are P-complete as well. △ Less

Submitted 6 May, 2016; v1 submitted 17 February, 2016; originally announced February 2016.

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

Context-Free Commutative Grammars with Integer Counters and Resets

Authors: Dmitry Chistikov, Christoph Haase, Simon Halfon

Abstract: We study the computational complexity of reachability, coverability and inclusion for extensions of context-free commutative grammars with integer counters and reset operations on them. Those grammars can alternatively be viewed as an extension of communication-free Petri nets. Our main results are that reachability and coverability are inter-reducible and both NP-complete. In particular, this cla… ▽ More We study the computational complexity of reachability, coverability and inclusion for extensions of context-free commutative grammars with integer counters and reset operations on them. Those grammars can alternatively be viewed as an extension of communication-free Petri nets. Our main results are that reachability and coverability are inter-reducible and both NP-complete. In particular, this class of commutative grammars enjoys semi-linear reachability sets. We also show that the inclusion problem is, in general, coNEXP-complete and already $Π_2^\text{P}$-complete for grammars with only one non-terminal symbol. Showing the lower bound for the latter result requires us to develop a novel $Π_2^\text{P}$-complete variant of the classic subset sum problem. △ Less

Submitted 24 June, 2016; v1 submitted 16 November, 2015; originally announced November 2015.

Comments: 33 pages

ACM Class: F.1.1

Approaching the Coverability Problem Continuously

Authors: Michael Blondin, Alain Finkel, Christoph Haase, Serge Haddad

Abstract: The coverability problem for Petri nets plays a central role in the verification of concurrent shared-memory programs. However, its high EXPSPACE-complete complexity poses a challenge when encountered in real-world instances. In this paper, we develop a new approach to this problem which is primarily based on applying forward coverability in continuous Petri nets as a pruning criterion inside a ba… ▽ More The coverability problem for Petri nets plays a central role in the verification of concurrent shared-memory programs. However, its high EXPSPACE-complete complexity poses a challenge when encountered in real-world instances. In this paper, we develop a new approach to this problem which is primarily based on applying forward coverability in continuous Petri nets as a pruning criterion inside a backward coverability framework. A cornerstone of our approach is the efficient encoding of a recently developed polynomial-time algorithm for reachability in continuous Petri nets into SMT. We demonstrate the effectiveness of our approach on standard benchmarks from the literature, which shows that our approach decides significantly more instances than any existing tool and is in addition often much faster, in particular on large instances. △ Less

Submitted 9 January, 2016; v1 submitted 19 October, 2015; originally announced October 2015.

Comments: 18 pages, 4 figures

ACM Class: D.2.4; F.1.1

Mixed Ehrhart polynomials

Authors: Christian Haase, Martina Juhnke-Kubitzke, Raman Sanyal, Thorsten Theobald

Abstract: For lattice polytopes $P_1,\ldots, P_k \subseteq \mathbb{R}^d$, Bihan (2014) introduced the discrete mixed volume $\mathrm{DMV}(P_1,\dots,P_k)$ in analogy to the classical mixed volume. In this note we initiate the study of the associated mixed Ehrhart polynomial $\mathrm{ME}_{P_1,\dots,P_k}(n) = \mathrm{DMV}(nP_1,\dots,nP_k)$. We study properties of this polynomial and we give interpretations for… ▽ More For lattice polytopes $P_1,\ldots, P_k \subseteq \mathbb{R}^d$, Bihan (2014) introduced the discrete mixed volume $\mathrm{DMV}(P_1,\dots,P_k)$ in analogy to the classical mixed volume. In this note we initiate the study of the associated mixed Ehrhart polynomial $\mathrm{ME}_{P_1,\dots,P_k}(n) = \mathrm{DMV}(nP_1,\dots,nP_k)$. We study properties of this polynomial and we give interpretations for some of its coefficients in terms of (discrete) mixed volumes. Bihan (2014) showed that the discrete mixed volume is always non-negative. Our investigations yield simpler proofs for certain special cases. We also introduce and study the associated mixed $h^*$-vector. We show that for large enough dilates $r P_1, \ldots, rP_k$ the corresponding mixed $h^*$-polynomial has only real roots and as a consequence the mixed $h^*$-vector becomes non-negative. △ Less

Submitted 9 January, 2017; v1 submitted 8 September, 2015; originally announced September 2015.

Comments: 12 pages

MSC Class: 52B20; 52A39

Tightening the Complexity of Equivalence Problems for Commutative Grammars

Authors: Christoph Haase, Piotr Hofman

Abstract: We show that the language equivalence problem for regular and context-free commutative grammars is coNEXP-complete. In addition, our lower bound immediately yields further coNEXP-completeness results for equivalence problems for communication-free Petri nets and reversal-bounded counter automata. Moreover, we improve both lower and upper bounds for language equivalence for exponent-sensitive commu… ▽ More We show that the language equivalence problem for regular and context-free commutative grammars is coNEXP-complete. In addition, our lower bound immediately yields further coNEXP-completeness results for equivalence problems for communication-free Petri nets and reversal-bounded counter automata. Moreover, we improve both lower and upper bounds for language equivalence for exponent-sensitive commutative grammars. △ Less

Submitted 25 June, 2015; originally announced June 2015.

Comments: 21 pages

ACM Class: F.1.1; F.4.1

Face-subgroups of permutation polytopes

Authors: Christian Haase

Abstract: In [Baumeister, H., Nill, Paffenholz, On permutation polytopes, Adv. Math. 222 (2009), 431-452 / arXiv:0709.1615] we conjectured a characterization of subgroups H of a permutation group G so that, on the level of permutation polytopes, P(H) is a face of P(G). Here we present the embarrassingly simple proof of this conjecture. In [Baumeister, H., Nill, Paffenholz, On permutation polytopes, Adv. Math. 222 (2009), 431-452 / arXiv:0709.1615] we conjectured a characterization of subgroups H of a permutation group G so that, on the level of permutation polytopes, P(H) is a face of P(G). Here we present the embarrassingly simple proof of this conjecture. △ Less

Submitted 2 March, 2015; originally announced March 2015.

Comments: 1 page

MSC Class: 05A05 (Primary); 52B15; 20B35 (Secondary)

The Complexity of the Kth Largest Subset Problem and Related Problems

Authors: Christoph Haase, Stefan Kiefer

Abstract: We show that the Kth largest subset problem and the Kth largest m-tuple problem are in PP and hard for PP under polynomial-time Turing reductions. Several problems from the literature were previously shown NP-hard via reductions from those two problems, and by our main result they become PP-hard as well. We also provide complementary PP-upper bounds for some of them. We show that the Kth largest subset problem and the Kth largest m-tuple problem are in PP and hard for PP under polynomial-time Turing reductions. Several problems from the literature were previously shown NP-hard via reductions from those two problems, and by our main result they become PP-hard as well. We also provide complementary PP-upper bounds for some of them. △ Less

Submitted 30 September, 2015; v1 submitted 27 January, 2015; originally announced January 2015.

ACM Class: F.1.3

Reachability in Two-Dimensional Vector Addition Systems with States is PSPACE-complete

Authors: Michael Blondin, Alain Finkel, Stefan Göller, Christoph Haase, Pierre McKenzie

Abstract: Determining the complexity of the reachability problem for vector addition systems with states (VASS) is a long-standing open problem in computer science. Long known to be decidable, the problem to this day lacks any complexity upper bound whatsoever. In this paper, reachability for two-dimensional VASS is shown PSPACE-complete. This improves on a previously known doubly exponential time bound est… ▽ More Determining the complexity of the reachability problem for vector addition systems with states (VASS) is a long-standing open problem in computer science. Long known to be decidable, the problem to this day lacks any complexity upper bound whatsoever. In this paper, reachability for two-dimensional VASS is shown PSPACE-complete. This improves on a previously known doubly exponential time bound established by Howell, Rosier, Huynh and Yen in 1986. The coverability and boundedness problems are also noted to be PSPACE-complete. In addition, some complexity results are given for the reachability problem in two-dimensional VASS and in integer VASS when numbers are encoded in unary. △ Less

Submitted 13 December, 2014; originally announced December 2014.

Comments: 27 pages, 8 figures

ACM Class: F.1.1; F.1.3

Convex-normal (pairs of) polytopes

Authors: Christian Haase, Jan Hofmann

Abstract: In 2012 Gubeladze (Adv.\ Math.\ 2012) introduced the notion of k-convex-normal polytopes to show that integral polytopes all of whose edges are longer than 4d(d+1) have the integer decomposition property. In the first part of this paper we show that for lattice polytopes there is no difference between k- and (k+1)-convex-normality (for k >= 3) and improve the bound to 2d(d+1). In the second part w… ▽ More In 2012 Gubeladze (Adv.\ Math.\ 2012) introduced the notion of k-convex-normal polytopes to show that integral polytopes all of whose edges are longer than 4d(d+1) have the integer decomposition property. In the first part of this paper we show that for lattice polytopes there is no difference between k- and (k+1)-convex-normality (for k >= 3) and improve the bound to 2d(d+1). In the second part we extend the definition to pairs of polytopes and show that for rational polytopes P and Q, where the normal fan of P is a refinement of the normal fan of Q, if every edge e_P of P is at least d times as long as the corresponding edge e_Q of Q, then (P+Q) \cap \Z^d = (P\cap \Z^d) + (Q \cap \Z^d). △ Less

Submitted 23 October, 2014; originally announced October 2014.

Comments: 10 pages, 8 figures

MSC Class: 52B20

The Odds of Staying on Budget

Authors: Christoph Haase, Stefan Kiefer

Abstract: Given Markov chains and Markov decision processes (MDPs) whose transitions are labelled with non-negative integer costs, we study the computational complexity of deciding whether the probability of paths whose accumulated cost satisfies a Boolean combination of inequalities exceeds a given threshold. For acyclic Markov chains, we show that this problem is PP-complete, whereas it is hard for the Po… ▽ More Given Markov chains and Markov decision processes (MDPs) whose transitions are labelled with non-negative integer costs, we study the computational complexity of deciding whether the probability of paths whose accumulated cost satisfies a Boolean combination of inequalities exceeds a given threshold. For acyclic Markov chains, we show that this problem is PP-complete, whereas it is hard for the PosSLP problem and in PSPACE for general Markov chains. Moreover, for acyclic and general MDPs, we prove PSPACE- and EXP-completeness, respectively. Our results have direct implications on the complexity of computing reward quantiles in succinctly represented stochastic systems. △ Less

Submitted 21 April, 2015; v1 submitted 21 September, 2014; originally announced September 2014.

Comments: Technical report for an ICALP'15 paper. 30 pages, 1 figure

ACM Class: F.1.1

Integer Vector Addition Systems with States

Authors: Christoph Haase, Simon Halfon

Abstract: This paper studies reachability, coverability and inclusion problems for Integer Vector Addition Systems with States (ZVASS) and extensions and restrictions thereof. A ZVASS comprises a finite-state controller with a finite number of counters ranging over the integers. Although it is folklore that reachability in ZVASS is NP-complete, it turns out that despite their naturalness, from a complexity… ▽ More This paper studies reachability, coverability and inclusion problems for Integer Vector Addition Systems with States (ZVASS) and extensions and restrictions thereof. A ZVASS comprises a finite-state controller with a finite number of counters ranging over the integers. Although it is folklore that reachability in ZVASS is NP-complete, it turns out that despite their naturalness, from a complexity point of view this class has received little attention in the literature. We fill this gap by providing an in-depth analysis of the computational complexity of the aforementioned decision problems. Most interestingly, it turns out that while the addition of reset operations to ordinary VASS leads to undecidability and Ackermann-hardness of reachability and coverability, respectively, they can be added to ZVASS while retaining NP-completness of both coverability and reachability. △ Less

Submitted 28 July, 2014; v1 submitted 10 June, 2014; originally announced June 2014.

Comments: 17 pages, 2 figures

ACM Class: F.1.1

Existence of unimodular triangulations - positive results

Authors: Christian Haase, Andreas Paffenholz, Lindsay C. Piechnik, Francisco Santos

Abstract: Unimodular triangulations of lattice polytopes arise in algebraic geometry, commutative algebra, integer programming and, of course, combinatorics. In this article, we review several classes of polytopes that do have unimodular triangulations and constructions that preserve their existence. We include, in particular, the first effective proof of the classical result by Knudsen-Mumford-Waterman… ▽ More Unimodular triangulations of lattice polytopes arise in algebraic geometry, commutative algebra, integer programming and, of course, combinatorics. In this article, we review several classes of polytopes that do have unimodular triangulations and constructions that preserve their existence. We include, in particular, the first effective proof of the classical result by Knudsen-Mumford-Waterman stating that every lattice polytope has a dilation that admits a unimodular triangulation. Our proof yields an explicit (although doubly exponential) bound for the dilation factor. △ Less

Submitted 11 December, 2017; v1 submitted 7 May, 2014; originally announced May 2014.

Comments: 89 pages; changes from v2 and v1: the survey part has been expanded, in particular the section on open questions

MSC Class: 52B10; 52B20

Journal ref: Mem. Amer. Math. Soc. Volume 270, Number 1321, American Math. Society, 2021. ISBNs: 978-1-4704-4716-8 (print); 978-1-4704-6530-8 (online)

Subclasses of Presburger Arithmetic and the Weak EXP Hierarchy

Authors: Christoph Haase

Abstract: It is shown that for any fixed $i>0$, the $Σ_{i+1}$-fragment of Presburger arithmetic, i.e., its restriction to $i+1$ quantifier alternations beginning with an existential quantifier, is complete for $\mathsfΣ^{\mathsf{EXP}}_{i}$, the $i$-th level of the weak EXP hierarchy, an analogue to the polynomial-time hierarchy residing between $\mathsf{NEXP}$ and $\mathsf{EXPSPACE}$. This result completes… ▽ More It is shown that for any fixed $i>0$, the $Σ_{i+1}$-fragment of Presburger arithmetic, i.e., its restriction to $i+1$ quantifier alternations beginning with an existential quantifier, is complete for $\mathsfΣ^{\mathsf{EXP}}_{i}$, the $i$-th level of the weak EXP hierarchy, an analogue to the polynomial-time hierarchy residing between $\mathsf{NEXP}$ and $\mathsf{EXPSPACE}$. This result completes the computational complexity landscape for Presburger arithmetic, a line of research which dates back to the seminal work by Fischer & Rabin in 1974. Moreover, we apply some of the techniques developed in the proof of the lower bound in order to establish bounds on sets of naturals definable in the $Σ_1$-fragment of Presburger arithmetic: given a $Σ_1$-formula $Φ(x)$, it is shown that the set of non-negative solutions is an ultimately periodic set whose period is at most doubly-exponential and that this bound is tight. △ Less

Submitted 12 May, 2014; v1 submitted 21 January, 2014; originally announced January 2014.

Comments: 10 pages, 2 figures

MSC Class: 03B70 ACM Class: F.4.1