Presenter
Franziska Alber
University of Regensburg
Authors
Franziska Alber, Philipp Rümmer
Abstract
Variable Automata (VA) are an extension of finite-state automata to infinite alphabets, where transition labels represent non-reassignable variables, allowing for the comparison of input letters. VA are applied in the modelling of systems that require unbounded data domains, such as sequence solving or XML documents with data values. The increased expressiveness comes at a price, as the universality problem (i.e., deciding whether a VA accepts all possible words over a fixed alphabet) is undecidable for VA. Our research is motivated by the close relationship between the universality problem and the complementation of languages, an operation that is often required in verification. We have shown that the universality problem is decidable when restricted to VA over a single variable, and will present the key ideas behind the construction in this talk.
Slides
TBA