Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)
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)
@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} }
Published in: LIPIcs, Volume 289, 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)
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)
@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} }
Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)
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)
@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} }
Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)
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)
@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} }
Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)
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)
@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} }
Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)
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)
@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} }
Published in: LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)
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)
@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} }
Published in: LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)
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)
@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} }
Published in: LIPIcs, Volume 150, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)
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)
@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} }
Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)
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)
@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} }
Published in: LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)
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)
@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} }
Published in: LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)
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)
@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} }
Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)
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)
@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} }
Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)
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)
@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} }
Published in: LIPIcs, Volume 47, 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)
Christoph Haase and Piotr Hofman. Tightening the Complexity of Equivalence Problems for Commutative Grammars. In 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 47, pp. 41:1-41:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@InProceedings{haase_et_al:LIPIcs.STACS.2016.41, author = {Haase, Christoph and Hofman, Piotr}, title = {{Tightening the Complexity of Equivalence Problems for Commutative Grammars}}, booktitle = {33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)}, pages = {41:1--41:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-001-9}, ISSN = {1868-8969}, year = {2016}, volume = {47}, editor = {Ollinger, Nicolas and Vollmer, Heribert}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2016.41}, URN = {urn:nbn:de:0030-drops-57422}, doi = {10.4230/LIPIcs.STACS.2016.41}, annote = {Keywords: language equivalence, commutative grammars, presburger arithmetic, semi-linear sets, petri nets} }
Feedback for Dagstuhl Publishing