Realizable and Context-Free Hyperlanguages

TL;DR

This paper investigates the realizability of hyperlanguages using automata, revealing complexity challenges and proposing a refined model to describe non-regular hyperproperties with manageable decidability.

Contribution

It introduces the realizability problem for regular hyperlanguages, explores the undecidability in context-free hyperlanguages, and proposes synchronous hypergrammars as a practical alternative.

Findings

Realizability problem is complex even for singleton hyperlanguages.

Context-free hyperlanguages are highly undecidable.

Synchronous hypergrammars enable describing non-regular hyperproperties with decidable features.

Abstract

Hyperproperties lift conventional trace-based languages from a set of execution traces to a set of sets of executions. From a formal-language perspective, these are sets of sets of words, namely hyperlanguages. Hyperautomata are based on classical automata models that are lifted to handle hyperlanguages. Finite hyperautomata (NFH) have been suggested to express regular hyperproperties. We study the realizability problem for regular hyperlanguages: given a set of languages, can it be precisely described by an NFH? We show that the problem is complex already for singleton hyperlanguages. We then go beyond regular hyperlanguages, and study context-free hyperlanguages. We show that the natural extension to context-free hypergrammars is highly undecidable. We then suggest a refined model, namely synchronous hypergrammars, which enables describing interesting non-regular hyperproperties, while retaining many decidable properties of context-free grammars.