We develop model checking algorithms for Temporal Stream Logic (TSL) and Hyper Temporal Stream Logic (HyperTSL) modulo theories. TSL extends Linear Temporal Logic (LTL) with memory cells, functions and predicates, making it a convenient and expressive logic to reason over software and other systems with infinite data domains. HyperTSL further extends TSL to the specification of hyperproperties - properties that relate multiple system executions. As such, HyperTSL can express information flow policies like noninterference in software systems. We augment HyperTSL with theories, resulting in HyperTSL(T),and build on methods from LTL software verification to obtain model checking algorithms for TSL and HyperTSL(T). This results in a sound but necessarily incomplete algorithm for specifications contained in the forall*exists* fragment of HyperTSL(T). Our approach constitutes the first software model checking algorithm for temporal hyperproperties with quantifier alternations that does not rely on a finite-state abstraction.

翻译：我们开发了基于理论的时序流逻辑（TSL）和超时序流逻辑（Hyper Temporal Stream Logic, HyperTSL）的模型检测算法。TSL通过引入存储单元、函数和谓词扩展了线性时序逻辑（LTL），使其成为一种便捷且富有表现力的逻辑，能够对软件及其他具有无限数据域的系统进行推理。HyperTSL进一步将TSL扩展至超属性的规约——即关联多个系统执行的属性。因此，HyperTSL能够表达软件系统中的无干扰等信息流策略。我们通过引入理论对HyperTSL进行扩充，得到HyperTSL(T)，并借鉴LTL软件验证中的方法，为TSL和HyperTSL(T)开发了模型检测算法。该算法对于包含在HyperTSL(T)的forall*exists*片段内的规约，能够获得一个可靠但必然不完备的算法。我们的方法构成了首个无需依赖有限状态抽象、可处理带量词交替的时序超属性的软件模型检测算法。