We present a novel asynchronous hyper linear time temporal logic named LPrL (Linear Time Predicate Logic) and establish its basic theory. LPrL is a natural first order extension of LTL (Linear time temporal logic), in which the predicates specify the properties of and the relationships between traces (infinite sequences of actions) using Boolean combinations of LTL formulas. To augment the expressive power of the logic, we introduce a simple language of terms and add the equality predicate t = t' where t and t' are terms. We first illustrate how a number of the security policies as well as a basic consistency property of distributed processes can be captured using LPrL. We then establish our main results using automata theoretic techniques. Namely, the satisfiability and model checking problems for LPrL can be solved in elementary time. These results are in sharp contrast to HyperLTL, the prevalent synchronous hyper linear time logic, whose satisfiability problem is undecidable and whose model checking problem has non-elementary time complexity.

翻译：本文提出了一种新型异步超线性时间时序逻辑LPrL（线性时间谓词逻辑），并建立了其基础理论。LPrL是LTL（线性时序逻辑）的自然一阶扩展，其中谓词通过LTL公式的布尔组合来刻画迹（动作的无限序列）的性质及其相互关系。为增强该逻辑的表达能力，我们引入了一个简单的项语言，并添加了等式谓词t = t'（其中t和t'为项）。我们首先阐释了如何利用LPrL刻画若干安全策略以及分布式进程的基本一致性性质。随后运用自动机理论方法证明了主要结论：LPrL的可满足性与模型检测问题可在初等时间内求解。该结果与主流同步超线性时间逻辑HyperLTL形成鲜明对比——后者的可满足性问题是不可判定的，且其模型检测问题具有非初等时间复杂度。