Regular Cost Functions over Finite Trees

We develop the theory of regular cost functions over finite trees: a quantitative extension to the notion of regular languages of trees: Cost functions map each input (tree) to a value in + 1, and are considered modulo an equivalence relation which forgets about specific values, but preserves boundedness of functions on all subsets of the domain. We introduce nondeterministic and alternating finite tree cost automata for describing cost functions. We show that all these forms of automata are effectively equivalent. We also provide decision procedures for them. Finally, following B

• Type: Journal
• Year: 2010
• Where: LICS
• Authors: Thomas Colcombet, Christof Löding
• Keywords: Automated Reasoning, Cost Functions, Decision Procedures, LICS 2010, Quantitative Extension