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

Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60) 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

Cites work

Cited in

(39)

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)