16 Search Results for "Haase, Christoph"

Document
Invited Paper
DOI: 10.4230/LIPIcs.FSTTCS.2024.1
An Introduction to the Theory of Linear Integer Arithmetic (Invited Paper)

Authors: Dmitry Chistikov

Published in: LIPIcs, Volume 323, 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)

Abstract
Presburger arithmetic, or linear integer arithmetic (LIA), is a logic that allows one to express linear constraints on integers: equalities, inequalities, and divisibility by nonzero n ∈ ℤ. More formally, it is the first-order theory of integers with addition and ordering. This paper offers a short introduction: what can be expressed in this logical theory, decision problems, and automated reasoning methods. We begin with an elementary introduction, explaining the language of linear arithmetic constraints by examples. We adopt a theoretical perspective, focusing on the decision problem: determining the truth value of a logical sentence. The following three views on Presburger arithmetic give us three effective methods for decision procedures: a view from geometry (using semi-linear sets), from automata theory (using finite automata and recognizable sets), and from symbolic computation (using quantifier elimination). The decision problem for existential formulas of Presburger arithmetic is essentially the feasibility problem of integer linear programming. By a fundamental result due to Borosh and Treybig [Proc. Am. Math. Soc. 55(2), 1976] and Papadimitriou [J. ACM 28(4), 1981], it belongs to the complexity class NP. Echoing the three views discussed above, we sketch three proofs of this result and discuss how these ideas have been used and developed in the recent research literature. This is a companion paper for a conference talk focused on the three views on Presburger arithmetic and their applications. The reader will require background knowledge at the level of undergraduate computer science curricula. The discussion of complexity aspects is more advanced.
Cite as

