SearcharxivSearch

arXiv subjects

Philippe Schnoebelen

Publications and source records attributed to Philippe Schnoebelen.

At least 19 recordsLinked to original sources

On Ordinal Invariants in Well Quasi Orders and Finite Antichain Orders

We investigate the ordinal invariants height, length, and width of well quasi orders (WQO), with particular emphasis on width, an invariant of interest for the larger class of orders with finite antichain condition (FAC). We show that the width in the class of FAC orders is completely determined by the width in the class of WQOs, in the sense that if we know how to calculate the width of any WQO then we have a procedure to calculate the width of any given FAC order. We show how the width of WQO orders obtained via some classical constructions can sometimes be computed in a compositional way. In particular, this allows proving that every ordinal can be obtained as the width of some WQO poset. One of the difficult questions is to give a complete formula for the width of Cartesian products of WQOs. Even the width of the product of two ordinals is only known through a complex recursive formula. Although we have not given a complete answer to this question we have advanced the state of knowledge by considering some more complex special cases and in particular by calculating the width of certain products containing three factors. In the course of writing the paper we have discovered that some of the relevant literature was written on cross-purposes and some of the notions re-discovered several times. Therefore we also use the occasion to give a unified presentation of the known results. ERRATUM:We incorrectly claimed in Lemma 4.4(1) the formula $o(P\cdot Q)=o(P)\cdot o(Q)$ for wpos $P$ and $Q$ and incorrectly attributed it to Abraham and Bonnet. We incorrectly claimed in 4.4(2) that the formula for $h(P\cdot Q)$ was due to Abraham and Bonnet.

math.LO

On the piecewise complexity of words

The piecewise complexity $h(u)$ of a word is the minimal length of subwords needed to exactly characterise $u$. Its piecewise minimality index $ρ(u)$ is the smallest length $k$ such that $u$ is minimal among its order-$k$ class $[u]_k$ in Simon's congruence. We initiate a study of these two descriptive complexity measures. Among other results we provide efficient algorithms for computing $h(u)$ and $ρ(u)$ for a given word $u$.

cs.FL

Measuring well quasi-ordered finitary powersets

The complexity of a well-quasi-order (wqo) can be measured through three ordinal invariants: the width as a measure of antichains, height as a measure of chains, and maximal order type as a measure of bad sequences. We study these ordinal invariants for the finitary powerset, i.e., the collection Pf(A) of finite subsets of a wqo A ordered with the Hoare embedding relation. We show that the invariants of Pf(A) cannot be expressed as a function of the invariants of A, and provide tight upper and lower bounds for them. We then focus on a family of well-behaved wqos, for which these invariants can be computed compositionally, using a newly defined ordinal invariant called the approximate maximal order type. This family is built from multiplicatively indecomposable ordinals, using classical operations such as disjoint unions, products, finite words, finite multisets, and the finitary powerset construction.

cs.LO

On the piecewise complexity of words and periodic words

The piecewise complexity $h(u)$ of a word is the minimal length of subwords needed to exactly characterise $u$. Its piecewise minimality index $ρ(u)$ is the smallest length $k$ such that $u$ is minimal among its order-$k$ class $[u]_k$ in Simon's congruence. We study these two measures and provide efficient algorithms for computing $h(u)$ and $ρ(u)$. We also provide efficient algorithms for the case where $u$ is a periodic word, of the form $u=v^n$

cs.FL

On arch factorization and subword universality for words and compressed words

Using arch-jumping functions and properties of the arch factorization of words, we propose a new algorithm for computing the subword circular universality index of words. We also introduce the subword universality signature for words, that leads to simple algorithms for the universality indexes of SLP-compressed words.

cs.FL

Decidability, Complexity, and Expressiveness of First-Order Logic Over the Subword Ordering

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.

cs.LO

On flat lossy channel machines

We show that reachability, repeated reachability, nontermination and unboundedness are NP-complete for Lossy Channel Machines that are flat, i.e., with no nested cycles in the control graph. The upper complexity bound relies on a fine analysis of iterations of lossy channel actions and uses compressed word techniques for efficiently reasoning with paths of exponential lengths. The lower bounds already apply to acyclic or single-path machines.

cs.LO

The height of piecewise-testable languages and the complexity of the logic of subwords

The height of a piecewise-testable language $L$ is the maximum length of the words needed to define $L$ by excluding and requiring given subwords. The height of $L$ is an important descriptive complexity measure that has not yet been investigated in a systematic way. This article develops a series of new techniques for bounding the height of finite languages and of languages obtained by taking closures by subwords, superwords and related operations. As an application of these results, we show that $\mathsf{FO}^2(A^*,\sqsubseteq)$, the two-variable fragment of the first-order logic of sequences with the subword ordering, can only express piecewise-testable properties and has elementary complexity.

cs.LO

The Ideal Approach to Computing Closed Subsets in Well-Quasi-Ordering

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.

cs.LO

On shuffle products, acyclic automata and piecewise-testable languages

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$.

cs.FL

On the state complexity of closures and interiors of regular languages with subwords and superwords

The downward and upward closures of a regular language $L$ are obtained by collecting all the subwords and superwords of its elements, respectively. The downward and upward interiors of $L$ are obtained dually by collecting words having all their subwords and superwords in $L$, respectively. We provide lower and upper bounds on the size of the smallest automata recognizing these closures and interiors. We also consider the computational complexity of decision problems for closures of regular languages.

cs.FL

Decidability in the logic of subsequences and supersequences

We consider first-order logics of sequences ordered by the subsequence ordering, aka sequence embedding. We show that the Σ_2 theory is undecidable, answering a question left open by Kuske. Regarding fragments with a bounded number of variables, we show that the FO2 theory is decidable while the FO3 theory is undecidable.

cs.LO

On Reachability for Unidirectional Channel Systems Extended with Regular Tests

"Unidirectional channel systems" (Chambart & Schnoebelen, CONCUR 2008) are finite-state systems where one-way communication from a Sender to a Receiver goes via one reliable and one unreliable unbounded fifo channel. While reachability is decidable for these systems, equipping them with the possibility of testing regular properties on the contents of channels makes it undecidable. Decidability is preserved when only emptiness and nonemptiness tests are considered: the proof relies on an elaborate reduction to a generalized version of Post's Embedding Problem.

cs.LO

The Power of Priority Channel Systems

We introduce Priority Channel Systems, a new class of channel systems where messages carry a numeric priority and where higher-priority messages can supersede lower-priority messages preceding them in the fifo communication buffers. The decidability of safety and inevitability properties is shown via the introduction of a priority embedding, a well-quasi-ordering that has not previously been used in well-structured systems. We then show how Priority Channel Systems can compute Fast-Growing functions and prove that the aforementioned verification problems are $\mathbf{F}_{\varepsilon_{0}}$-complete.

cs.LO

Generalized Post Embedding Problems

The Regular Post Embedding Problem extended with partial (co)directness is shown decidable. This extends to universal and/or counting versions. It is also shown that combining directness and codirectness in Post Embedding problems leads to undecidability.

cs.LO

The Power of Well-Structured Systems

Well-structured systems, aka WSTSs, are computational models where the set of possible configurations is equipped with a well-quasi-ordering which is compatible with the transition relation between configurations. This structure supports generic decidability results that are important in verification and several other fields. This paper recalls the basic theory underlying well-structured systems and shows how two classic decision algorithms can be formulated as an exhaustive search for some "bad" sequences. This lets us describe new powerful techniques for the complexity analysis of WSTS algorithms. Recently, these techniques have been successful in precisely characterising the power, in a complexity-theoretical sense, of several important WSTS models like unreliable channel systems, monotonic counter machines, or networks of timed systems.

cs.LO

Solving Stochastic Büchi Games on Infinite Arenas with a Finite Attractor

We consider games played on an infinite probabilistic arena where the first player aims at satisfying generalized Büchi objectives almost surely, i.e., with probability one. We provide a fixpoint characterization of the winning sets and associated winning strategies in the case where the arena satisfies the finite-attractor property. From this we directly deduce the decidability of these games on probabilistic lossy channel systems.

cs.LO