Realizing Omega-regular Hyperproperties

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 $\omega$-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 $\omega$-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 $\omega$-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. More specifically, the HyperQPTL fragment of formulas with a universal-existential propositional quantifier alternation followed by a single trace quantifier is undecidable in general, even though the projection of the fragment to HyperLTL has a decidable realizability problem. Lastly, we implemented the bounded synthesis problem for HyperQPTL in the prototype tool BoSy. Using BoSy with HyperQPTL specifications, we have been able to synthesize several resource arbiters. The synthesis problem of non-linear-time hyperlogics is still open. For example, it is not yet known how to synthesize systems from specifications given in branching-time hyperlogics like HyperCTL$^*$.