A temporal logic for asynchronous hyperproperties

DOI10.1007/978-3-030-81685-8_33MaRDI QIDQ832224zbMATH OpenOpenAlexFDO

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

Publication date 25 March 2022

Copyright license Creative Commons Attribution 4.0 International

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

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)

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.

Recommendations

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

Cites work

• scientific article; zbMATH DE number 5595162 (Why is no real title available?)
• A per model of secure information flow in sequential programs
• A variant of a recursively unsolvable problem
• Algorithms for model checking HyperLTL and HyperCTL\(^*\)
• Bounded model checking for hyperproperties
• Defining liveness
• Temporal verification of reactive systems: response
• The first-order logic of hyperproperties
• Verifying hyperliveness
• Witnessing secure compilation

Cited in

(22)

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

Describes a project that uses

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)