On the Hierarchy of Finite-Word Hyperlanguages

Abstract

Hyperproperties lift conventional properties, which reason about traces, to properties that reason about sets of traces. Their formal-language counterpart are hyperlanguages, which are sets of languages. Several formalisms for hyperlanguages have been defined and studied: hyperautomata and context-free hypergrammars lift the notions of regular and context-free languages to regular hyperlanguages and context-free hyperlanguages, respectively. We unify and generalize these notions, and define general hypermodels, for both synchronous and asynchronous semantics. We then proceed to study the Chomsky hierarchy for hyperlanguages. In this setting, we study the relations within each semantic separately, as well as between the semantics. We show that both synchronous and asynchronous semantics follows the standard Chomsky hierarchy, separately. We further study the relations between the different levels of the hierarchy over the two semantics, and show them to be incomparable.