cispa_all_3186.pdf (401.41 kB)

Realizing Omega-regular Hyperproperties

Download (401.41 kB)
Version 2 2023-12-11, 20:12
Version 1 2023-11-29, 18:13
conference contribution
posted on 2023-12-11, 20:12 authored by Bernd FinkbeinerBernd Finkbeiner, Christopher Hahn, Jana Hofmann, Leander Tentrup
We study the expressiveness and reactive synthesis problem of HyperQPTL, a logic that specifies omega-regular hyperproperties. HyperQPTL is an extension of linear-time temporal logic (LTL) with explicit trace and propositional quantification and therefore truly combines trace relations and omega-regularity. As such, HyperQPTL can express promptness, which states that there is a common bound on the number of steps up to which an event must have happened. We demonstrate how the HyperQPTL formulation of promptness differs from the type of promptness expressible in the logic Prompt-LTL. Furthermore, we study the realizability problem of HyperQPTL by identifying decidable fragments, where one decidable fragment contains formulas for promptness. We show that, in contrast to the satisfiability problem of HyperQPTL, propositional quantification has an immediate impact on the decidability of the realizability problem. We present a reduction to the realizability problem of HyperLTL, which immediately yields a bounded synthesis procedure. We implemented the synthesis procedure for HyperQPTL in the bounded synthesis tool BoSy. Our experimental results show that a range of arbiter satisfying promptness can be synthesized.


Preferred Citation

Bernd Finkbeiner, Christopher Hahn, Jana Hofmann and Leander Tentrup. Realizing Omega-regular Hyperproperties. In: Computer Aided Verification (CAV). 2020.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

Computer Aided Verification (CAV)

Legacy Posted Date


Open Access Type

  • Unknown


@inproceedings{cispa_all_3186, title = "Realizing Omega-regular Hyperproperties", author = "Finkbeiner, Bernd and Hahn, Christopher and Hofmann, Jana and Tentrup, Leander", booktitle="{Computer Aided Verification (CAV)}", year="2020", }

Usage metrics


    No categories selected


    Ref. manager