Temporal Logics for Hyperproperties
Logic in Computer Science
2014-01-22 v2
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.
Keywords
Cite
@article{arxiv.1401.4492,
title = {Temporal Logics for Hyperproperties},
author = {Michael R. Clarkson and Bernd Finkbeiner and Masoud Koleini and Kristopher K. Micinski and Markus N. Rabe and César Sánchez},
journal= {arXiv preprint arXiv:1401.4492},
year = {2014}
}