Realizing -regular hyperproperties

DOI10.1007/978-3-030-53291-8_4MaRDI QIDQ2226720zbMATH OpenOpenAlexFDO

Authors Bernd Finkbeiner, Christopher Hahn, Jana Hofmann, Leander Tentrup

Publication date 9 February 2021

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2101.07161

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

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${}^{\ast }$.

Recommendations

• Synthesis from hyperproperties
• Synthesizing reactive systems from hyperproperties
• Model checking algorithms for hyperproperties (invited paper)
• Temporal hyperproperties
• scientific article; zbMATH DE number 6851935

Cited in

(4)

• Realizable and context-free hyperlanguages
• A semantic model for interacting cyber-physical systems
• Synthesis from hyperproperties
• Model checking algorithms for hyperproperties (invited paper)

This page was built for publication: Realizing \(\omega\)-regular hyperproperties

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2226720)