arXiv subjects

Thomas Place

Publications and source records attributed to Thomas Place.

30 records · Page 2Linked to original sources

arXiv2018

A generic characterization of Pol(C)

We investigate the polynomial closure operation (C -> Pol(C)) defined on classes of regular languages. We present an interesting and useful connection relating the separation problem for the class C and the membership problem for it polynomial closure Pol(C). This connection is formulated as an algebraic characterization of Pol(C) which holds when C is an arbitrary \pvari of regular languages and whose statement is parameterized by C-separation. Its main application is an effective reduction from Pol(C)-membership to C-separation. Thus, as soon as one designs a C-separation algorithm, this yields "for free" a membership algorithm for the more complex class Pol(C).

cs.FL↗

arXiv2017

Generic Results for Concatenation Hierarchies

In the theory of formal languages, the understanding of concatenation hierarchies of regular languages is one of the most fundamental and challenging topic. In this paper, we survey progress made in the comprehension of this problem since 1971, and we establish new generic statements regarding this problem.

cs.FL↗

arXiv2017

Adding successor: A transfer theorem for separation and covering

Given a class C of word languages, the C-separation problem asks for an algorithm that, given as input two regular languages, decides whether there exists a third language in C containing the first language, while being disjoint from the second. Separation is usually investigated as a means to obtain a deep understanding of the class C. In the paper, we are mainly interested in classes defined by logical formalisms. Such classes are often built on top of each other: given some logic, one builds a stronger one by adding new predicates to its signature. A natural construction is to enrich a logic with the successor relation. In this paper, we present a transfer result applying to this construction: we show that for suitable logically defined classes, separation for the logic enriched with the successor relation reduces to separation for the original logic. Our theorem also applies to a problem that is stronger than separation: covering. Moreover, we actually present two reductions: one for languages of finite words and the other for languages of infinite words.

cs.FL↗

arXiv2017

Going Higher in First-Order Quantifier Alternation Hierarchies on Words

We investigate quantifier alternation hierarchies in first-order logic on finite words. Levels in these hierarchies are defined by counting the number of quantifier alternations in formulas. We prove that one can decide membership of a regular language in the levels $\mathcal{B}Σ_2$ (finite boolean combinations of formulas having only one alternation) and $Σ_3$ (formulas having only two alternations and beginning with an existential block). Our proofs work by considering a deeper problem, called separation, which, once solved for lower levels, allows us to solve membership for higher levels.

cs.LO↗

arXiv2016

Separating Regular Languages with First-Order Logic

Given two languages, a separator is a third language that contains the first one and is disjoint from the second one. We investigate the following decision problem: given two regular input languages of finite words, decide whether there exists a first-order definable separator. We prove that in order to answer this question, sufficient information can be extracted from semigroups recognizing the input languages, using a fixpoint computation. This yields an EXPTIME algorithm for checking first-order separability. Moreover, the correctness proof of this algorithm yields a stronger result, namely a description of a possible separator. Finally, we generalize this technique to answer the same question for regular languages of infinite words.

cs.FL↗

arXiv2015

Quantifier Alternation for Infinite Words

We investigate the expressive power of quantifier alternation hierarchy of first-order logic over words. This hierarchy includes the classes $Σ_i$ (sentences having at most $i$ blocks of quantifiers starting with an $\exists$) and $\mathcal{B}Σ_i$ (Boolean combinations of $Σ_i$ sentences). So far, this expressive power has been effectively characterized for the lower levels only. Recently, a breakthrough was made over finite words, and decidable characterizations were obtained for $\mathcal{B}Σ_2$ and $Σ_3$, by relying on a decision problem called separation, and solving it for $Σ_2$. The contribution of this paper is a generalization of these results to the setting of infinite words: we solve separation for $Σ_2$ and $Σ_3$, and obtain decidable characterizations of $\mathcal{B}Σ_2$ and $Σ_3$ as consequences.

cs.FL↗

arXiv2015

Deciding definability in FO2(<h,<v) on trees

We provide a decidable characterization of regular forest languages definable in FO2(<h,<v). By FO2(<h,<v) we refer to the two variable fragment of first order logic built from the descendant relation and the following sibling relation. In terms of expressive power it corresponds to a fragment of the navigational core of XPath that contains modalities for going up to some ancestor, down to some descendant, left to some preceding sibling, and right to some following sibling. We also show that our techniques can be applied to other two variable first-order logics having exactly the same vertical modalities as FO2(<h,<v) but having different horizontal modalities.

cs.LO↗

arXiv2015

A Transfer Theorem for the Separation Problem

We investigate two problems for a class C of regular word languages. The C-membership problem asks for an algorithm to decide whether an input language belongs to C. The C-separation problem asks for an algorithm that, given as input two regular languages, decides whether there exists a third language in C containing the first language, while being disjoint from the second. These problems are considered as means to obtain a deep understanding of the class C. It is usual for such classes to be defined by logical formalisms. Logics are often built on top of each other, by adding new predicates. A natural construction is to enrich a logic with the successor relation. In this paper, we obtain simple self-contained proofs of two transfer results: we show that for suitable logically defined classes, the membership, resp. the separation problem for a class enriched with the successor relation reduces to the same problem for the original class. Our reductions work both for languages of finite words and infinite words. The proofs are mostly self-contained, and only require a basic background on regular languages. This paper therefore gives new, simple proofs of results that were considered as difficult, such as the decid- ability of the membership problem for the levels 1, 3/2, 2 and 5/2 of the dot-depth hierarchy.

cs.FL↗

arXiv2014

On Separation by Locally Testable and Locally Threshold Testable Languages

A separator for two languages is a third language containing the first one and disjoint from the second one. We investigate the following decision problem: given two regular input languages, decide whether there exists a locally testable (resp. a locally threshold testable) separator. In both cases, we design a decision procedure based on the occurrence of special patterns in automata accepting the input languages. We prove that the problem is computationally harder than deciding membership. The correctness proof of the algorithm yields a stronger result, namely a description of a possible separator. Finally, we discuss the same problem for context-free input languages.

cs.FL↗

arXiv2014

Going higher in the First-order Quantifier Alternation Hierarchy on Words

We investigate the quantifier alternation hierarchy in first-order logic on finite words. Levels in this hierarchy are defined by counting the number of quantifier alternations in formulas. We prove that one can decide membership of a regular language to the levels $\mathcal{B}Σ_2$ (boolean combination of formulas having only 1 alternation) and $Σ_3$ (formulas having only 2 alternations beginning with an existential block). Our proof works by considering a deeper problem, called separation, which, once solved for lower levels, allows us to solve membership for higher levels.

cs.FL↗

arXiv2013

Separating regular languages by piecewise testable and unambiguous languages

Separation is a classical problem asking whether, given two sets belonging to some class, it is possible to separate them by a set from a smaller class. We discuss the separation problem for regular languages. We give a Ptime algorithm to check whether two given regular languages are separable by a piecewise testable language, that is, whether a $BΣ1(<)$ sentence can witness that the languages are disjoint. The proof refines an algebraic argument from Almeida and the third author. When separation is possible, we also express a separator by saturating one of the original languages by a suitable congruence. Following the same line, we show that one can as well decide whether two regular languages can be separated by an unambiguous language, albeit with a higher complexity.

cs.FL↗

arXiv2011

A decidable characterization of locally testable tree languages

A regular tree language L is locally testable if membership of a tree in L depends only on the presence or absence of some fix set of neighborhoods in the tree. In this paper we show that it is decidable whether a regular tree language is locally testable. The decidability is shown for ranked trees and for unranked unordered trees.

cs.FL↗