Search Results

Documents authored by Czerwinski, Wojciech

Found 2 Possible Name Variants:

Czerwinski, Wojciech

Document
Invited Paper
DOI: 10.4230/LIPIcs.MFCS.2024.2
Challenges of the Reachability Problem in Infinite-State Systems (Invited Paper)

Authors: Wojciech Czerwiński

Published in: LIPIcs, Volume 306, 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)

Abstract
The reachability problem is a central problem for various infinite state systems like automata with pushdown, with different kinds of counters or combinations thereof. Despite its centrality and decades of research the community still lacks a lot of answers for fundamental and basic questions of that type. I briefly describe my personal viewpoint on the current state of art and emphasise interesting directions, which are worth investigating in my opinion. I also formulate several easy to formulate and understand challenges, which might be pretty hard to solve but at the same time illustrate fundamental lack of our understanding in the area.
Cite as

Wojciech Czerwiński. Challenges of the Reachability Problem in Infinite-State Systems (Invited Paper). In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 2:1-2:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{czerwinski:LIPIcs.MFCS.2024.2,
  author =	{Czerwi\'{n}ski, Wojciech},
  title =	{{Challenges of the Reachability Problem in Infinite-State Systems}},
  booktitle =	{49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)},
  pages =	{2:1--2:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-335-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{306},
  editor =	{Kr\'{a}lovi\v{c}, Rastislav and Ku\v{c}era, Anton{\'\i}n},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2024.2},
  URN =		{urn:nbn:de:0030-drops-205582},
  doi =		{10.4230/LIPIcs.MFCS.2024.2},
  annote =	{Keywords: reachability problem, infinite-state systems, vector addition systems, pushdown}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2023.16
Acyclic Petri and Workflow Nets with Resets

Authors: Dmitry Chistikov, Wojciech Czerwiński, Piotr Hofman, Filip Mazowiecki, and Henry Sinclair-Banks

Published in: LIPIcs, Volume 284, 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)

Abstract
In this paper we propose two new subclasses of Petri nets with resets, for which the reachability and coverability problems become tractable. Namely, we add an acyclicity condition that only applies to the consumptions and productions, not the resets. The first class is acyclic Petri nets with resets, and we show that coverability is PSPACE-complete for them. This contrasts the known Ackermann-hardness for coverability in (not necessarily acyclic) Petri nets with resets. We prove that the reachability problem remains undecidable for acyclic Petri nets with resets. The second class concerns workflow nets, a practically motivated and natural subclass of Petri nets. Here, we show that both coverability and reachability in acyclic workflow nets with resets are PSPACE-complete. Without the acyclicity condition, reachability and coverability in workflow nets with resets are known to be equally hard as for Petri nets with resets, that being Ackermann-hard and undecidable, respectively.
Cite as

Dmitry Chistikov, Wojciech Czerwiński, Piotr Hofman, Filip Mazowiecki, and Henry Sinclair-Banks. Acyclic Petri and Workflow Nets with Resets. In 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 284, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{chistikov_et_al:LIPIcs.FSTTCS.2023.16,
  author =	{Chistikov, Dmitry and Czerwi\'{n}ski, Wojciech and Hofman, Piotr and Mazowiecki, Filip and Sinclair-Banks, Henry},
  title =	{{Acyclic Petri and Workflow Nets with Resets}},
  booktitle =	{43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)},
  pages =	{16:1--16:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-304-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{284},
  editor =	{Bouyer, Patricia and Srinivasan, Srikanth},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2023.16},
  URN =		{urn:nbn:de:0030-drops-193892},
  doi =		{10.4230/LIPIcs.FSTTCS.2023.16},
  annote =	{Keywords: Petri nets, Workflow Nets, Resets, Acyclic, Reachability, Coverability}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2023.22
Languages Given by Finite Automata over the Unary Alphabet

Authors: Wojciech Czerwiński, Maciej Dębski, Tomasz Gogasz, Gordon Hoi, Sanjay Jain, Michał Skrzypczak, Frank Stephan, and Christopher Tan

Published in: LIPIcs, Volume 284, 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)

Abstract
This paper studies the complexity of operations on finite automata and the complexity of their decision problems when the alphabet is unary and n the number of states of the finite automata considered. The following main results are obtained: 1) Equality and inclusion of NFAs can be decided within time 2^O((n log n)^{1/3}); previous upper bound 2^O((n log n)^{1/2}) was by Chrobak (1986) via DFA conversion. 2) The state complexity of operations of UFAs (unambiguous finite automata) increases for complementation and union at most by quasipolynomial; however, for concatenation of two n-state UFAs, the worst case is an UFA of at least 2^Ω(n^{1/6}) states. Previously the upper bounds for complementation and union were exponential-type and this lower bound for concatenation is new.
Cite as

Wojciech Czerwiński, Maciej Dębski, Tomasz Gogasz, Gordon Hoi, Sanjay Jain, Michał Skrzypczak, Frank Stephan, and Christopher Tan. Languages Given by Finite Automata over the Unary Alphabet. In 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 284, pp. 22:1-22:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.FSTTCS.2023.22,
  author =	{Czerwi\'{n}ski, Wojciech and D\k{e}bski, Maciej and Gogasz, Tomasz and Hoi, Gordon and Jain, Sanjay and Skrzypczak, Micha{\l} and Stephan, Frank and Tan, Christopher},
  title =	{{Languages Given by Finite Automata over the Unary Alphabet}},
  booktitle =	{43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)},
  pages =	{22:1--22:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-304-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{284},
  editor =	{Bouyer, Patricia and Srinivasan, Srikanth},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2023.22},
  URN =		{urn:nbn:de:0030-drops-193959},
  doi =		{10.4230/LIPIcs.FSTTCS.2023.22},
  annote =	{Keywords: Nondeterministic Finite Automata, Unambiguous Finite Automata, Upper Bounds on Runtime, Conditional Lower Bounds, Languages over the Unary Alphabet}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2023.35
New Lower Bounds for Reachability in Vector Addition Systems

Authors: Wojciech Czerwiński, Ismaël Jecker, Sławomir Lasota, Jérôme Leroux, and Łukasz Orlikowski

Published in: LIPIcs, Volume 284, 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)

Abstract
We investigate the dimension-parametric complexity of the reachability problem in vector addition systems with states (VASS) and its extension with pushdown stack (pushdown VASS). Up to now, the problem is known to be F_d-hard for VASS of dimension 3d+2 (the complexity class F_d corresponds to the kth level of the fast-growing hierarchy), and no essentially better bound is known for pushdown VASS. We provide a new construction that improves the lower bound for VASS: F_d-hardness in dimension 2d+3. Furthermore, building on our new insights we show a new lower bound for pushdown VASS: F_d-hardness in dimension d/2 + 6. This dimension-parametric lower bound is strictly stronger than the upper bound for VASS, which suggests that the (still unknown) complexity of the reachability problem in pushdown VASS is higher than in plain VASS (where it is Ackermann-complete).
Cite as

Wojciech Czerwiński, Ismaël Jecker, Sławomir Lasota, Jérôme Leroux, and Łukasz Orlikowski. New Lower Bounds for Reachability in Vector Addition Systems. In 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 284, pp. 35:1-35:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.FSTTCS.2023.35,
  author =	{Czerwi\'{n}ski, Wojciech and Jecker, Isma\"{e}l and Lasota, S{\l}awomir and Leroux, J\'{e}r\^{o}me and Orlikowski, {\L}ukasz},
  title =	{{New Lower Bounds for Reachability in Vector Addition Systems}},
  booktitle =	{43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)},
  pages =	{35:1--35:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-304-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{284},
  editor =	{Bouyer, Patricia and Srinivasan, Srikanth},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2023.35},
  URN =		{urn:nbn:de:0030-drops-194088},
  doi =		{10.4230/LIPIcs.FSTTCS.2023.35},
  annote =	{Keywords: vector addition systems, reachability problem, pushdown vector addition system, lower bounds}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CONCUR.2022.5
