Source author record

Luc Dartois

Luc Dartois appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record

Formal Languages and Automata Theory Logic in Computer Science

Catalog footprint

What is connected

6works

2topics

4close collaborators

Actions

Connect this record

Open graph Browse works

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

preprint2022arXiv

Efficient Construction of Reversible Transducers from Regular Transducer Expressions

The class of regular transformations has several equivalent characterizations such as functional MSO transductions, deterministic two-way transducers, streaming string transducers, as well as regular transducer expressions (RTE). For algorithmic applications, it is very common and useful to transform a specification, here, an RTE, to a machine, here, a transducer. In this paper, we give an efficient construction of a two-way reversible transducer (2RFT) equivalent to a given RTE. 2RFTs are a well behaved class of transducers which are deterministic and co-deterministic (hence allows evaluation in linear time \wrt the input word), and where composition has only polynomial complexity. We show that, for full RTE, the constructed 2RFT has size doubly exponential in the size of the expression, while, if the RTE does not use Hadamard product or chained-star, the constructed 2RFT has size exponential in the size of the RTE.

preprint2021arXiv

SD-Regular Transducer Expressions for Aperiodic Transformations

FO transductions, aperiodic deterministic two-way transducers, as well as aperiodic streaming string transducers are all equivalent models for first order definable functions. In this paper, we solve the long standing open problem of expressions capturing first order definable functions, thereby generalizing the seminal SF=AP (star free expressions = aperiodic languages) result of Schützenberger. Our result also generalizes a lesser known characterization by Schützenberger of aperiodic languages by SD-regular expressions (SD=AP). We show that every first order definable function over finite words captured by an aperiodic deterministic two-way transducer can be described with an SD-regular transducer expression (SDRTE). An SDRTE is a regular expression where Kleene stars are used in a restricted way: they can appear only on aperiodic languages which are prefix codes of bounded synchronization delay. SDRTEs are constructed from simple functions using the combinators unambiguous sum (deterministic choice), Hadamard product, and unambiguous versions of the Cauchy product and the k-chained Kleene-star, where the star is restricted as mentioned. In order to construct an SDRTE associated with an aperiodic deterministic two-way transducer, (i) we concretize Schützenberger's SD=AP result, by proving that aperiodic languages are captured by SD-regular expressions which are unambiguous and stabilising; (ii) by structural induction on the unambiguous, stabilising SD-regular expressions describing the domain of the transducer, we construct SDRTEs. Finally, we also look at various formalisms equivalent to SDRTEs which use the function composition, allowing to trade the k-chained star for a 1-star.

preprint2016arXiv

Aperiodic String Transducers

Regular string-to-string functions enjoy a nice triple characterization through deterministic two-way transducers (2DFT), streaming string transducers (SST) and MSO definable functions. This result has recently been lifted to FO definable functions, with equivalent representations by means of aperiodic 2DFT and aperiodic 1-bounded SST, extending a well-known result on regular languages. In this paper, we give three direct transformations: i) from 1-bounded SST to 2DFT, ii) from 2DFT to copyless SST, and iii) from k-bounded to 1-bounded SST. We give the complexity of each construction and also prove that they preserve the aperiodicity of transducers. As corollaries, we obtain that FO definable string-to-string functions are equivalent to SST whose transition monoid is finite and aperiodic, and to aperiodic copyless SST.

preprint2016arXiv

Two-Way Visibly Pushdown Automata and Transducers

Automata-logic connections are pillars of the theory of regular languages. Such connections are harder to obtain for transducers, but important results have been obtained recently for word-to-word transformations, showing that the three following models are equivalent: deterministic two-way transducers, monadic second-order (MSO) transducers, and deterministic one-way automata equipped with a finite number of registers. Nested words are words with a nesting structure, allowing to model unranked trees as their depth-first-search linearisations. In this paper, we consider transformations from nested words to words, allowing in particular to produce unranked trees if output words have a nesting structure. The model of visibly pushdown transducers allows to describe such transformations, and we propose a simple deterministic extension of this model with two-way moves that has the following properties: i) it is a simple computational model, that naturally has a good evaluation complexity; ii) it is expressive: it subsumes nested word-to-word MSO transducers, and the exact expressiveness of MSO transducers is recovered using a simple syntactic restriction; iii) it has good algorithmic/closure properties: the model is closed under composition with a unambiguous one-way letter-to-letter transducer which gives closure under regular look-around, and has a decidable equivalence problem.

preprint2015arXiv

Adding modular predicates to first-order fragments

We investigate the decidability of the definability problem for fragments of first order logic over finite words enriched with modular predicates. Our approach aims toward the most generic statements that we could achieve, which successfully covers the quantifier alternation hierarchy of first order logic and some of its fragments. We obtain that deciding this problem for each level of the alternation hierarchy of both first order logic and its two-variable fragment when equipped with all regular numerical predicates is not harder than deciding it for the corresponding level equipped with only the linear order and the successor. For two-variable fragments we also treat the case of the signature containing only the order and modular predicates.Relying on some recent results, this proves the decidability for each level of the alternation hierarchy of the two-variable first order fragmentwhile in the case of the first order logic the question remains open for levels greater than two.The main ingredients of the proofs are syntactic transformations of first order formulas as well as the algebraic framework of finite categories.

preprint2010arXiv

Rankers over Infinite Words

We consider the four fragments FO2, the intersection of Sigma2 and FO2, the intersection of Pi2 and FO2, and Delta2 of first-order logic FO[<] over finite and infinite words. For all four fragments, we give characterizations in terms of rankers. In particular, we generalize the notion of a ranker to infinite words in two possible ways. Both extensions are natural in the sense that over finite words, they coincide with classical rankers and over infinite words, they both have the full expressive power of FO2. Moreover, the first extension of rankers admits a characterization of the intersection of Sigma2 and FO2 while the other leads to a characterization of the intersection of Pi2 and FO2. Both versions of rankers yield characterizations of the fragment Delta2. As a byproduct, we also obtain characterizations based on unambiguous temporal logic and unambiguous interval temporal logic.