  Formal languages are in the core of models of computation and their behavior.
A rich family of models for many classes of languages have been widely studied.
Hyperproperties lift conventional trace-based languages from a set of execution
traces to a set of sets of executions. 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. Although there is
an extensive body of work on formal-language representation of trace
properties, we currently lack such a general characterization for
hyperproperties. We introduce hyperlanguages over finite words and models for
expressing them. Essentially, these models express multiple words by using
assignments to quantified word variables. Relying on the standard models for
regular languages, we propose hyperregular expressions and finite-word
hyperautomata (NFH), for modeling the class of regular hyperlanguages. We
demonstrate the ability of regular hyperlanguages to express hyperproperties
for finite traces. We explore the closure properties and the complexity of the
fundamental decision problems such as nonemptiness, universality, membership,
and containment for various fragments of NFH.
