Two-Way Visibly Pushdown Automata and Transducers

TL;DR

This paper introduces a simple, expressive, and computationally efficient deterministic two-way visibly pushdown transducer model for nested word transformations, unifying and extending existing models with good algorithmic properties.

Contribution

It proposes a deterministic two-way visibly pushdown transducer model that subsumes nested word MSO transducers and has favorable complexity and closure properties.

Findings

Model is closed under composition with unambiguous transducers

Decidable equivalence problem for the model

Expressiveness matches nested word MSO transducers with restrictions

Abstract

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.