35 citations · 169 across the 13 of their papers we have counts for
15 papers
Integer Programming with GCD Constraints
Rémy Defossez, Christoph Haase, Alessio Mansutti +1
We study the non-linear extension of integer programming with greatest common divisor constraints of the form , where and are linear polynomials, is a…
Semënov Arithmetic, Affine VASS, and String Constraints
Andrei Draghici, Christoph Haase, Florin Manea
We study extensions of Semënov arithmetic, the first-order theory of the structure . It is well-knonw that this theory becomes undecidable when extended with…
Universal quantification makes automatic structures hard to decide
Christoph Haase, Radoslaw Piórkowski
Automatic structures are first-order structures whose universe and relations can be represented as regular languages. It follows from the standard closure properties of regular lan…
Affine Extensions of Integer Vector Addition Systems with States
Michael Blondin, Christoph Haase, Filip Mazowiecki +1
We study the reachability problem for affine -VASS, which are integer vector addition systems with states in which transitions perform affine transformations on the cou…
A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One
Stefan Göller, Christoph Haase, Ranko Lazić +1
Branching VASS (BVASS) generalise vector addition systems with states by allowing for special branching transitions that can non-deterministically distribute a counter value betwee…
Efficient Quantile Computation in Markov Chains via Counting Problems for Parikh Images
Christoph Haase, Stefan Kiefer, Markus Lohrey
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…
Context-Free Commutative Grammars with Integer Counters and Resets
Dmitry Chistikov, Christoph Haase, Simon Halfon
We study the computational complexity of reachability, coverability and inclusion for extensions of context-free commutative grammars with integer counters and reset operations on…
Approaching the Coverability Problem Continuously
Michael Blondin, Alain Finkel, Christoph Haase +1
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 challe…
Tightening the Complexity of Equivalence Problems for Commutative Grammars
Christoph Haase, Piotr Hofman
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-c…
The Complexity of the Kth Largest Subset Problem and Related Problems
Christoph Haase, Stefan Kiefer
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 literat…
Reachability in Two-Dimensional Vector Addition Systems with States is PSPACE-complete
Michael Blondin, Alain Finkel, Stefan Göller +2
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 decidabl…
The Odds of Staying on Budget
Christoph Haase, Stefan Kiefer
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 t…
Integer Vector Addition Systems with States
Christoph Haase, Simon Halfon
This paper studies reachability, coverability and inclusion problems for Integer Vector Addition Systems with States (ZVASS) and extensions and restrictions thereof. A ZVASS compri…
Subclasses of Presburger Arithmetic and the Weak EXP Hierarchy
Christoph Haase
It is shown that for any fixed , the -fragment of Presburger arithmetic, i.e., its restriction to quantifier alternations beginning with an existential quantifi…
The Power of Priority Channel Systems
Christoph Haase, Sylvain Schmitz, Philippe Schnoebelen
We introduce Priority Channel Systems, a new class of channel systems where messages carry a numeric priority and where higher-priority messages can supersede lower-priority messag…