Search Results

Documents authored by Michielini, Vincent

Document
DOI: 10.4230/LIPIcs.LICS.2026.19
Reachability in VASS Extended with Integer Counters

Authors: Clotilde Bizière, Wojciech Czerwiński, Roland Guttenberg, Jérôme Leroux, Vincent Michielini, Łukasz Orlikowski, Antoni Puch, and Henry Sinclair-Banks

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

Abstract
We consider a variant of VASS extended with integer counters, denoted VASS+ℤ. These are automata equipped with ℕ- and ℤ-counters; the ℕ-counters are required to remain nonnegative and the ℤ-counters do not have this restriction. We study the complexity of the reachability problem for VASS+ℤ when the number of ℕ-counters is fixed. We show that reachability is NP-complete in 1-VASS+ℤ (i.e. when there is only one ℕ-counter) regardless of unary or binary encoding. For d ≥ 2, using a KLMST-based algorithm, we prove that reachability in d-VASS+ℤ lies in the complexity class ℱ_{d+2}. Our upper bound improves on the naively obtained Ackermannian complexity by simulating the ℤ-counters with ℕ-counters. To complement our upper bounds, we show that extending VASS with integer counters significantly lowers the number of ℕ-counters needed to exhibit hardness. We prove that reachability in unary 2-VASS+ℤ is PSpace-hard; without ℤ-counters this lower bound is only known in dimension 5. We also prove that reachability in unary 3-VASS+ℤ is Tower-hard. Without ℤ-counters, reachability in 3-VASS has elementary complexity and Tower-hardness is only known in dimension 8.
Cite as

Clotilde Bizière, Wojciech Czerwiński, Roland Guttenberg, Jérôme Leroux, Vincent Michielini, Łukasz Orlikowski, Antoni Puch, and Henry Sinclair-Banks. Reachability in VASS Extended with Integer Counters. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 19:1-19:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{biziere_et_al:LIPIcs.LICS.2026.19,
  author =	{Bizi\`{e}re, Clotilde and Czerwi\'{n}ski, Wojciech and Guttenberg, Roland and Leroux, J\'{e}r\^{o}me and Michielini, Vincent and Orlikowski, {\L}ukasz and Puch, Antoni and Sinclair-Banks, Henry},
  title =	{{Reachability in VASS Extended with Integer Counters}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{19:1--19:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.19},
  URN =		{urn:nbn:de:0030-drops-268061},
  doi =		{10.4230/LIPIcs.LICS.2026.19},
  annote =	{Keywords: vector addition systems, Petri nets, counter automata, reachability}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2020.69
Regular Choice Functions and Uniformisations For countable Domains

Authors: Vincent Michielini and Michał Skrzypczak

Published in: LIPIcs, Volume 170, 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)

Abstract
We view languages of words over a product alphabet A x B as relations between words over A and words over B. This leads to the notion of regular relations - relations given by a regular language. We ask when it is possible to find regular uniformisations of regular relations. The answer depends on the structure or shape of the underlying model: it is true e.g. for ω-words, while false for words over ℤ or for infinite trees. In this paper we focus on countable orders. Our main result characterises, which countable linear orders D have the property that every regular relation between words over D has a regular uniformisation. As it turns out, the only obstacle for uniformisability is the one displayed in the case of ℤ - non-trivial automorphisms of the given structure. Thus, we show that either all regular relations over D have regular uniformisations, or there is a non-trivial automorphism of D and even the simple relation of choice cannot be uniformised. Moreover, this dichotomy is effective.
Cite as

Vincent Michielini and Michał Skrzypczak. Regular Choice Functions and Uniformisations For countable Domains. In 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 170, pp. 69:1-69:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{michielini_et_al:LIPIcs.MFCS.2020.69,
  author =	{Michielini, Vincent and Skrzypczak, Micha{\l}},
  title =	{{Regular Choice Functions and Uniformisations For countable Domains}},
  booktitle =	{45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)},
  pages =	{69:1--69:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-159-7},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{170},
  editor =	{Esparza, Javier and Kr\'{a}l', Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2020.69},
  URN =		{urn:nbn:de:0030-drops-127386},
  doi =		{10.4230/LIPIcs.MFCS.2020.69},
  annote =	{Keywords: Uniformisation, Monadic Second-order logic, Countable words}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2019.61
Uniformisation Gives the Full Strength of Regular Languages

Authors: Nathan Lhote, Vincent Michielini, and Michał Skrzypczak

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)

Abstract
Given R a binary relation between words (which we treat as a language over a product alphabet AxB), a uniformisation of it is another relation L included in R which chooses a single word over B, for each word over A whenever there exists one. It is known that MSO, the full class of regular languages, is strong enough to define a uniformisation for each of its relations. The quest of this work is to see which other formalisms, weaker than MSO, also have this property. In this paper, we solve this problem for pseudo-varieties of semigroups: we show that no nonempty pseudo-variety weaker than MSO can provide uniformisations for its relations.
Cite as

Nathan Lhote, Vincent Michielini, and Michał Skrzypczak. Uniformisation Gives the Full Strength of Regular Languages. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 61:1-61:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{lhote_et_al:LIPIcs.MFCS.2019.61,
  author =	{Lhote, Nathan and Michielini, Vincent and Skrzypczak, Micha{\l}},
  title =	{{Uniformisation Gives the Full Strength of Regular Languages}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{61:1--61:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.61},
  URN =		{urn:nbn:de:0030-drops-110053},
  doi =		{10.4230/LIPIcs.MFCS.2019.61},
  annote =	{Keywords: pseudo-variety, finite word, semigroup, uniformisation, regular language}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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