DE GRUYTER OLDENBOURG it – Information Technology 2014; 56(6): 273–279 Special Issue

The linear-hyper-branching spectrum of temporal logics Abstract: The family of temporal logics has recently been extended with logics for the specification of hyperproper-ties, such as noninterference or observational determin-ism.Hyperproperties relatemultiple computation paths of a system by requiring that they satisfy a certain relation-ship, such as an identical valuation of the low-security outputs. Unlike classic temporal logics like LTL or CTL*, which refer to one computation path at a time, temporal logics for hyperproperties like HyperLTL and HyperCTL* can express such relationships by explicitly quantifying over multiple computation paths simultaneously. In this paper, we study the extended spectrum of temporal log-ics by relating the new logics to the linear-branching spec-trum of process equivalences