Finite-Word Hyperlanguages

TL;DR

This paper introduces hyperlanguages over finite words and models such as hyperregular expressions and hyperautomata to represent and analyze hyperproperties, extending formal language theory to sets of traces for security and system properties.

Contribution

It provides a formal framework for finite-word hyperlanguages, including models and decision problems, filling a gap in the characterization of hyperproperties.

Findings

Hyperregular expressions can express hyperproperties of finite traces.

Finite-word hyperautomata (NFH) model regular hyperlanguages.

Decidability results for nonemptiness, universality, membership, and containment.

Abstract

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.