CISPA
Browse
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.

History

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

2020-09-14

Open Access Type

  • Unknown

BibTeX

@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

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC