Advanced Models and Techniques for Data Languages

Formal languages over infinite alphabets, known as data languages, can be used for processes carrying data. In general, automata models over such infinite alphabets, such as classical register automata or, equivalently, nominal orbit-finite automata, have computationally hard or even undecidable reasoning problems unless stringent restrictions are imposed on either the power of control, the number of registers, or the expressivity of the model. In the present work, we introduce positive data languages which are languages over an infinite alphabet closed under possibly non-injective renamings of data values. Informally, they model properties of data words expressible by assertions of equality, but not inequality, of data values occurring in the word. We investigate the class of positive data languages which are recognisable by non-deterministic nominal orbit-finite automata and provide a number of equivalent characterisations of this class in terms of positive register automata, monadic second-order logic with positive equality tests, and non-deterministic automata in specific categories. We show that for this restriction of data languages the inclusion, universality and equivalence problem have elementary complexity even when the number of registers is unbounded. Next to positive data languages, we also look at automata models with explicit name binding. It was shown that for such models many reasoning problems have elementary complexity without bound on the number of registers. We demonstrate that elementary complexity survives under extending the power of control to alternation: We introduce regular alternating nominal automata (RANAs), and show that their non-emptiness and inclusion problems are decidable in exponential space. Moreover, we show that RANAs allow for nearly complete de-alternation, specifically de-alternation up to a single deadlocked universal state. As a corollary to our results, we improve the complexity of model checking for nominal fixed-point logic with name binding over finite data words, by one exponential level. Lastly, we introduce active learning methods for such automata. We develop a framework in which every learning algorithm for standard deterministic or non-deterministic finite automata over finite alphabets can be used to learn these automata with explicit name binding, with a query complexity determined by that of the chosen learner. For this, we develop an algorithmic handling of -equivalence of bar strings, which allows to bridge the gap between finite and infinite alphabets. The principles underlying our framework are generic and also apply to nominal automata with explicit name binding for infinite bar strings and bar trees, leading to the first active learning methods for data languages of infinite words and finite trees.