(2022) Prophecy Variables for Hyperproperty Verification.
Abstract
Temporal logics for hyperproperties like HyperLTL use trace quantifiers to express properties that relate multiple system runs. In practice, the verification of such specifications is mostly limited to formulas without quantifier alternation, where verification can be reduced to checking a trace property over the self-composition of the system. Quantifier alternations like $\forall \pi. \exists \pi'. \phi$, can either be solved by complementation or with an interpretation as a two-person game between a $\forall$-player, who incrementally constructs the trace $\pi$, and an $\exists$-player, who constructs $\pi'$ in such a way that $\pi$ and $\pi'$ together satisfy $\phi$. The game-based approach is significantly cheaper but incomplete, because the $\exists$-player does not know the future moves of the $\forall$-player. In this paper, we establish that the game-based approach can be made complete by adding ($\omega$-regular) temporal prophecies. Our proof is constructive, yielding an effective algorithm for the generation of a complete set of prophecies. We have implemented this construction in a prototype model checker called HyPro.
| Item Type: | Conference or Workshop Item (A Paper) (Paper) |
|---|---|
| Divisions: | Bernd Finkbeiner (Reactive Systems Group, RSG) |
| Conference: | CSF IEEE Computer Security Foundations Symposium (was CSFW) |
| Depositing User: | Raven Beutner |
| Date Deposited: | 01 Jun 2022 08:19 |
| Last Modified: | 01 Jun 2022 08:23 |
| Primary Research Area: | NRA1: Trustworthy Information Processing |
| URI: | https://publications.cispa.saarland/id/eprint/3705 |
Actions
Actions (login required)
 |
View Item |