-
Measuring well quasi-ordered finitary powersets
Authors:
Sergio Abriola,
Simon Halfon,
Aliaume Lopez,
Sylvain Schmitz,
Philippe Schnoebelen,
Isa Vialard
Abstract:
The complexity of a well-quasi-order (wqo) can be measured through three classical ordinal invariants: the width as a measure of antichains, the height as a measure of chains, and the maximal order type as a measure of bad sequences. This article considers the "finitary powerset" construction: the collection Pf(X) of finite subsets of a wqo X ordered with the Hoare embedding relation remains a wqo…
▽ More
The complexity of a well-quasi-order (wqo) can be measured through three classical ordinal invariants: the width as a measure of antichains, the height as a measure of chains, and the maximal order type as a measure of bad sequences. This article considers the "finitary powerset" construction: the collection Pf(X) of finite subsets of a wqo X ordered with the Hoare embedding relation remains a wqo. The width, height and maximal order type of Pf(X) cannot be expressed as a function of the invariants of X, and we provide tight upper and lower bounds for the three invariants. The article also identifies an algebra of well-behaved wqos, that include finitary powersets as well as other more classical constructions, and for which the ordinal invariants can be computed compositionnally. This relies on a new ordinal invariant called the approximated maximal order type.
△ Less
Submitted 22 December, 2023;
originally announced December 2023.
-
The Ideal Approach to Computing Closed Subsets in Well-Quasi-Ordering
Authors:
Jean Goubault-Larrecq,
Simon Halfon,
Prateek Karandikar,
K. Narayan Kumar,
Philippe Schnoebelen
Abstract:
Elegant and general algorithms for handling upwards-closed and downwards-closed subsets of WQOs can be developed using the filter-based and ideal-based representation for these sets. These algorithms can be built in a generic or parameterized way, in parallel with the way complex WQOs are obtained by combining or modifying simpler WQOs.
Elegant and general algorithms for handling upwards-closed and downwards-closed subsets of WQOs can be developed using the filter-based and ideal-based representation for these sets. These algorithms can be built in a generic or parameterized way, in parallel with the way complex WQOs are obtained by combining or modifying simpler WQOs.
△ Less
Submitted 24 April, 2019;
originally announced April 2019.
-
On shuffle products, acyclic automata and piecewise-testable languages
Authors:
Simon Halfon,
Philippe Schnoebelen
Abstract:
We show that the shuffle $L \unicode{x29E2} F$ of a piecewise-testable language $L$ and a finite language $F$ is piecewise-testable. The proof relies on a classic but little-used automata-theoretic characterization of piecewise-testable languages. We also discuss some mild generalizations of the main result, and provide bounds on the piecewise complexity of $L \unicode{x29E2} F$.
We show that the shuffle $L \unicode{x29E2} F$ of a piecewise-testable language $L$ and a finite language $F$ is piecewise-testable. The proof relies on a classic but little-used automata-theoretic characterization of piecewise-testable languages. We also discuss some mild generalizations of the main result, and provide bounds on the piecewise complexity of $L \unicode{x29E2} F$.
△ Less
Submitted 1 February, 2019; v1 submitted 6 October, 2018;
originally announced October 2018.
-
Decidability, Complexity, and Expressiveness of First-Order Logic Over the Subword Ordering
Authors:
Simon Halfon,
Philippe Schnoebelen,
Georg Zetzsche
Abstract:
We consider first-order logic over the subword ordering on finite words, where each word is available as a constant. Our first result is that the $Σ_1$ theory is undecidable (already over two letters).
We investigate the decidability border by considering fragments where all but a certain number of variables are alternation bounded, meaning that the variable must always be quantified over langua…
▽ More
We consider first-order logic over the subword ordering on finite words, where each word is available as a constant. Our first result is that the $Σ_1$ theory is undecidable (already over two letters).
We investigate the decidability border by considering fragments where all but a certain number of variables are alternation bounded, meaning that the variable must always be quantified over languages with a bounded number of letter alternations. We prove that when at most two variables are not alternation bounded, the $Σ_1$ fragment is decidable, and that it becomes undecidable when three variables are not alternation bounded. Regarding higher quantifier alternation depths, we prove that the $Σ_2$ fragment is undecidable already for one variable without alternation bound and that when all variables are alternation bounded, the entire first-order theory is decidable.
△ Less
Submitted 24 September, 2021; v1 submitted 25 January, 2017;
originally announced January 2017.
-
Context-Free Commutative Grammars with Integer Counters and Resets
Authors:
Dmitry Chistikov,
Christoph Haase,
Simon Halfon
Abstract:
We study the computational complexity of reachability, coverability and inclusion for extensions of context-free commutative grammars with integer counters and reset operations on them. Those grammars can alternatively be viewed as an extension of communication-free Petri nets. Our main results are that reachability and coverability are inter-reducible and both NP-complete. In particular, this cla…
▽ More
We study the computational complexity of reachability, coverability and inclusion for extensions of context-free commutative grammars with integer counters and reset operations on them. Those grammars can alternatively be viewed as an extension of communication-free Petri nets. Our main results are that reachability and coverability are inter-reducible and both NP-complete. In particular, this class of commutative grammars enjoys semi-linear reachability sets. We also show that the inclusion problem is, in general, coNEXP-complete and already $Π_2^\text{P}$-complete for grammars with only one non-terminal symbol. Showing the lower bound for the latter result requires us to develop a novel $Π_2^\text{P}$-complete variant of the classic subset sum problem.
△ Less
Submitted 24 June, 2016; v1 submitted 16 November, 2015;
originally announced November 2015.
-
Integer Vector Addition Systems with States
Authors:
Christoph Haase,
Simon Halfon
Abstract:
This paper studies reachability, coverability and inclusion problems for Integer Vector Addition Systems with States (ZVASS) and extensions and restrictions thereof. A ZVASS comprises a finite-state controller with a finite number of counters ranging over the integers. Although it is folklore that reachability in ZVASS is NP-complete, it turns out that despite their naturalness, from a complexity…
▽ More
This paper studies reachability, coverability and inclusion problems for Integer Vector Addition Systems with States (ZVASS) and extensions and restrictions thereof. A ZVASS comprises a finite-state controller with a finite number of counters ranging over the integers. Although it is folklore that reachability in ZVASS is NP-complete, it turns out that despite their naturalness, from a complexity point of view this class has received little attention in the literature. We fill this gap by providing an in-depth analysis of the computational complexity of the aforementioned decision problems. Most interestingly, it turns out that while the addition of reset operations to ordinary VASS leads to undecidability and Ackermann-hardness of reachability and coverability, respectively, they can be added to ZVASS while retaining NP-completness of both coverability and reachability.
△ Less
Submitted 28 July, 2014; v1 submitted 10 June, 2014;
originally announced June 2014.