Realizing $$\omega $$-regular Hyperproperties
| Autor: | Leander Tentrup, Christopher Hahn, Bernd Finkbeiner, Jana Hofmann |
|---|---|
| Rok vydání: | 2020 |
| Předmět: |
Model checking
Discrete mathematics 050101 languages & linguistics Computer science 05 social sciences 02 engineering and technology Undecidable problem Decidability Quantifier (logic) Fragment (logic) Realizability Bounded function 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing 0501 psychology and cognitive sciences Boolean satisfiability problem |
| Zdroj: | Computer Aided Verification-32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21–24, 2020, Proceedings, Part II Lecture Notes in Computer Science Lecture Notes in Computer Science-Computer Aided Verification Computer Aided Verification ISBN: 9783030532901 |
| ISSN: | 0302-9743 1611-3349 |
| DOI: | 10.1007/978-3-030-53291-8_4 |
| Popis: | 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$^*$. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|