Realizing Omega-regular Hyperproperties
Bernd Finkbeiner, Christopher Hahn, Jana Hofmann, Leander Tentrup

TL;DR
This paper introduces HyperQPTL, a highly expressive hyperlogic capable of expressing omega-regular hyperproperties, explores its theoretical properties including decidability of realizability, and demonstrates practical synthesis applications.
Contribution
The paper presents HyperQPTL, a new hyperlogic with optimal expressiveness for omega-regular hyperproperties, analyzes its model checking and realizability, and implements synthesis in a prototype tool.
Findings
HyperQPTL can express promptness, bounded waiting, and epistemic properties.
Decidability of realizability for certain HyperQPTL fragments is established.
Implemented synthesis of resource arbiters using HyperQPTL in the BoSy tool.
Abstract
We studied the hyperlogic HyperQPTL, which combines the concepts of trace relations and -regularity. We showed that HyperQPTL is very expressive, it can express properties like promptness, bounded waiting for a grant, epistemic properties, and, in particular, any -regular property. Those properties are not expressible in previously studied hyperlogics like HyperLTL. At the same time, we argued that the expressiveness of HyperQPTL is optimal in a sense that a more expressive logic for -regular hyperproperties would have an undecidable model checking problem. We furthermore studied the realizability problem of HyperQPTL. We showed that realizability is decidable for HyperQPTL fragments that contain properties like promptness. But still, in contrast to the satisfiability problem, propositional quantification does make the realizability problem of hyperlogics harder.…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
