(2022) Realizable and Context-Free Hyperlanguages.
|
Text
hyper_grammars-15.pdf - Published Version Download (354kB) | Preview |
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.
Item Type: | Conference or Workshop Item (A Paper) (Paper) |
---|---|
Divisions: | Bernd Finkbeiner (Reactive Systems Group, RSG) |
Conference: | GandALF GandALF - games, automata, logics, and formal methods |
Depositing User: | Hadar Frenkel |
Date Deposited: | 29 Aug 2023 05:07 |
Last Modified: | 29 Aug 2023 05:07 |
Primary Research Area: | NRA1: Trustworthy Information Processing |
URI: | https://publications.cispa.saarland/id/eprint/3818 |
Actions
Actions (login required)
View Item |