Pith. sign in

REVIEW 1 cited by

Temporal Logics for Hyperproperties

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 1401.4492 v2 pith:7XLTADOZ submitted 2014-01-17 cs.LO

Temporal Logics for Hyperproperties

Michael R. Clarkson , Bernd Finkbeiner , Masoud Koleini , Kristopher K. Micinski , Markus N. Rabe , C\'esar S\'anchez This is my paper
classification cs.LO
keywords hyperpropertieslogicsproposedhyperltlmodelpathsquantificationtemporal
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved
0 comments
read the original abstract

Two new logics for verification of hyperproperties are proposed. Hyperproperties characterize security policies, such as noninterference, as a property of sets of computation paths. Standard temporal logics such as LTL, CTL, and CTL* can refer only to a single path at a time, hence cannot express many hyperproperties of interest. The logics proposed here, HyperLTL and HyperCTL*, add explicit and simultaneous quantification over multiple paths to LTL and to CTL*. This kind of quantification enables expression of hyperproperties. A model checking algorithm for the proposed logics is given. For a fragment of HyperLTL, a prototype model checker has been implemented.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Disintegration Temporal Logic for Probabilistic Hyperproperties

    cs.LO 2026-07 conditional novelty 8.0

    DTL is a new probabilistic temporal logic expressing conditional-independence hyperproperties, with a PTIME linear fragment and an automata-theoretic qualitative fragment.