Dmitry Chistikov. An Introduction to the Theory of Linear Integer Arithmetic (Invited Paper). In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 1:1-1:36, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{chistikov:LIPIcs.FSTTCS.2024.1,
  author =	{Chistikov, Dmitry},
  title =	{{An Introduction to the Theory of Linear Integer Arithmetic}},
  booktitle =	{44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
  pages =	{1:1--1:36},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-355-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{323},
  editor =	{Barman, Siddharth and Lasota, S{\l}awomir},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.1},
  URN =		{urn:nbn:de:0030-drops-221909},
  doi =		{10.4230/LIPIcs.FSTTCS.2024.1},
  annote =	{Keywords: Logical theories of arithmetic, decision procedures}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2024.142
An Efficient Quantifier Elimination Procedure for Presburger Arithmetic

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

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

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

Christoph Haase, Shankara Narayanan Krishna, Khushraj Madnani, Om Swostik Mishra, and Georg Zetzsche. An Efficient Quantifier Elimination Procedure for Presburger Arithmetic. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 142:1-142:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{haase_et_al:LIPIcs.ICALP.2024.142,
  author =	{Haase, Christoph and Krishna, Shankara Narayanan and Madnani, Khushraj and Mishra, Om Swostik and Zetzsche, Georg},
  title =	{{An Efficient Quantifier Elimination Procedure for Presburger Arithmetic}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{142:1--142:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.142},
  URN =		{urn:nbn:de:0030-drops-202856},
  doi =		{10.4230/LIPIcs.ICALP.2024.142},
  annote =	{Keywords: Presburger arithmetic, quantifier elimination, parametric integer programming, convex geometry}
}
Document
DOI: 10.4230/LIPIcs.STACS.2024.29
Semënov Arithmetic, Affine {VASS}, and String Constraints

Authors: Andrei Draghici, Christoph Haase, and Florin Manea

Published in: LIPIcs, Volume 289, 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)

Abstract
We study extensions of Semënov arithmetic, the first-order theory of the structure ⟨ℕ,+,2^x⟩. It is well-known that this theory becomes undecidable when extended with regular predicates over tuples of number strings, such as the Büchi V₂-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 result, we settle an open problem from the literature and show decidability of a class of string constraints involving length constraints.
Cite as

Andrei Draghici, Christoph Haase, and Florin Manea. Semënov Arithmetic, Affine {VASS}, and String Constraints. In 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, pp. 29:1-29:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{draghici_et_al:LIPIcs.STACS.2024.29,
  author =	{Draghici, Andrei and Haase, Christoph and Manea, Florin},
  title =	{{Sem\"{e}nov Arithmetic, Affine \{VASS\}, and String Constraints}},
  booktitle =	{41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)},
  pages =	{29:1--29:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-311-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{289},
  editor =	{Beyersdorff, Olaf and Kant\'{e}, Mamadou Moustapha and Kupferman, Orna and Lokshtanov, Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2024.29},
  URN =		{urn:nbn:de:0030-drops-197393},
  doi =		{10.4230/LIPIcs.STACS.2024.29},
  annote =	{Keywords: arithmetic theories, B\"{u}chi arithmetic, exponentiation, vector addition systems with states, string constraints}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2023.13
Universal Quantification Makes Automatic Structures Hard to Decide

Authors: Christoph Haase and Radosław Piórkowski

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

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 identity ∀x.Φ≡¬(∃x.¬Φ). 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.
Cite as

Christoph Haase and Radosław Piórkowski. Universal Quantification Makes Automatic Structures Hard to Decide. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 13:1-13:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{haase_et_al:LIPIcs.CONCUR.2023.13,
  author =	{Haase, Christoph and Pi\'{o}rkowski, Rados{\l}aw},
  title =	{{Universal Quantification Makes Automatic Structures Hard to Decide}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{13:1--13:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.13},
  URN =		{urn:nbn:de:0030-drops-190075},
  doi =		{10.4230/LIPIcs.CONCUR.2023.13},
  annote =	{Keywords: automatic structures, universal projection, state complexity, tiling problems}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2023.52
On Polynomial-Time Decidability of k-Negations Fragments of FO Theories (Extended Abstract)

Authors: Christoph Haase, Alessio Mansutti, and Amaury Pouly

Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)

Abstract
This paper introduces a generic framework that provides sufficient conditions for guaranteeing polynomial-time decidability of fixed-negation fragments of first-order theories that adhere to certain fixed-parameter tractability requirements. It enables deciding sentences of such theories with arbitrary existential quantification, conjunction and a fixed number of negation symbols in polynomial time. It was recently shown by Nguyen and Pak [SIAM J. Comput. 51(2): 1-31 (2022)] that an even more restricted such fragment of Presburger arithmetic (the first-order theory of the integers with addition and order) is NP-hard. In contrast, by application of our framework, we show that the fixed negation fragment of weak Presburger arithmetic, which drops the order relation from Presburger arithmetic in favour of equality, is decidable in polynomial time.
Cite as

Christoph Haase, Alessio Mansutti, and Amaury Pouly. On Polynomial-Time Decidability of k-Negations Fragments of FO Theories (Extended Abstract). In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 52:1-52:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{haase_et_al:LIPIcs.MFCS.2023.52,
  author =	{Haase, Christoph and Mansutti, Alessio and Pouly, Amaury},
  title =	{{On Polynomial-Time Decidability of k-Negations Fragments of FO Theories (Extended Abstract)}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{52:1--52:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.52},
  URN =		{urn:nbn:de:0030-drops-185869},
  doi =		{10.4230/LIPIcs.MFCS.2023.52},
  annote =	{Keywords: first-order theories, arithmetic theories, fixed-parameter tractability}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2022.33
Higher-Order Quantified Boolean Satisfiability

Authors: Dmitry Chistikov, Christoph Haase, Zahra Hadizadeh, and Alessio Mansutti

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract
The Boolean satisfiability problem plays a central role in computational complexity and is often used as a starting point for showing NP lower bounds. Generalisations such as Succinct SAT, where a Boolean formula is succinctly represented as a Boolean circuit, have been studied in the literature in order to lift the Boolean satisfiability problem to higher complexity classes such as NEXP. While, in theory, iterating this approach yields complete problems for k-NEXP for all k > 0, using such iterations of Succinct SAT is at best tedious when it comes to proving lower bounds. The main contribution of this paper is to show that the Boolean satisfiability problem has another canonical generalisation in terms of higher-order Boolean functions that is arguably more suitable for showing lower bounds beyond NP. We introduce a family of problems HOSAT(k,d), k ≥ 0, d ≥ 1, in which variables are interpreted as Boolean functions of order at most k and there are d quantifier alternations between functions of order exactly k. We show that the unbounded HOSAT problem is TOWER-complete, and that HOSAT(k,d) is complete for the weak k-EXP hierarchy with d alternations for fixed k,d ≥ 1 and d odd. We illustrate the usefulness of HOSAT by characterising the complexity of weak Presburger arithmetic, the first-order theory of the integers with addition and equality but without order. It has been a long-standing open problem whether weak Presburger arithmetic has the same complexity as standard Presburger arithmetic. We answer this question affirmatively, even for the negation-free fragment and the Horn fragment of weak Presburger arithmetic.
Cite as

Dmitry Chistikov, Christoph Haase, Zahra Hadizadeh, and Alessio Mansutti. Higher-Order Quantified Boolean Satisfiability. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 33:1-33:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{chistikov_et_al:LIPIcs.MFCS.2022.33,
  author =	{Chistikov, Dmitry and Haase, Christoph and Hadizadeh, Zahra and Mansutti, Alessio},
  title =	{{Higher-Order Quantified Boolean Satisfiability}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{33:1--33:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.33},
  URN =		{urn:nbn:de:0030-drops-168313},
  doi =		{10.4230/LIPIcs.MFCS.2022.33},
  annote =	{Keywords: Boolean satisfiability problem, higher-order Boolean functions, weak k-EXP hierarchies, non-elementary complexity, Presburger arithmetic}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2021.55
On Deciding Linear Arithmetic Constraints Over p-adic Integers for All Primes

Authors: Christoph Haase and Alessio Mansutti

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

Abstract
Given an existential formula Φ of linear arithmetic over p-adic integers together with valuation constraints, we study the p-universality problem which consists of deciding whether Φ is satisfiable for all primes p, and the analogous problem for the closely related existential theory of Büchi arithmetic. Our main result is a coNEXP upper bound for both problems, together with a matching lower bound for existential Büchi arithmetic. On a technical level, our results are obtained from analysing properties of a certain class of p-automata, finite-state automata whose languages encode sets of tuples of natural numbers.
Cite as

Christoph Haase and Alessio Mansutti. On Deciding Linear Arithmetic Constraints Over p-adic Integers for All Primes. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 55:1-55:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{haase_et_al:LIPIcs.MFCS.2021.55,
  author =	{Haase, Christoph and Mansutti, Alessio},
  title =	{{On Deciding Linear Arithmetic Constraints Over p-adic Integers for All Primes}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{55:1--55:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.55},
  URN =		{urn:nbn:de:0030-drops-144953},
  doi =		{10.4230/LIPIcs.MFCS.2021.55},
  annote =	{Keywords: linear arithmetic, B\"{u}chi arithmetic, p-adic numbers, automatic structures}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2020.115
On the Size of Finite Rational Matrix Semigroups

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

Published in: LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)

Abstract
Let n be a positive integer and M a set of rational n × n-matrices such that M generates a finite multiplicative semigroup. We show that any matrix in the semigroup is a product of matrices in M whose length is at most 2^{n (2 n + 3)} g(n)^{n+1} ∈ 2^{O(n² log n)}, where g(n) is the maximum order of finite groups over rational n × 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.
Cite as

Georgina Bumpus, Christoph Haase, Stefan Kiefer, Paul-Ioan Stoienescu, and Jonathan Tanner. On the Size of Finite Rational Matrix Semigroups. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 115:1-115:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{bumpus_et_al:LIPIcs.ICALP.2020.115,
  author =	{Bumpus, Georgina and Haase, Christoph and Kiefer, Stefan and Stoienescu, Paul-Ioan and Tanner, Jonathan},
  title =	{{On the Size of Finite Rational Matrix Semigroups}},
  booktitle =	{47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
  pages =	{115:1--115:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-138-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{168},
  editor =	{Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.115},
  URN =		{urn:nbn:de:0030-drops-125226},
  doi =		{10.4230/LIPIcs.ICALP.2020.115},
  annote =	{Keywords: Matrix semigroups, Burnside problem, weighted automata, vector addition systems}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2020.119
On the Power of Ordering in Linear Arithmetic Theories

Authors: Dmitry Chistikov and Christoph Haase

Published in: LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)

Abstract
We study the problems of deciding whether a relation definable by a first-order formula in linear rational or linear integer arithmetic with an order relation is definable in absence of the order relation. Over the integers, this problem was shown decidable by Choffrut and Frigeri [Discret. Math. Theor. C., 12(1), pp. 21 - 38, 2010], albeit with non-elementary time complexity. Our contribution is to establish a full geometric characterisation of those sets definable without order which in turn enables us to prove coNP-completeness of this problem over the rationals and to establish an elementary upper bound over the integers. We also provide a complementary Π₂^P lower bound for the integer case that holds even in a fixed dimension. This lower bound is obtained by showing that universality for ultimately periodic sets, i.e., semilinear sets in dimension one, is Π₂^P-hard, which resolves an open problem of Huynh [Elektron. Inf.verarb. Kybern., 18(6), pp. 291 - 338, 1982].
Cite as

Dmitry Chistikov and Christoph Haase. On the Power of Ordering in Linear Arithmetic Theories. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 119:1-119:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{chistikov_et_al:LIPIcs.ICALP.2020.119,
  author =	{Chistikov, Dmitry and Haase, Christoph},
  title =	{{On the Power of Ordering in Linear Arithmetic Theories}},
  booktitle =	{47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
  pages =	{119:1--119:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-138-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{168},
  editor =	{Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.119},
  URN =		{urn:nbn:de:0030-drops-125265},
  doi =		{10.4230/LIPIcs.ICALP.2020.119},
  annote =	{Keywords: logical definability, linear arithmetic theories, semi linear sets, ultimately periodic sets, numerical semigroups}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2019.31
Concurrent Parameterized Games

Authors: Nathalie Bertrand, Patricia Bouyer, and Anirban Majumdar

Published in: LIPIcs, Volume 150, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)

Abstract
Traditional concurrent games on graphs involve a fixed number of players, who take decisions simultaneously, determining the next state of the game. In this paper, we introduce a parameterized variant of concurrent games on graphs, where the parameter is precisely the number of players. Parameterized concurrent games are described by finite graphs, in which the transitions bear regular languages to describe the possible move combinations that lead from one vertex to another. We consider the problem of determining whether the first player, say Eve, has a strategy to ensure a reachability objective against any strategy profile of her opponents as a coalition. In particular Eve’s strategy should be independent of the number of opponents she actually has. Technically, this paper focuses on an a priori simpler setting where the languages labeling transitions only constrain the number of opponents (but not their precise action choices). These constraints are described as semilinear sets, finite unions of intervals, or intervals. We establish the precise complexities of the parameterized reachability game problem, ranging from PTIME-complete to PSPACE-complete, in a variety of situations depending on the contraints (semilinear predicates, unions of intervals, or intervals) and on the presence or not of non-determinism.
Cite as

Nathalie Bertrand, Patricia Bouyer, and Anirban Majumdar. Concurrent Parameterized Games. In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 31:1-31:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{bertrand_et_al:LIPIcs.FSTTCS.2019.31,
  author =	{Bertrand, Nathalie and Bouyer, Patricia and Majumdar, Anirban},
  title =	{{Concurrent Parameterized Games}},
  booktitle =	{39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)},
  pages =	{31:1--31:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-131-3},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{150},
  editor =	{Chattopadhyay, Arkadev and Gastin, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2019.31},
  URN =		{urn:nbn:de:0030-drops-115931},
  doi =		{10.4230/LIPIcs.FSTTCS.2019.31},
  annote =	{Keywords: concurrent games, parameterized verification}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2018.14
Affine Extensions of Integer Vector Addition Systems with States

Authors: Michael Blondin, Christoph Haase, and Filip Mazowiecki

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Abstract
We study the reachability problem for affine 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 Z-VASS with the finite-monoid property (afmp-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-Z-VASS encompasses classical operations of counter machines such as resets, permutations, transfers and copies. We show that reachability in an afmp-Z-VASS reduces to reachability in a Z-VASS whose control-states grow polynomially in the size of the matrix monoid. Our construction shows that reachability relations of afmp-Z-VASS are semilinear, and in particular enables us to show that reachability in Z-VASS with transfers and Z-VASS with copies is PSPACE-complete.
Cite as

Michael Blondin, Christoph Haase, and Filip Mazowiecki. Affine Extensions of Integer Vector Addition Systems with States. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{blondin_et_al:LIPIcs.CONCUR.2018.14,
  author =	{Blondin, Michael and Haase, Christoph and Mazowiecki, Filip},
  title =	{{Affine Extensions of Integer Vector Addition Systems with States}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{14:1--14:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.14},
  URN =		{urn:nbn:de:0030-drops-95520},
  doi =		{10.4230/LIPIcs.CONCUR.2018.14},
  annote =	{Keywords: Vector addition systems, affine transformations, reachability, semilinear sets, computational complexity}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2017.12
Counting Problems for Parikh Images

Authors: Christoph Haase, Stefan Kiefer, and Markus Lohrey

Published in: LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

Abstract
Given finite-state automata (or context-free grammars) A,B over the same alphabet and a Parikh vector p, we study the complexity of deciding whether the number of words in the language of A with Parikh image p is greater than the number of such words in the language of B. Recently, this problem turned out to be tightly related to the cost problem for weighted Markov chains. We classify the complexity according to whether A and B are deterministic, the size of the alphabet, and the encoding of p (binary or unary).
Cite as

Christoph Haase, Stefan Kiefer, and Markus Lohrey. Counting Problems for Parikh Images. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 12:1-12:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{haase_et_al:LIPIcs.MFCS.2017.12,
  author =	{Haase, Christoph and Kiefer, Stefan and Lohrey, Markus},
  title =	{{Counting Problems for Parikh Images}},
  booktitle =	{42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)},
  pages =	{12:1--12:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-046-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{83},
  editor =	{Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.12},
  URN =		{urn:nbn:de:0030-drops-80597},
  doi =		{10.4230/LIPIcs.MFCS.2017.12},
  annote =	{Keywords: Parikh images, finite automata, counting problems}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2017.94
On the Complexity of Quantified Integer Programming

Authors: Dmitry Chistikov and Christoph Haase

Published in: LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)

Abstract
Quantified integer programming is the problem of deciding assertions of the form Q_k x_k ... forall x_2 exists x_1 : A * x >= c where vectors of variables x_k,..,x_1 form the vector x, all variables are interpreted over N (alternatively, over Z), and A and c are a matrix and vector over Z of appropriate sizes. We show in this paper that quantified integer programming with alternation depth k is complete for the kth level of the polynomial hierarchy.
Cite as

Dmitry Chistikov and Christoph Haase. On the Complexity of Quantified Integer Programming. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 94:1-94:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{chistikov_et_al:LIPIcs.ICALP.2017.94,
  author =	{Chistikov, Dmitry and Haase, Christoph},
  title =	{{On the Complexity of Quantified Integer Programming}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{94:1--94:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-041-5},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{80},
  editor =	{Chatzigiannakis, Ioannis and Indyk, Piotr and Kuhn, Fabian and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.94},
  URN =		{urn:nbn:de:0030-drops-75024},
  doi =		{10.4230/LIPIcs.ICALP.2017.94},
  annote =	{Keywords: integer programming, semi-linear sets, Presburger arithmetic, quantifier elimination}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2016.105
A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One

Authors: Stefan Göller, Christoph Haase, Ranko Lazic, and Patrick Totzke

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

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

Stefan Göller, Christoph Haase, Ranko Lazic, and Patrick Totzke. A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 105:1-105:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{goller_et_al:LIPIcs.ICALP.2016.105,
  author =	{G\"{o}ller, Stefan and Haase, Christoph and Lazic, Ranko and Totzke, Patrick},
  title =	{{A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{105:1--105:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.105},
  URN =		{urn:nbn:de:0030-drops-62409},
  doi =		{10.4230/LIPIcs.ICALP.2016.105},
  annote =	{Keywords: branching vector addition systems, reachability, coverability, boundedness}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2016.128
The Taming of the Semi-Linear Set

Authors: Dmitry Chistikov and Christoph Haase

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

Abstract
Semi-linear sets, which are rational subsets of the monoid (Z^d,+), have numerous applications in theoretical computer science. Although semi-linear sets are usually given implicitly, by formulas in Presburger arithmetic or by other means, the effect of Boolean operations on semi-linear sets in terms of the size of description has primarily been studied for explicit representations. In this paper, we develop a framework suitable for implicitly presented semi-linear sets, in which the size of a semi-linear set is characterized by its norm—the maximal magnitude of a generator. We put together a toolbox of operations and decompositions for semi-linear sets which gives bounds in terms of the norm (as opposed to just the bit-size of the description), a unified presentation, and simplified proofs. This toolbox, in particular, provides exponentially better bounds for the complement and set-theoretic difference. We also obtain bounds on unambiguous decompositions and, as an application of the toolbox, settle the complexity of the equivalence problem for exponent-sensitive commutative grammars.
Cite as

Dmitry Chistikov and Christoph Haase. The Taming of the Semi-Linear Set. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 128:1-128:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{chistikov_et_al:LIPIcs.ICALP.2016.128,
  author =	{Chistikov, Dmitry and Haase, Christoph},
  title =	{{The Taming of the Semi-Linear Set}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{128:1--128:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.128},
  URN =		{urn:nbn:de:0030-drops-62636},
  doi =		{10.4230/LIPIcs.ICALP.2016.128},
  annote =	{Keywords: semi-linear sets, convex polyhedra, triangulations, integer linear programming, commutative grammars}
}
  • Refine by Author
  • 14 Haase, Christoph
  • 5 Chistikov, Dmitry
  • 3 Mansutti, Alessio
  • 2 Kiefer, Stefan
  • 1 Bertrand, Nathalie
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 3 Presburger arithmetic
  • 3 semi-linear sets
  • 2 Büchi arithmetic
  • 2 arithmetic theories
  • 2 automatic structures
  • Show More...

  • Refine by Type
  • 16 document

  • Refine by Publication Year
  • 3 2016
  • 3 2024
  • 2 2017
  • 2 2020
  • 2 2023
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact