(Asynchronous) Temporal Logics for Hyperproperties on Finite Traces

Hyperproperties are properties of systems that relate more than one trace, which are common in information-flow, concurrency, symmetry, diagnosability, etc. Several temporal logics for hyperproperties have been proposed—like HyperLTL and HyperCTL* where traces are compared synchronously—and recently extended for comparing traces asynchronously. However, all these temporal hyperlogics are for infinite traces, in spite of the recent popularity of temporal logics on finite traces.In this paper, we introduce SC-HyperLTL, a logic for asynchronous hyperproperties on finite traces and with past operators, by adapting and combining two existing logics for asynchronous hyperproperties: stuttering HyperLTL () and context HyperLTL (). We show that SC-HyperLTL is decidable and can encode many hyperproperties of interest. We present two practical algorithms that reduce the model checking problem of SC-HyperLTL to inputs of two existing tools: AutoHyper (which can model check hyperproperties on infinite traces) and nuXmv (a model checker for trace properties). We illustrate our algorithms on a prototype implementation.