REVIEW 1 cited by
HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties
Not yet reviewed by Pith; the record is open.
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
HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties
read the original abstract
In this paper, we propose a new logic for expressing and reasoning about probabilistic hyperproperties. Hyperproperties characterize the relation between different independent executions of a system. Probabilistic hyperproperties express quantitative dependencies between such executions. The standard temporal logics for probabilistic systems, i.e., PCTL and PCTL* can refer only to a single path at a time and, hence, cannot express many probabilistic hyperproperties of interest. The logic proposed in this paper, \HyperPCTL, adds explicit and simultaneous quantification over multiple traces to PCTL. Such quantification allows expressing probabilistic hyperproperties. A model checking algorithm for the proposed logic is also given for discrete-time Markov chains.
Forward citations
Cited by 1 Pith paper
-
Disintegration Temporal Logic for Probabilistic Hyperproperties
DTL is a new probabilistic temporal logic expressing conditional-independence hyperproperties, with a PTIME linear fragment and an automata-theoretic qualitative fragment.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.