  Hyperproperties lift conventional trace properties from a set of execution
traces to a set of sets of execution traces. Hyperproperties have been shown to
be a powerful formalism for expressing and reasoning about information-flow
security policies and important properties of cyber-physical systems such as
sensitivity and robustness, as well as consistency conditions in distributed
computing such as linearizability. Although there is an extensive body of work
on automata-based representation of trace properties, we currently lack such
characterization for hyperproperties. We introduce hyperautomata for em
hyperlanguages, which are languages over sets of words. Essentially,
hyperautomata allow running multiple quantified words over an automaton. We
propose a specific type of hyperautomata called nondeterministic finite
hyperautomata (NFH), which accept regular hyperlanguages. We demonstrate the
ability of regular hyperlanguages to express hyperproperties for finite traces.
We then explore the fundamental properties of NFH and show their closure under
the Boolean operations. We show that while nonemptiness is undecidable in
general, it is decidable for several fragments of NFH. We further show the
decidability of the membership problem for finite sets and regular languages
for NFH, as well as the containment problem for several fragments of NFH.
Finally, we introduce learning algorithms based on Angluin's L-star algorithm
for the fragments NFH in which the quantification is either strictly universal
or strictly existential.
