Linear temporal logic (LTL) is used in system verification to write formal specifications for reactive systems. However, some relevant properties, e.g. non-inference in information flow security, cannot be expressed in LTL. A class of such properties that has recently received ample attention is known as hyperproperties. There are two major streams in the research regarding capturing hyperproperties, namely hyperlogics, which extend LTL with trace quantifiers (HyperLTL), and logics that employ team semantics, extending truth to sets of traces. In this article we explore the relation between asynchronous LTL under set-based team semantics (TeamLTL) and HyperLTL. In particular we consider the extensions of TeamLTL with the Boolean disjunction and a fragment of the extension of TeamLTL with the Boolean negation, where the negation cannot occur in the left-hand side of the Until-operator or within the Global-operator. We show that TeamLTL extended with the Boolean disjunction is equi-expressive with the positive Boolean closure of HyperLTL restricted to one universal quantifier, while the left-downward closed fragment of TeamLTL extended with the Boolean negation is expressively equivalent with the Boolean closure of HyperLTL restricted to one universal quantifier.

翻译：线性时序逻辑（LTL）在系统验证中用于描述反应式系统的形式化规约。然而，某些重要性质（如信息流安全中的非推断性）无法用LTL表达。近年来备受关注的一类此类性质被称为超性质。当前捕获超性质的研究主要存在两大方向：一是通过扩展LTL引入轨迹量词构成的超逻辑（HyperLTL），二是采用团队语义将真值扩展到轨迹集合的逻辑。本文探讨基于集合的团队语义下的异步LTL（TeamLTL）与HyperLTL之间的逻辑关系。具体而言，我们研究了TeamLTL的两种扩展形式：其一是添加布尔析取算子的扩展，其二是添加布尔否定算子的片段（该片段限制否定词不得出现在Until算子的左侧或Global算子内部）。我们证明：添加布尔析取的TeamLTL在表达能力上等价于受限单全称量词HyperLTL的正布尔闭包；而添加布尔否定且满足左向下封闭性的TeamLTL片段在表达能力上等价于受限单全称量词HyperLTL的布尔闭包。