A temporal logic for asynchronous hyperproperties
From MaRDI portal
Publication:832224
DOI10.1007/978-3-030-81685-8_33zbMath1493.68205arXiv2104.14025OpenAlexW3184417962MaRDI QIDQ832224
Jan Baumeister, Norine Coenen, César Sánchez, Borzoo Bonakdarpour, Bernd Finkbeiner
Publication date: 25 March 2022
Full work available at URL: https://arxiv.org/abs/2104.14025
Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Temporal logic (03B44)
Related Items
Flavors of sequential information flow, HyperPCTL model checking by probabilistic decomposition, HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems, Unnamed Item, Finite-word hyperlanguages
Uses Software
Cites Work
- Unnamed Item
- Witnessing secure compilation
- Defining liveness
- Algorithms for model checking HyperLTL and HyperCTL\(^*\)
- Bounded model checking for hyperproperties
- Temporal Verification of Reactive Systems: Response
- The First-Order Logic of Hyperproperties
- A variant of a recursively unsolvable problem
- A per model of secure information flow in sequential programs
- Verifying hyperliveness