Involved VASS Zoo (Invited Talk)

Authors: Wojciech Czerwiński

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract
We briefly describe recent advances on understanding the complexity of the reachability problem for vector addition systems (or equivalently for vector addition systems with states - VASSes). We present a zoo of a few involved VASS examples, which illustrate various aspects of hardness of VASSes and various techniques of proving lower complexity bounds.
Cite as

Wojciech Czerwiński. Involved VASS Zoo (Invited Talk). In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 5:1-5:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{czerwinski:LIPIcs.CONCUR.2022.5,
  author =	{Czerwi\'{n}ski, Wojciech},
  title =	{{Involved VASS Zoo}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{5:1--5:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir 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.CONCUR.2022.5},
  URN =		{urn:nbn:de:0030-drops-170681},
  doi =		{10.4230/LIPIcs.CONCUR.2022.5},
  annote =	{Keywords: vector addition systems, reachability problem, low dimensions, examples}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2022.16
Language Inclusion for Boundedly-Ambiguous Vector Addition Systems Is Decidable

Authors: Wojciech Czerwiński and Piotr Hofman

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract
We consider the problems of language inclusion and language equivalence for Vector Addition Systems with States (VASSes) with the acceptance condition defined by the set of accepting states (and more generally by some upward-closed conditions). In general the problem of language equivalence is undecidable even for one-dimensional VASSes, thus to get decidability we investigate restricted subclasses. On one hand we show that the problem of language inclusion of a VASS in k-ambiguous VASS (for any natural k) is decidable and even in Ackermann. On the other hand we prove that the language equivalence problem is Ackermann-hard already for deterministic VASSes. These two results imply Ackermann-completeness for language inclusion and equivalence in several possible restrictions. Some of our techniques can be also applied in much broader generality in infinite-state systems, namely for some subclass of well-structured transition systems.
Cite as

Wojciech Czerwiński and Piotr Hofman. Language Inclusion for Boundedly-Ambiguous Vector Addition Systems Is Decidable. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 16:1-16:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.CONCUR.2022.16,
  author =	{Czerwi\'{n}ski, Wojciech and Hofman, Piotr},
  title =	{{Language Inclusion for Boundedly-Ambiguous Vector Addition Systems Is Decidable}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{16:1--16:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir 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.CONCUR.2022.16},
  URN =		{urn:nbn:de:0030-drops-170796},
  doi =		{10.4230/LIPIcs.CONCUR.2022.16},
  annote =	{Keywords: vector addition systems, language inclusion, language equivalence, determinism, unambiguity, bounded ambiguity, Petri nets, well-structured transition systems}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2021.128
Improved Lower Bounds for Reachability in Vector Addition Systems

Authors: Wojciech Czerwiński, Sławomir Lasota, and Łukasz Orlikowski

Published in: LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)

Abstract
We investigate computational complexity of the reachability problem for vector addition systems (or, equivalently, Petri nets), the central algorithmic problem in verification of concurrent systems. Concerning its complexity, after 40 years of stagnation, a non-elementary lower bound has been shown recently: the problem needs a tower of exponentials of time or space, where the height of tower is linear in the input size. We improve on this lower bound, by increasing the height of tower from linear to exponential. As a side-effect, we obtain better lower bounds for vector addition systems of fixed dimension.
Cite as

Wojciech Czerwiński, Sławomir Lasota, and Łukasz Orlikowski. Improved Lower Bounds for Reachability in Vector Addition Systems. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 128:1-128:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.ICALP.2021.128,
  author =	{Czerwi\'{n}ski, Wojciech and Lasota, S{\l}awomir and Orlikowski, {\L}ukasz},
  title =	{{Improved Lower Bounds for Reachability in Vector Addition Systems}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{128:1--128:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.128},
  URN =		{urn:nbn:de:0030-drops-141973},
  doi =		{10.4230/LIPIcs.ICALP.2021.128},
  annote =	{Keywords: Petri nets, vector addition systems, reachability problem}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2021.129
New Techniques for Universality in Unambiguous Register Automata

Authors: Wojciech Czerwiński, Antoine Mottet, and Karin Quaas

Published in: LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)

Abstract
Register automata are finite automata equipped with a finite set of registers ranging over the domain of some relational structure like (ℕ; =) or (ℚ; <). Register automata process words over the domain, and along a run of the automaton, the registers can store data from the input word for later comparisons. It is long known that the universality problem, i.e., the problem to decide whether a given register automaton accepts all words over the domain, is undecidable. Recently, we proved the problem to be decidable in 2-ExpSpace if the register automaton under study is over (ℕ; =) and unambiguous, i.e., every input word has at most one accepting run; this result was shortly after improved to 2-ExpTime by Barloy and Clemente. In this paper, we go one step further and prove that the problem is in ExpSpace, and in PSpace if the number of registers is fixed. Our proof is based on new techniques that additionally allow us to show that the problem is in PSpace for single-register automata over (ℚ; <). As a third technical contribution we prove that the problem is decidable (in ExpSpace) for a more expressive model of unambiguous register automata, where the registers can take values nondeterministically, if defined over (ℕ; =) and only one register is used.
Cite as

Wojciech Czerwiński, Antoine Mottet, and Karin Quaas. New Techniques for Universality in Unambiguous Register Automata. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 129:1-129:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.ICALP.2021.129,
  author =	{Czerwi\'{n}ski, Wojciech and Mottet, Antoine and Quaas, Karin},
  title =	{{New Techniques for Universality in Unambiguous Register Automata}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{129:1--129:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.129},
  URN =		{urn:nbn:de:0030-drops-141983},
  doi =		{10.4230/LIPIcs.ICALP.2021.129},
  annote =	{Keywords: Register Automata, Data Languages, Unambiguity, Unambiguous, Universality, Containment, Language Inclusion, Equivalence}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.36
Universality Problem for Unambiguous VASS

Authors: Wojciech Czerwiński, Diego Figueira, and Piotr Hofman

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
We study languages of unambiguous VASS, that is, Vector Addition Systems with States, whose transitions read letters from a finite alphabet, and whose acceptance condition is defined by a set of final states (i.e., the coverability language). We show that the problem of universality for unambiguous VASS is ExpSpace-complete, in sheer contrast to Ackermann-completeness for arbitrary VASS, even in dimension 1. When the dimension d ∈ ℕ is fixed, the universality problem is PSpace-complete if d ≥ 2, and coNP-hard for 1-dimensional VASSes (also known as One Counter Nets).
Cite as

Wojciech Czerwiński, Diego Figueira, and Piotr Hofman. Universality Problem for Unambiguous VASS. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 36:1-36:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.CONCUR.2020.36,
  author =	{Czerwi\'{n}ski, Wojciech and Figueira, Diego and Hofman, Piotr},
  title =	{{Universality Problem for Unambiguous VASS}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{36:1--36:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.36},
  URN =		{urn:nbn:de:0030-drops-128486},
  doi =		{10.4230/LIPIcs.CONCUR.2020.36},
  annote =	{Keywords: unambiguity, vector addition systems, universality problems}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.48
Reachability in Fixed Dimension Vector Addition Systems with States

Authors: Wojciech Czerwiński, Sławomir Lasota, Ranko Lazić, Jérôme Leroux, and Filip Mazowiecki

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
The reachability problem is a central decision problem in verification of vector addition systems with states (VASS). In spite of recent progress, the complexity of the reachability problem remains unsettled, and it is closely related to the lengths of shortest VASS runs that witness reachability. We obtain three main results for VASS of fixed dimension. For the first two, we assume that the integers in the input are given in unary, and that the control graph of the given VASS is flat (i.e., without nested cycles). We obtain a family of VASS in dimension 3 whose shortest runs are exponential, and we show that the reachability problem is NP-hard in dimension 7. These results resolve negatively questions that had been posed by the works of Blondin et al. in LICS 2015 and Englert et al. in LICS 2016, and contribute a first construction that distinguishes 3-dimensional flat VASS from 2-dimensional ones. Our third result, by means of a novel family of products of integer fractions, shows that 4-dimensional VASS can have doubly exponentially long shortest runs. The smallest dimension for which this was previously known is 14.
Cite as

Wojciech Czerwiński, Sławomir Lasota, Ranko Lazić, Jérôme Leroux, and Filip Mazowiecki. Reachability in Fixed Dimension Vector Addition Systems with States. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 48:1-48:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.CONCUR.2020.48,
  author =	{Czerwi\'{n}ski, Wojciech and Lasota, S{\l}awomir and Lazi\'{c}, Ranko and Leroux, J\'{e}r\^{o}me and Mazowiecki, Filip},
  title =	{{Reachability in Fixed Dimension Vector Addition Systems with States}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{48:1--48:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.48},
  URN =		{urn:nbn:de:0030-drops-128605},
  doi =		{10.4230/LIPIcs.CONCUR.2020.48},
  annote =	{Keywords: reachability problem, vector addition systems, Petri nets}
}
Document
DOI: 10.4230/LIPIcs.ESA.2019.34
Improved Bounds for the Excluded-Minor Approximation of Treedepth

Authors: Wojciech Czerwiński, Wojciech Nadara, and Marcin Pilipczuk

Published in: LIPIcs, Volume 144, 27th Annual European Symposium on Algorithms (ESA 2019)

Abstract
Treedepth, a more restrictive graph width parameter than treewidth and pathwidth, plays a major role in the theory of sparse graph classes. We show that there exists a constant C such that for every integers a,b >= 2 and a graph G, if the treedepth of G is at least Cab log a, then the treewidth of G is at least a or G contains a subcubic (i.e., of maximum degree at most 3) tree of treedepth at least b as a subgraph. As a direct corollary, we obtain that every graph of treedepth Omega(k^3 log k) is either of treewidth at least k, contains a subdivision of full binary tree of depth k, or contains a path of length 2^k. This improves the bound of Omega(k^5 log^2 k) of Kawarabayashi and Rossman [SODA 2018]. We also show an application for approximation algorithms of treedepth: given a graph G of treedepth k and treewidth t, one can in polynomial time compute a treedepth decomposition of G of width O(kt log^{3/2} t). This improves upon a bound of O(kt^2 log t) stemming from a tradeoff between known results. The main technical ingredient in our result is a proof that every tree of treedepth d contains a subcubic subtree of treedepth at least d * log_3 ((1+sqrt{5})/2).
Cite as

Wojciech Czerwiński, Wojciech Nadara, and Marcin Pilipczuk. Improved Bounds for the Excluded-Minor Approximation of Treedepth. In 27th Annual European Symposium on Algorithms (ESA 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 144, pp. 34:1-34:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.ESA.2019.34,
  author =	{Czerwi\'{n}ski, Wojciech and Nadara, Wojciech and Pilipczuk, Marcin},
  title =	{{Improved Bounds for the Excluded-Minor Approximation of Treedepth}},
  booktitle =	{27th Annual European Symposium on Algorithms (ESA 2019)},
  pages =	{34:1--34:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-124-5},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{144},
  editor =	{Bender, Michael A. and Svensson, Ola and Herman, Grzegorz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2019.34},
  URN =		{urn:nbn:de:0030-drops-111557},
  doi =		{10.4230/LIPIcs.ESA.2019.34},
  annote =	{Keywords: treedepth, excluded minor}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2019.62
New Pumping Technique for 2-Dimensional VASS

Authors: Wojciech Czerwiński, Sławomir Lasota, Christof Löding, and Radosław Piórkowski

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

Abstract
We propose a new pumping technique for 2-dimensional vector addition systems with states (2-VASS) building on natural geometric properties of runs. We illustrate its applicability by reproving an exponential bound on the length of the shortest accepting run, and by proving a new pumping lemma for languages of 2-VASS. The technique is expected to be useful for settling questions concerning languages of 2-VASS, e.g., for establishing decidability status of the regular separability problem.
Cite as

Wojciech Czerwiński, Sławomir Lasota, Christof Löding, and Radosław Piórkowski. New Pumping Technique for 2-Dimensional VASS. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 62:1-62:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.MFCS.2019.62,
  author =	{Czerwi\'{n}ski, Wojciech and Lasota, S{\l}awomir and L\"{o}ding, Christof and Pi\'{o}rkowski, Rados{\l}aw},
  title =	{{New Pumping Technique for 2-Dimensional VASS}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{62:1--62:14},
  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.62},
  URN =		{urn:nbn:de:0030-drops-110066},
  doi =		{10.4230/LIPIcs.MFCS.2019.62},
  annote =	{Keywords: vector addition systems with states, pumping, decidability}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2018.35
Regular Separability of Well-Structured Transition Systems

Authors: Wojciech Czerwinski, Slawomir Lasota, Roland Meyer, Sebastian Muskalla, K. Narayan Kumar, and Prakash Saivasan

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

Abstract
We investigate the languages recognized by well-structured transition systems (WSTS) with upward and downward compatibility. Our first result shows that, under very mild assumptions, every two disjoint WSTS languages are regular separable: There is a regular language containing one of them and being disjoint from the other. As a consequence, if a language as well as its complement are both recognized by WSTS, then they are necessarily regular. In particular, no subclass of WSTS languages beyond the regular languages is closed under complement. Our second result shows that for Petri nets, the complexity of the backwards coverability algorithm yields a bound on the size of the regular separator. We complement it by a lower bound construction.
Cite as

Wojciech Czerwinski, Slawomir Lasota, Roland Meyer, Sebastian Muskalla, K. Narayan Kumar, and Prakash Saivasan. Regular Separability of Well-Structured Transition Systems. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 35:1-35:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.CONCUR.2018.35,
  author =	{Czerwinski, Wojciech and Lasota, Slawomir and Meyer, Roland and Muskalla, Sebastian and Narayan Kumar, K. and Saivasan, Prakash},
  title =	{{Regular Separability of Well-Structured Transition Systems}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{35:1--35:18},
  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.35},
  URN =		{urn:nbn:de:0030-drops-95733},
  doi =		{10.4230/LIPIcs.CONCUR.2018.35},
  annote =	{Keywords: regular separability, wsts, coverability languages, Petri nets}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2018.119
Unboundedness Problems for Languages of Vector Addition Systems

Authors: Wojciech Czerwinski, Piotr Hofman, and Georg Zetzsche

Published in: LIPIcs, Volume 107, 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)

Abstract
A vector addition system (VAS) with an initial and a final marking and transition labels induces a language. In part because the reachability problem in VAS remains far from being well-understood, it is difficult to devise decision procedures for such languages. This is especially true for checking properties that state the existence of infinitely many words of a particular shape. Informally, we call these unboundedness properties. We present a simple set of axioms for predicates that can express unboundedness properties. Our main result is that such a predicate is decidable for VAS languages as soon as it is decidable for regular languages. Among other results, this allows us to show decidability of (i) separability by bounded regular languages, (ii) unboundedness of occurring factors from a language K with mild conditions on K, and (iii) universality of the set of factors.
Cite as

Wojciech Czerwinski, Piotr Hofman, and Georg Zetzsche. Unboundedness Problems for Languages of Vector Addition Systems. In 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 107, pp. 119:1-119:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.ICALP.2018.119,
  author =	{Czerwinski, Wojciech and Hofman, Piotr and Zetzsche, Georg},
  title =	{{Unboundedness Problems for Languages of Vector Addition Systems}},
  booktitle =	{45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)},
  pages =	{119:1--119:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-076-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{107},
  editor =	{Chatzigiannakis, Ioannis and Kaklamanis, Christos and Marx, D\'{a}niel and Sannella, Donald},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2018.119},
  URN =		{urn:nbn:de:0030-drops-91235},
  doi =		{10.4230/LIPIcs.ICALP.2018.119},
  annote =	{Keywords: vector addition systems, decision problems, unboundedness, separability}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2017.117
Regular Separability of Parikh Automata

Authors: Lorenzo Clemente, Wojciech Czerwinski, Slawomir Lasota, and Charles Paperman

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

Abstract
We investigate a subclass of languages recognized by vector addition systems, namely languages of nondeterministic Parikh automata. While the regularity problem (is the language of a given automaton regular?) is undecidable for this model, we surprisingly show decidability of the regular separability problem: given two Parikh automata, is there a regular language that contains one of them and is disjoint from the other? We supplement this result by proving undecidability of the same problem already for languages of visibly one counter automata.
Cite as

Lorenzo Clemente, Wojciech Czerwinski, Slawomir Lasota, and Charles Paperman. Regular Separability of Parikh Automata. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 117:1-117:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{clemente_et_al:LIPIcs.ICALP.2017.117,
  author =	{Clemente, Lorenzo and Czerwinski, Wojciech and Lasota, Slawomir and Paperman, Charles},
  title =	{{Regular Separability of Parikh Automata}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{117:1--117: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.117},
  URN =		{urn:nbn:de:0030-drops-74971},
  doi =		{10.4230/LIPIcs.ICALP.2017.117},
  annote =	{Keywords: Regular separability problem, Parikh automata, integer vector addition systems, visible one counter automata, decidability, undecidability}
}
Document
DOI: 10.4230/LIPIcs.STACS.2017.24
Separability of Reachability Sets of Vector Addition Systems

Authors: Lorenzo Clemente, Wojciech Czerwinski, Slawomir Lasota, and Charles Paperman

Published in: LIPIcs, Volume 66, 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)

Abstract
Given two families of sets F and G, the F-separability problem for G asks whether for two given sets U, V in G there exists a set S in F, such that U is included in S and V is disjoint with S. We consider two families of sets F: modular sets S which are subsets of N^d, defined as unions of equivalence classes modulo some natural number n in N, and unary sets, which extend modular sets by requiring equality below a threshold n, and equivalence modulo n above n. Our main result is decidability of modular- and unary-separability for the class G of reachability sets of Vector Addition Systems, Petri Nets, Vector Addition Systems with States, and for sections thereof.
Cite as

Lorenzo Clemente, Wojciech Czerwinski, Slawomir Lasota, and Charles Paperman. Separability of Reachability Sets of Vector Addition Systems. In 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 66, pp. 24:1-24:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{clemente_et_al:LIPIcs.STACS.2017.24,
  author =	{Clemente, Lorenzo and Czerwinski, Wojciech and Lasota, Slawomir and Paperman, Charles},
  title =	{{Separability of Reachability Sets of Vector Addition Systems}},
  booktitle =	{34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)},
  pages =	{24:1--24:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-028-6},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{66},
  editor =	{Vollmer, Heribert and Vall\'{e}e, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2017.24},
  URN =		{urn:nbn:de:0030-drops-70091},
  doi =		{10.4230/LIPIcs.STACS.2017.24},
  annote =	{Keywords: separability, Petri nets, modular sets, unary sets, decidability}
}
Document
DOI: 10.4230/LIPIcs.ICDT.2016.20
Reasoning About Integrity Constraints for Tree-Structured Data

Authors: Wojciech Czerwinski, Claire David, Filip Murlak, and Pawel Parys

Published in: LIPIcs, Volume 48, 19th International Conference on Database Theory (ICDT 2016)

Abstract
We study a class of integrity constraints for tree-structured data modelled as data trees, whose nodes have a label from a finite alphabet and store a data value from an infinite data domain. The constraints require each tuple of nodes selected by a conjunctive query (using navigational axes and labels) to satisfy a positive combination of equalities and a positive combination of inequalities over the stored data values. Such constraints are instances of the general framework of XML-to-relational constraints proposed recently by Niewerth and Schwentick. They cover some common classes of constraints, including W3C XML Schema key and unique constraints, as well as domain restrictions and denial constraints, but cannot express inclusion constraints, such as reference keys. Our main result is that consistency of such integrity constraints with respect to a given schema (modelled as a tree automaton) is decidable. An easy extension gives decidability for the entailment problem. Equivalently, we show that validity and containment of unions of conjunctive queries using navigational axes, labels, data equalities and inequalities is decidable, as long as none of the conjunctive queries uses both equalities and inequalities; without this restriction, both problems are known to be undecidable. In the context of XML data exchange, our result can be used to establish decidability for a consistency problem for XML schema mappings. All the decision procedures are doubly exponential, with matching lower bounds. The complexity may be lowered to singly exponential, when conjunctive queries are replaced by tree patterns, and the number of data comparisons is bounded.
Cite as

Wojciech Czerwinski, Claire David, Filip Murlak, and Pawel Parys. Reasoning About Integrity Constraints for Tree-Structured Data. In 19th International Conference on Database Theory (ICDT 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 48, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.ICDT.2016.20,
  author =	{Czerwinski, Wojciech and David, Claire and Murlak, Filip and Parys, Pawel},
  title =	{{Reasoning About Integrity Constraints for Tree-Structured Data}},
  booktitle =	{19th International Conference on Database Theory (ICDT 2016)},
  pages =	{20:1--20:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-002-6},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{48},
  editor =	{Martens, Wim and Zeume, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2016.20},
  URN =		{urn:nbn:de:0030-drops-57897},
  doi =		{10.4230/LIPIcs.ICDT.2016.20},
  annote =	{Keywords: data trees, integrity constraints, unions of conjunctive queries, schema mappings, entailment, containment, consistency}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2010.260
Fast equivalence-checking for normed context-free processes

Authors: Wojciech Czerwinski and Slawomir Lasota

Published in: LIPIcs, Volume 8, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)

Abstract
Bisimulation equivalence is decidable in polynomial time over normed graphs generated by a context-free grammar. We present a new algorithm, working in time $O(n^5)$, thus improving the previously known complexity $O(n^8 * polylog(n))$. It also improves the previously known complexity $O(n^6 * polylog(n))$ of the equality problem for simple grammars.
Cite as

Wojciech Czerwinski and Slawomir Lasota. Fast equivalence-checking for normed context-free processes. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 260-271, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.FSTTCS.2010.260,
  author =	{Czerwinski, Wojciech and Lasota, Slawomir},
  title =	{{Fast equivalence-checking for normed context-free processes}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{260--271},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-23-1},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{8},
  editor =	{Lodaya, Kamal and Mahajan, Meena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010.260},
  URN =		{urn:nbn:de:0030-drops-28690},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.260},
  annote =	{Keywords: bisimulation, norm, context-free grammar, simple grammar}
}

Czerwiński, Wojciech

Document
Invited Paper
DOI: 10.4230/LIPIcs.MFCS.2024.2
Challenges of the Reachability Problem in Infinite-State Systems (Invited Paper)

Authors: Wojciech Czerwiński

Published in: LIPIcs, Volume 306, 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)

Abstract
The reachability problem is a central problem for various infinite state systems like automata with pushdown, with different kinds of counters or combinations thereof. Despite its centrality and decades of research the community still lacks a lot of answers for fundamental and basic questions of that type. I briefly describe my personal viewpoint on the current state of art and emphasise interesting directions, which are worth investigating in my opinion. I also formulate several easy to formulate and understand challenges, which might be pretty hard to solve but at the same time illustrate fundamental lack of our understanding in the area.
Cite as

Wojciech Czerwiński. Challenges of the Reachability Problem in Infinite-State Systems (Invited Paper). In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 2:1-2:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{czerwinski:LIPIcs.MFCS.2024.2,
  author =	{Czerwi\'{n}ski, Wojciech},
  title =	{{Challenges of the Reachability Problem in Infinite-State Systems}},
  booktitle =	{49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)},
  pages =	{2:1--2:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-335-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{306},
  editor =	{Kr\'{a}lovi\v{c}, Rastislav and Ku\v{c}era, Anton{\'\i}n},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2024.2},
  URN =		{urn:nbn:de:0030-drops-205582},
  doi =		{10.4230/LIPIcs.MFCS.2024.2},
  annote =	{Keywords: reachability problem, infinite-state systems, vector addition systems, pushdown}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2023.16
Acyclic Petri and Workflow Nets with Resets

Authors: Dmitry Chistikov, Wojciech Czerwiński, Piotr Hofman, Filip Mazowiecki, and Henry Sinclair-Banks

Published in: LIPIcs, Volume 284, 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)

Abstract
In this paper we propose two new subclasses of Petri nets with resets, for which the reachability and coverability problems become tractable. Namely, we add an acyclicity condition that only applies to the consumptions and productions, not the resets. The first class is acyclic Petri nets with resets, and we show that coverability is PSPACE-complete for them. This contrasts the known Ackermann-hardness for coverability in (not necessarily acyclic) Petri nets with resets. We prove that the reachability problem remains undecidable for acyclic Petri nets with resets. The second class concerns workflow nets, a practically motivated and natural subclass of Petri nets. Here, we show that both coverability and reachability in acyclic workflow nets with resets are PSPACE-complete. Without the acyclicity condition, reachability and coverability in workflow nets with resets are known to be equally hard as for Petri nets with resets, that being Ackermann-hard and undecidable, respectively.
Cite as

Dmitry Chistikov, Wojciech Czerwiński, Piotr Hofman, Filip Mazowiecki, and Henry Sinclair-Banks. Acyclic Petri and Workflow Nets with Resets. In 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 284, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{chistikov_et_al:LIPIcs.FSTTCS.2023.16,
  author =	{Chistikov, Dmitry and Czerwi\'{n}ski, Wojciech and Hofman, Piotr and Mazowiecki, Filip and Sinclair-Banks, Henry},
  title =	{{Acyclic Petri and Workflow Nets with Resets}},
  booktitle =	{43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)},
  pages =	{16:1--16:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-304-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{284},
  editor =	{Bouyer, Patricia and Srinivasan, Srikanth},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2023.16},
  URN =		{urn:nbn:de:0030-drops-193892},
  doi =		{10.4230/LIPIcs.FSTTCS.2023.16},
  annote =	{Keywords: Petri nets, Workflow Nets, Resets, Acyclic, Reachability, Coverability}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2023.22
Languages Given by Finite Automata over the Unary Alphabet

Authors: Wojciech Czerwiński, Maciej Dębski, Tomasz Gogasz, Gordon Hoi, Sanjay Jain, Michał Skrzypczak, Frank Stephan, and Christopher Tan

Published in: LIPIcs, Volume 284, 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)

Abstract
This paper studies the complexity of operations on finite automata and the complexity of their decision problems when the alphabet is unary and n the number of states of the finite automata considered. The following main results are obtained: 1) Equality and inclusion of NFAs can be decided within time 2^O((n log n)^{1/3}); previous upper bound 2^O((n log n)^{1/2}) was by Chrobak (1986) via DFA conversion. 2) The state complexity of operations of UFAs (unambiguous finite automata) increases for complementation and union at most by quasipolynomial; however, for concatenation of two n-state UFAs, the worst case is an UFA of at least 2^Ω(n^{1/6}) states. Previously the upper bounds for complementation and union were exponential-type and this lower bound for concatenation is new.
Cite as

Wojciech Czerwiński, Maciej Dębski, Tomasz Gogasz, Gordon Hoi, Sanjay Jain, Michał Skrzypczak, Frank Stephan, and Christopher Tan. Languages Given by Finite Automata over the Unary Alphabet. In 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 284, pp. 22:1-22:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.FSTTCS.2023.22,
  author =	{Czerwi\'{n}ski, Wojciech and D\k{e}bski, Maciej and Gogasz, Tomasz and Hoi, Gordon and Jain, Sanjay and Skrzypczak, Micha{\l} and Stephan, Frank and Tan, Christopher},
  title =	{{Languages Given by Finite Automata over the Unary Alphabet}},
  booktitle =	{43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)},
  pages =	{22:1--22:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-304-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{284},
  editor =	{Bouyer, Patricia and Srinivasan, Srikanth},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2023.22},
  URN =		{urn:nbn:de:0030-drops-193959},
  doi =		{10.4230/LIPIcs.FSTTCS.2023.22},
  annote =	{Keywords: Nondeterministic Finite Automata, Unambiguous Finite Automata, Upper Bounds on Runtime, Conditional Lower Bounds, Languages over the Unary Alphabet}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2023.35
New Lower Bounds for Reachability in Vector Addition Systems

Authors: Wojciech Czerwiński, Ismaël Jecker, Sławomir Lasota, Jérôme Leroux, and Łukasz Orlikowski

Published in: LIPIcs, Volume 284, 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)

Abstract
We investigate the dimension-parametric complexity of the reachability problem in vector addition systems with states (VASS) and its extension with pushdown stack (pushdown VASS). Up to now, the problem is known to be F_d-hard for VASS of dimension 3d+2 (the complexity class F_d corresponds to the kth level of the fast-growing hierarchy), and no essentially better bound is known for pushdown VASS. We provide a new construction that improves the lower bound for VASS: F_d-hardness in dimension 2d+3. Furthermore, building on our new insights we show a new lower bound for pushdown VASS: F_d-hardness in dimension d/2 + 6. This dimension-parametric lower bound is strictly stronger than the upper bound for VASS, which suggests that the (still unknown) complexity of the reachability problem in pushdown VASS is higher than in plain VASS (where it is Ackermann-complete).
Cite as

Wojciech Czerwiński, Ismaël Jecker, Sławomir Lasota, Jérôme Leroux, and Łukasz Orlikowski. New Lower Bounds for Reachability in Vector Addition Systems. In 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 284, pp. 35:1-35:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.FSTTCS.2023.35,
  author =	{Czerwi\'{n}ski, Wojciech and Jecker, Isma\"{e}l and Lasota, S{\l}awomir and Leroux, J\'{e}r\^{o}me and Orlikowski, {\L}ukasz},
  title =	{{New Lower Bounds for Reachability in Vector Addition Systems}},
  booktitle =	{43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)},
  pages =	{35:1--35:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-304-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{284},
  editor =	{Bouyer, Patricia and Srinivasan, Srikanth},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2023.35},
  URN =		{urn:nbn:de:0030-drops-194088},
  doi =		{10.4230/LIPIcs.FSTTCS.2023.35},
  annote =	{Keywords: vector addition systems, reachability problem, pushdown vector addition system, lower bounds}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CONCUR.2022.5
Involved VASS Zoo (Invited Talk)

Authors: Wojciech Czerwiński

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract
We briefly describe recent advances on understanding the complexity of the reachability problem for vector addition systems (or equivalently for vector addition systems with states - VASSes). We present a zoo of a few involved VASS examples, which illustrate various aspects of hardness of VASSes and various techniques of proving lower complexity bounds.
Cite as

Wojciech Czerwiński. Involved VASS Zoo (Invited Talk). In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 5:1-5:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{czerwinski:LIPIcs.CONCUR.2022.5,
  author =	{Czerwi\'{n}ski, Wojciech},
  title =	{{Involved VASS Zoo}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{5:1--5:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir 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.CONCUR.2022.5},
  URN =		{urn:nbn:de:0030-drops-170681},
  doi =		{10.4230/LIPIcs.CONCUR.2022.5},
  annote =	{Keywords: vector addition systems, reachability problem, low dimensions, examples}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2022.16
Language Inclusion for Boundedly-Ambiguous Vector Addition Systems Is Decidable

Authors: Wojciech Czerwiński and Piotr Hofman

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract
We consider the problems of language inclusion and language equivalence for Vector Addition Systems with States (VASSes) with the acceptance condition defined by the set of accepting states (and more generally by some upward-closed conditions). In general the problem of language equivalence is undecidable even for one-dimensional VASSes, thus to get decidability we investigate restricted subclasses. On one hand we show that the problem of language inclusion of a VASS in k-ambiguous VASS (for any natural k) is decidable and even in Ackermann. On the other hand we prove that the language equivalence problem is Ackermann-hard already for deterministic VASSes. These two results imply Ackermann-completeness for language inclusion and equivalence in several possible restrictions. Some of our techniques can be also applied in much broader generality in infinite-state systems, namely for some subclass of well-structured transition systems.
Cite as

Wojciech Czerwiński and Piotr Hofman. Language Inclusion for Boundedly-Ambiguous Vector Addition Systems Is Decidable. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 16:1-16:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.CONCUR.2022.16,
  author =	{Czerwi\'{n}ski, Wojciech and Hofman, Piotr},
  title =	{{Language Inclusion for Boundedly-Ambiguous Vector Addition Systems Is Decidable}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{16:1--16:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir 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.CONCUR.2022.16},
  URN =		{urn:nbn:de:0030-drops-170796},
  doi =		{10.4230/LIPIcs.CONCUR.2022.16},
  annote =	{Keywords: vector addition systems, language inclusion, language equivalence, determinism, unambiguity, bounded ambiguity, Petri nets, well-structured transition systems}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2021.128
Improved Lower Bounds for Reachability in Vector Addition Systems

Authors: Wojciech Czerwiński, Sławomir Lasota, and Łukasz Orlikowski

Published in: LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)

Abstract
We investigate computational complexity of the reachability problem for vector addition systems (or, equivalently, Petri nets), the central algorithmic problem in verification of concurrent systems. Concerning its complexity, after 40 years of stagnation, a non-elementary lower bound has been shown recently: the problem needs a tower of exponentials of time or space, where the height of tower is linear in the input size. We improve on this lower bound, by increasing the height of tower from linear to exponential. As a side-effect, we obtain better lower bounds for vector addition systems of fixed dimension.
Cite as

Wojciech Czerwiński, Sławomir Lasota, and Łukasz Orlikowski. Improved Lower Bounds for Reachability in Vector Addition Systems. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 128:1-128:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.ICALP.2021.128,
  author =	{Czerwi\'{n}ski, Wojciech and Lasota, S{\l}awomir and Orlikowski, {\L}ukasz},
  title =	{{Improved Lower Bounds for Reachability in Vector Addition Systems}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{128:1--128:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.128},
  URN =		{urn:nbn:de:0030-drops-141973},
  doi =		{10.4230/LIPIcs.ICALP.2021.128},
  annote =	{Keywords: Petri nets, vector addition systems, reachability problem}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2021.129
New Techniques for Universality in Unambiguous Register Automata

Authors: Wojciech Czerwiński, Antoine Mottet, and Karin Quaas

Published in: LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)

Abstract
Register automata are finite automata equipped with a finite set of registers ranging over the domain of some relational structure like (ℕ; =) or (ℚ; <). Register automata process words over the domain, and along a run of the automaton, the registers can store data from the input word for later comparisons. It is long known that the universality problem, i.e., the problem to decide whether a given register automaton accepts all words over the domain, is undecidable. Recently, we proved the problem to be decidable in 2-ExpSpace if the register automaton under study is over (ℕ; =) and unambiguous, i.e., every input word has at most one accepting run; this result was shortly after improved to 2-ExpTime by Barloy and Clemente. In this paper, we go one step further and prove that the problem is in ExpSpace, and in PSpace if the number of registers is fixed. Our proof is based on new techniques that additionally allow us to show that the problem is in PSpace for single-register automata over (ℚ; <). As a third technical contribution we prove that the problem is decidable (in ExpSpace) for a more expressive model of unambiguous register automata, where the registers can take values nondeterministically, if defined over (ℕ; =) and only one register is used.
Cite as

Wojciech Czerwiński, Antoine Mottet, and Karin Quaas. New Techniques for Universality in Unambiguous Register Automata. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 129:1-129:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.ICALP.2021.129,
  author =	{Czerwi\'{n}ski, Wojciech and Mottet, Antoine and Quaas, Karin},
  title =	{{New Techniques for Universality in Unambiguous Register Automata}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{129:1--129:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.129},
  URN =		{urn:nbn:de:0030-drops-141983},
  doi =		{10.4230/LIPIcs.ICALP.2021.129},
  annote =	{Keywords: Register Automata, Data Languages, Unambiguity, Unambiguous, Universality, Containment, Language Inclusion, Equivalence}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.36
Universality Problem for Unambiguous VASS

Authors: Wojciech Czerwiński, Diego Figueira, and Piotr Hofman

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
We study languages of unambiguous VASS, that is, Vector Addition Systems with States, whose transitions read letters from a finite alphabet, and whose acceptance condition is defined by a set of final states (i.e., the coverability language). We show that the problem of universality for unambiguous VASS is ExpSpace-complete, in sheer contrast to Ackermann-completeness for arbitrary VASS, even in dimension 1. When the dimension d ∈ ℕ is fixed, the universality problem is PSpace-complete if d ≥ 2, and coNP-hard for 1-dimensional VASSes (also known as One Counter Nets).
Cite as

Wojciech Czerwiński, Diego Figueira, and Piotr Hofman. Universality Problem for Unambiguous VASS. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 36:1-36:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.CONCUR.2020.36,
  author =	{Czerwi\'{n}ski, Wojciech and Figueira, Diego and Hofman, Piotr},
  title =	{{Universality Problem for Unambiguous VASS}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{36:1--36:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.36},
  URN =		{urn:nbn:de:0030-drops-128486},
  doi =		{10.4230/LIPIcs.CONCUR.2020.36},
  annote =	{Keywords: unambiguity, vector addition systems, universality problems}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.48
Reachability in Fixed Dimension Vector Addition Systems with States

Authors: Wojciech Czerwiński, Sławomir Lasota, Ranko Lazić, Jérôme Leroux, and Filip Mazowiecki

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
The reachability problem is a central decision problem in verification of vector addition systems with states (VASS). In spite of recent progress, the complexity of the reachability problem remains unsettled, and it is closely related to the lengths of shortest VASS runs that witness reachability. We obtain three main results for VASS of fixed dimension. For the first two, we assume that the integers in the input are given in unary, and that the control graph of the given VASS is flat (i.e., without nested cycles). We obtain a family of VASS in dimension 3 whose shortest runs are exponential, and we show that the reachability problem is NP-hard in dimension 7. These results resolve negatively questions that had been posed by the works of Blondin et al. in LICS 2015 and Englert et al. in LICS 2016, and contribute a first construction that distinguishes 3-dimensional flat VASS from 2-dimensional ones. Our third result, by means of a novel family of products of integer fractions, shows that 4-dimensional VASS can have doubly exponentially long shortest runs. The smallest dimension for which this was previously known is 14.
Cite as

Wojciech Czerwiński, Sławomir Lasota, Ranko Lazić, Jérôme Leroux, and Filip Mazowiecki. Reachability in Fixed Dimension Vector Addition Systems with States. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 48:1-48:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.CONCUR.2020.48,
  author =	{Czerwi\'{n}ski, Wojciech and Lasota, S{\l}awomir and Lazi\'{c}, Ranko and Leroux, J\'{e}r\^{o}me and Mazowiecki, Filip},
  title =	{{Reachability in Fixed Dimension Vector Addition Systems with States}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{48:1--48:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.48},
  URN =		{urn:nbn:de:0030-drops-128605},
  doi =		{10.4230/LIPIcs.CONCUR.2020.48},
  annote =	{Keywords: reachability problem, vector addition systems, Petri nets}
}
Document
DOI: 10.4230/LIPIcs.ESA.2019.34
Improved Bounds for the Excluded-Minor Approximation of Treedepth

Authors: Wojciech Czerwiński, Wojciech Nadara, and Marcin Pilipczuk

Published in: LIPIcs, Volume 144, 27th Annual European Symposium on Algorithms (ESA 2019)

Abstract
Treedepth, a more restrictive graph width parameter than treewidth and pathwidth, plays a major role in the theory of sparse graph classes. We show that there exists a constant C such that for every integers a,b >= 2 and a graph G, if the treedepth of G is at least Cab log a, then the treewidth of G is at least a or G contains a subcubic (i.e., of maximum degree at most 3) tree of treedepth at least b as a subgraph. As a direct corollary, we obtain that every graph of treedepth Omega(k^3 log k) is either of treewidth at least k, contains a subdivision of full binary tree of depth k, or contains a path of length 2^k. This improves the bound of Omega(k^5 log^2 k) of Kawarabayashi and Rossman [SODA 2018]. We also show an application for approximation algorithms of treedepth: given a graph G of treedepth k and treewidth t, one can in polynomial time compute a treedepth decomposition of G of width O(kt log^{3/2} t). This improves upon a bound of O(kt^2 log t) stemming from a tradeoff between known results. The main technical ingredient in our result is a proof that every tree of treedepth d contains a subcubic subtree of treedepth at least d * log_3 ((1+sqrt{5})/2).
Cite as

Wojciech Czerwiński, Wojciech Nadara, and Marcin Pilipczuk. Improved Bounds for the Excluded-Minor Approximation of Treedepth. In 27th Annual European Symposium on Algorithms (ESA 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 144, pp. 34:1-34:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.ESA.2019.34,
  author =	{Czerwi\'{n}ski, Wojciech and Nadara, Wojciech and Pilipczuk, Marcin},
  title =	{{Improved Bounds for the Excluded-Minor Approximation of Treedepth}},
  booktitle =	{27th Annual European Symposium on Algorithms (ESA 2019)},
  pages =	{34:1--34:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-124-5},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{144},
  editor =	{Bender, Michael A. and Svensson, Ola and Herman, Grzegorz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2019.34},
  URN =		{urn:nbn:de:0030-drops-111557},
  doi =		{10.4230/LIPIcs.ESA.2019.34},
  annote =	{Keywords: treedepth, excluded minor}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2019.62
New Pumping Technique for 2-Dimensional VASS

Authors: Wojciech Czerwiński, Sławomir Lasota, Christof Löding, and Radosław Piórkowski

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

Abstract
We propose a new pumping technique for 2-dimensional vector addition systems with states (2-VASS) building on natural geometric properties of runs. We illustrate its applicability by reproving an exponential bound on the length of the shortest accepting run, and by proving a new pumping lemma for languages of 2-VASS. The technique is expected to be useful for settling questions concerning languages of 2-VASS, e.g., for establishing decidability status of the regular separability problem.
Cite as

Wojciech Czerwiński, Sławomir Lasota, Christof Löding, and Radosław Piórkowski. New Pumping Technique for 2-Dimensional VASS. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 62:1-62:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.MFCS.2019.62,
  author =	{Czerwi\'{n}ski, Wojciech and Lasota, S{\l}awomir and L\"{o}ding, Christof and Pi\'{o}rkowski, Rados{\l}aw},
  title =	{{New Pumping Technique for 2-Dimensional VASS}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{62:1--62:14},
  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.62},
  URN =		{urn:nbn:de:0030-drops-110066},
  doi =		{10.4230/LIPIcs.MFCS.2019.62},
  annote =	{Keywords: vector addition systems with states, pumping, decidability}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2018.35
Regular Separability of Well-Structured Transition Systems

Authors: Wojciech Czerwinski, Slawomir Lasota, Roland Meyer, Sebastian Muskalla, K. Narayan Kumar, and Prakash Saivasan

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

Abstract
We investigate the languages recognized by well-structured transition systems (WSTS) with upward and downward compatibility. Our first result shows that, under very mild assumptions, every two disjoint WSTS languages are regular separable: There is a regular language containing one of them and being disjoint from the other. As a consequence, if a language as well as its complement are both recognized by WSTS, then they are necessarily regular. In particular, no subclass of WSTS languages beyond the regular languages is closed under complement. Our second result shows that for Petri nets, the complexity of the backwards coverability algorithm yields a bound on the size of the regular separator. We complement it by a lower bound construction.
Cite as

Wojciech Czerwinski, Slawomir Lasota, Roland Meyer, Sebastian Muskalla, K. Narayan Kumar, and Prakash Saivasan. Regular Separability of Well-Structured Transition Systems. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 35:1-35:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.CONCUR.2018.35,
  author =	{Czerwinski, Wojciech and Lasota, Slawomir and Meyer, Roland and Muskalla, Sebastian and Narayan Kumar, K. and Saivasan, Prakash},
  title =	{{Regular Separability of Well-Structured Transition Systems}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{35:1--35:18},
  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.35},
  URN =		{urn:nbn:de:0030-drops-95733},
  doi =		{10.4230/LIPIcs.CONCUR.2018.35},
  annote =	{Keywords: regular separability, wsts, coverability languages, Petri nets}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2018.119
Unboundedness Problems for Languages of Vector Addition Systems

Authors: Wojciech Czerwinski, Piotr Hofman, and Georg Zetzsche

Published in: LIPIcs, Volume 107, 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)

Abstract
A vector addition system (VAS) with an initial and a final marking and transition labels induces a language. In part because the reachability problem in VAS remains far from being well-understood, it is difficult to devise decision procedures for such languages. This is especially true for checking properties that state the existence of infinitely many words of a particular shape. Informally, we call these unboundedness properties. We present a simple set of axioms for predicates that can express unboundedness properties. Our main result is that such a predicate is decidable for VAS languages as soon as it is decidable for regular languages. Among other results, this allows us to show decidability of (i) separability by bounded regular languages, (ii) unboundedness of occurring factors from a language K with mild conditions on K, and (iii) universality of the set of factors.
Cite as

Wojciech Czerwinski, Piotr Hofman, and Georg Zetzsche. Unboundedness Problems for Languages of Vector Addition Systems. In 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 107, pp. 119:1-119:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.ICALP.2018.119,
  author =	{Czerwinski, Wojciech and Hofman, Piotr and Zetzsche, Georg},
  title =	{{Unboundedness Problems for Languages of Vector Addition Systems}},
  booktitle =	{45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)},
  pages =	{119:1--119:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-076-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{107},
  editor =	{Chatzigiannakis, Ioannis and Kaklamanis, Christos and Marx, D\'{a}niel and Sannella, Donald},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2018.119},
  URN =		{urn:nbn:de:0030-drops-91235},
  doi =		{10.4230/LIPIcs.ICALP.2018.119},
  annote =	{Keywords: vector addition systems, decision problems, unboundedness, separability}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2017.117
Regular Separability of Parikh Automata

Authors: Lorenzo Clemente, Wojciech Czerwinski, Slawomir Lasota, and Charles Paperman

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

Abstract
We investigate a subclass of languages recognized by vector addition systems, namely languages of nondeterministic Parikh automata. While the regularity problem (is the language of a given automaton regular?) is undecidable for this model, we surprisingly show decidability of the regular separability problem: given two Parikh automata, is there a regular language that contains one of them and is disjoint from the other? We supplement this result by proving undecidability of the same problem already for languages of visibly one counter automata.
Cite as

Lorenzo Clemente, Wojciech Czerwinski, Slawomir Lasota, and Charles Paperman. Regular Separability of Parikh Automata. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 117:1-117:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{clemente_et_al:LIPIcs.ICALP.2017.117,
  author =	{Clemente, Lorenzo and Czerwinski, Wojciech and Lasota, Slawomir and Paperman, Charles},
  title =	{{Regular Separability of Parikh Automata}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{117:1--117: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.117},
  URN =		{urn:nbn:de:0030-drops-74971},
  doi =		{10.4230/LIPIcs.ICALP.2017.117},
  annote =	{Keywords: Regular separability problem, Parikh automata, integer vector addition systems, visible one counter automata, decidability, undecidability}
}
Document
DOI: 10.4230/LIPIcs.STACS.2017.24
Separability of Reachability Sets of Vector Addition Systems

Authors: Lorenzo Clemente, Wojciech Czerwinski, Slawomir Lasota, and Charles Paperman

Published in: LIPIcs, Volume 66, 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)

Abstract
Given two families of sets F and G, the F-separability problem for G asks whether for two given sets U, V in G there exists a set S in F, such that U is included in S and V is disjoint with S. We consider two families of sets F: modular sets S which are subsets of N^d, defined as unions of equivalence classes modulo some natural number n in N, and unary sets, which extend modular sets by requiring equality below a threshold n, and equivalence modulo n above n. Our main result is decidability of modular- and unary-separability for the class G of reachability sets of Vector Addition Systems, Petri Nets, Vector Addition Systems with States, and for sections thereof.
Cite as

Lorenzo Clemente, Wojciech Czerwinski, Slawomir Lasota, and Charles Paperman. Separability of Reachability Sets of Vector Addition Systems. In 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 66, pp. 24:1-24:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{clemente_et_al:LIPIcs.STACS.2017.24,
  author =	{Clemente, Lorenzo and Czerwinski, Wojciech and Lasota, Slawomir and Paperman, Charles},
  title =	{{Separability of Reachability Sets of Vector Addition Systems}},
  booktitle =	{34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)},
  pages =	{24:1--24:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-028-6},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{66},
  editor =	{Vollmer, Heribert and Vall\'{e}e, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2017.24},
  URN =		{urn:nbn:de:0030-drops-70091},
  doi =		{10.4230/LIPIcs.STACS.2017.24},
  annote =	{Keywords: separability, Petri nets, modular sets, unary sets, decidability}
}
Document
DOI: 10.4230/LIPIcs.ICDT.2016.20
Reasoning About Integrity Constraints for Tree-Structured Data

Authors: Wojciech Czerwinski, Claire David, Filip Murlak, and Pawel Parys

Published in: LIPIcs, Volume 48, 19th International Conference on Database Theory (ICDT 2016)

Abstract
We study a class of integrity constraints for tree-structured data modelled as data trees, whose nodes have a label from a finite alphabet and store a data value from an infinite data domain. The constraints require each tuple of nodes selected by a conjunctive query (using navigational axes and labels) to satisfy a positive combination of equalities and a positive combination of inequalities over the stored data values. Such constraints are instances of the general framework of XML-to-relational constraints proposed recently by Niewerth and Schwentick. They cover some common classes of constraints, including W3C XML Schema key and unique constraints, as well as domain restrictions and denial constraints, but cannot express inclusion constraints, such as reference keys. Our main result is that consistency of such integrity constraints with respect to a given schema (modelled as a tree automaton) is decidable. An easy extension gives decidability for the entailment problem. Equivalently, we show that validity and containment of unions of conjunctive queries using navigational axes, labels, data equalities and inequalities is decidable, as long as none of the conjunctive queries uses both equalities and inequalities; without this restriction, both problems are known to be undecidable. In the context of XML data exchange, our result can be used to establish decidability for a consistency problem for XML schema mappings. All the decision procedures are doubly exponential, with matching lower bounds. The complexity may be lowered to singly exponential, when conjunctive queries are replaced by tree patterns, and the number of data comparisons is bounded.
Cite as

Wojciech Czerwinski, Claire David, Filip Murlak, and Pawel Parys. Reasoning About Integrity Constraints for Tree-Structured Data. In 19th International Conference on Database Theory (ICDT 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 48, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.ICDT.2016.20,
  author =	{Czerwinski, Wojciech and David, Claire and Murlak, Filip and Parys, Pawel},
  title =	{{Reasoning About Integrity Constraints for Tree-Structured Data}},
  booktitle =	{19th International Conference on Database Theory (ICDT 2016)},
  pages =	{20:1--20:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-002-6},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{48},
  editor =	{Martens, Wim and Zeume, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2016.20},
  URN =		{urn:nbn:de:0030-drops-57897},
  doi =		{10.4230/LIPIcs.ICDT.2016.20},
  annote =	{Keywords: data trees, integrity constraints, unions of conjunctive queries, schema mappings, entailment, containment, consistency}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2010.260
Fast equivalence-checking for normed context-free processes

Authors: Wojciech Czerwinski and Slawomir Lasota

Published in: LIPIcs, Volume 8, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)

Abstract
Bisimulation equivalence is decidable in polynomial time over normed graphs generated by a context-free grammar. We present a new algorithm, working in time $O(n^5)$, thus improving the previously known complexity $O(n^8 * polylog(n))$. It also improves the previously known complexity $O(n^6 * polylog(n))$ of the equality problem for simple grammars.
Cite as

Wojciech Czerwinski and Slawomir Lasota. Fast equivalence-checking for normed context-free processes. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 260-271, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.FSTTCS.2010.260,
  author =	{Czerwinski, Wojciech and Lasota, Slawomir},
  title =	{{Fast equivalence-checking for normed context-free processes}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{260--271},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-23-1},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{8},
  editor =	{Lodaya, Kamal and Mahajan, Meena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010.260},
  URN =		{urn:nbn:de:0030-drops-28690},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.260},
  annote =	{Keywords: bisimulation, norm, context-free grammar, simple grammar}
}
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 Imprint Privacy Contact