关于异步TeamLTL与HyperLTL表达力的一点注记
A Remark on the Expressivity of Asynchronous TeamLTL and HyperLTL
AI总结：
本文研究异步TeamLTL与HyperLTL的表达力关系，证明TeamLTL的布尔析取扩展等价于单全称量词HyperLTL的正布尔闭包，其布尔否定扩展的左向下封闭片段等价于对应布尔闭包。
摘要：
线性时序逻辑（LTL）在系统验证中用于为反应式系统编写形式化规范。然而，一些相关性质，例如信息流安全中的非推断性，无法在LTL中表达。近来受到广泛关注的一类此类性质被称为超性质（hyperproperties）。在刻画超性质的研究中存在两大主要流派，即扩展LTL以引入迹量词的超逻辑（HyperLTL），以及采用团队语义、将真值扩展到迹集合的逻辑。本文探讨了基于集合团队语义的异步LTL（TeamLTL）与HyperLTL之间的关系。特别地，我们考虑了TeamLTL带布尔析取的扩展，以及TeamLTL带布尔否定扩展的一个片段，其中否定不能出现在Until算子的左侧，也不能出现在Global算子内部。我们证明，带布尔析取扩展的TeamLTL与限制为单个全称量词的HyperLTL的正布尔闭包具有相同的表达力，而带布尔否定扩展的TeamLTL的左向下封闭片段与限制为单个全称量词的HyperLTL的布尔闭包在表达力上等价。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
