A temporal logic for asynchronous hyperproperties

DOI10.1007/978-3-030-81685-8_33zbMATH Open1493.68205arXiv2104.14025OpenAlexW3184417962MaRDI QIDQ832224FDOQ832224

Authors: Jan Baumeister, Norine Coenen, Borzoo Bonakdarpour, Bernd Finkbeiner, César Sánchez 

Publication date: 25 March 2022

Abstract: Hyperproperties are properties of computational systems that require more than one trace to evaluate, e.g., many information-flow security and concurrency requirements. Where a trace property defines a set of traces, a hyperproperty defines a set of sets of traces. The temporal logics HyperLTL and HyperCTL* have been proposed to express hyperproperties. However, their semantics are synchronous in the sense that all traces proceed at the same speed and are evaluated at the same position. This precludes the use of these logics to analyze systems whose traces can proceed at different speeds and allow that different traces take stuttering steps independently. To solve this problem in this paper, we propose an asynchronous variant of HyperLTL. On the negative side, we show that the model-checking problem for this variant is undecidable. On the positive side, we identify a decidable fragment which covers a rich set of formulas with practical applications. We also propose two model-checking algorithms that reduce our problem to the HyperLTL model-checking problem in the synchronous semantics.

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

Recommendations

• Temporal hyperproperties
• Model checking algorithms for hyperproperties (invited paper)
• HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties
• On verifying timed hyperproperties
• Synthesis from hyperproperties

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites Work

• Title not available (Why is that?)
• A variant of a recursively unsolvable problem
• Temporal verification of reactive systems: response
• Defining liveness
• A per model of secure information flow in sequential programs
• Witnessing secure compilation
• Algorithms for model checking HyperLTL and HyperCTL\(^*\)
• Bounded model checking for hyperproperties
• The first-order logic of hyperproperties
• Verifying hyperliveness

Cited In (22)

• Timed hyperproperties
• HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems
• Software Verification of Hyperproperties Beyond k-Safety
• Temporal hyperproperties
• The first-order logic of hyperproperties
• Efficient loop conditions for bounded model checking hyperproperties
• Unifying hyper and epistemic temporal logics
• Bounded model checking for asynchronous hyperproperties
• On verifying timed hyperproperties
• A remark on the expressivity of asynchronous TeamLTL and HyperLTL
• Synthesis from hyperproperties
• HyperPCTL model checking by probabilistic decomposition
• Flavors of sequential information flow
• Deciding hyperproperties combined with functional specifications
• Temporal team semantics revisited
• Realizable and context-free hyperlanguages
• Finite-word hyperlanguages
• Asynchronous extensions of hyperLTL
• Concurrent hyperproperties
• Second-order hyperproperties
• Introducing asynchronicity to probabilistic hyperproperties
• Team semantics for the specification and verification of hyperproperties

Uses Software

• ABC

This page was built for publication: A temporal logic for asynchronous hyperproperties

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