Authors: Michael Clarkson, Masoud Koleini, and Kristopher Micinski. Title: HyperLTL Abstract: In this work, we introduce HyperLTL, a logic based on LTL that is capable of expressing security properties, such as noninference, generalized noninterference, and observational determinism. LTL cannot directly express such properties, nor can branching-time logics. But HyperLTL can, because it extends LTL with connectives for explicit quantification over paths and for propositions over multiple paths. We also present ongoing work on a model-checking algorithm to verify HyperLTL formulas. HyperLTL is designed for verification of hyperproperties, a formalism that is complete for expressing security properties. HyperLTL is a step toward a general verification methodology for hyperproperties.