Coalgebraic Nominal Automata with Name Allocation

点击翻译按钮获取中文摘要

While formal language theory classically works with finite alphabets, there has been increasing recent interest in languages over infinite alphabets, which may be used to model values from infinite data types such as strings or natural numbers. There is, by now, a wide variety of formalisms for data languages in this sense, aimed at specifying and verifying properties of structures and processes that carry or exchange data, such as XML documents, cryptographic protocols, or dynamically configured parallel processes. Many such formalisms feature registers, in which data values encountered in a data word can be stored for comparison with data values seen later. Register automata in this sense have turned out to be equivalent to more recently developed nominal automata models, which arise by transferring the standard concept of finite automata from sets in the usual sense to sets with atoms (referred to as names). A challenge widely encountered in formalisms for data languages is that central reasoning problems, notably the language inclusion problem, exhibit nonelementary computational complexity or even undecidability unless stringent limitations are imposed on either computational power (e.g. restricting to deterministic or unambiguous models) or on the number of registers. In our own recent research, we have identified a fairly mild trade-off in expressiveness that alleviates this problem. Specifically, we have introduced name-allocating automata models, in which freshness of data values is modelled in the nominal setting using the standard notion of alpha-equivalence, i.e. renaming of bound names. Name-allocating nominal automata models on both finite and infinite words allow inclusion checking in comparatively moderate (in particular, elementary) complexity even in presence of full nondeterminism and unboundedly many registers, with fairly reasonable restrictions on expressiveness (e.g. they can accept the language "some data value occurs twice", which is not acceptable by deterministic or unambiguous register automata). The aim of the CoNAN project is a full development of the algorithmics and meta-theory of name-allocating automata in terms of both scope and depth. Specific research goals include the design of name-allocating temporal logics; the development of algebraic and game-theoretic methods for the analysis of the algorithmics and expressiveness of name-allocating logics and automata models; and extension of the framework to automata models featuring additional expressive means such as name deallocation and branching types beyond nondeterminism. We thus aim to provide a comprehensive body of methods and algorithms for a wide range of data languages.