text: Motivated by the successful application of the theory of regular languages to formal verification of finite-state systems, there is a renewed interest in developing a theory of analyzable functions from strings to numerical values that can provide a foundation for analyzing quantitative properties of finitestate systems. In this paper, we propose a deterministic model for associating costs with strings that is parameterized by operations of interest (such as addition, scaling, and min), a notion of regularity that provides a yardstick to measure expressiveness, and study decision problems and theoretical properties of resulting classes of cost functions. Our definition of regularity relies on the theory of string-to-tree transducers, and allows associating costs with events that are conditional upon regular properties of future events. Our model of cost register automata allows computation of regular functions using multiple “write-only” registers whose values can be combined using the allowed set of operations. We show that classical shortest-path algorithms as well as algorithms designed for computing discounted costs, can be adopted for solving the min-cost problems for the more general classes of functions specified in our model. Cost register automata with min and increment give a deterministic model that is equivalent to weighted automata, an extensively studied nondeterministic model, and this connection results in new insights and new open problems.
  @cite_35: Two well-known formalisms for the specification and computation of tree transductions are compared: the mso graph transducer and the attributed tree transducer with look-ahead, respectively. The mso graph transducer, restricted to trees, uses monadic second order logic to define the output tree in terms of the input tree. The attributed tree transducer is an attribute grammar in which all attributes are trees; it is preceded by a look-ahead phase in which all attributes have finitely many values. The main result is that these formalisms are equivalent, i.e., that the attributed tree transducer with look-ahead is an appropriate implementation model for the tree transductions that are specifiable in mso logic. This result holds for mso graph transducers that produce trees with shared subtrees. If no sharing is allowed, the attributed tree transducer satisfies the single use restriction.
  @cite_8: Abstract This lecture surveys about 15 years of research about context-free graph grammars, graph operations, graph transformations and monadic second-order logic done in cooperation with participants of the European network GETGRATS and of previous European projects related with graph grammars and graph transformations.
  @cite_3: A characterization is given of the class of tree translations definable in monadic second-order logic (MSO), in terms of macro tree transducers. The first main result is that the MSO definable tree translations are exactly those tree translations realized by macro tree transducers (MTTs) with regular look-ahead that are single use restricted. For this the single use restriction known from attribute grammars is generalized to MTTs. Since MTTs are closed under regular look-ahead, this implies that every MSO definable tree translation can be realized by an MTT. The second main result is that the class of MSO definable tree translations can also be obtained by restricting MTTs with regular look-ahead to be finite copying, i.e., to require that each input subtree is processed only a bounded number of times. The single use restriction is a rather strong, static restriction on the rules of an MTT, whereas the finite copying restriction is a more liberal, dynamic restriction on the derivations of an MTT.
  @cite_2: We extend a classic result of Buchi, Elgot, and Trakhtenbrot: MSO definable string transductions i.e., string-to-string functions that are definable by an interpretation using monadic second-order (MSO) logic, are exactly those realized by deterministic two-way finite-state transducers, i.e., finite-state automata with a two-way input tape and a one-way output tape. Consequently, the equivalence of two mso definable string transductions is decidable. In the nondeterministic case however, MSO definable string tranductions, i.e., binary relations on strings that are mso definable by an interpretation with parameters, are incomparable to those realized by nondeterministic two-way finite-state transducers. This is a motivation to look for another machine model, and we show that both classes of MSO definable string transductions are characterized in terms of Hennie machines, i.e., two-way finite-state transducers that are allowed to rewrite their input tape, but may visit each position of their input only a bounded number of times.
  @cite_5: Macro tree transducers are a combination of top-down tree transducers and macro grammars. They serve as a model for syntax-directed semantics in which context information can be handled. In this paper the formal model of macro tree transducers is studied by investigating typical automata theoretical topics like composition, decomposition, domains, and ranges of the induced translation classes. The extension with regular look-ahead is considered.
summary: A wide variety of different models have been proposed to model string and tree transductions. The models that are most relevant to this paper are MSO-definable transductions @cite_8 @cite_2 and macro tree transducers @cite_5 @cite_3 . An MSO-definable graph transduction specifies a function between sets of graphs; the nodes, edges and labels of the output graph are described in terms of MSO formulas over the nodes, edges and labels of a finite number of copies of the input graph. A macro tree transducer (MTT) is a top-down tree to tree transducer equipped with parameters. Parameters can store temporary trees and append them to the final tree during the computation. In general, MTT are more expressive than MSO-definable tree transductions. A subclass of MTTs obtained by restricting the number of times a subtree and a parameter can be used has been shown to be equi-expressive as MSO-definable tree transductions @cite_3 . In addition to these models, formalisms such as attribute grammars @cite_3 , attribute tree transducers @cite_35 have also been studied.