The linear-hyper-branching spectrum of temporal logics
The linear-hyper-branching spectrum of temporal logics
复制标题
时序逻辑的线性超分支谱
DOI：
10.1515/itit-2014-1067
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
M. Rabe
中科院分区：
文献类型：
--
作者：
B. Finkbeiner;M. Rabe
时态逻辑家族最近被扩展为描述超性质的逻辑，如不干涉或观察决定论。超属性通过要求它们满足一定的关系来关联系统的多个计算路径，例如低安全性输出的相同估值。与LTL或CTL* 等经典时态逻辑不同，它们每次引用一个计算路径，HyperLTL和HyperCTL* 等超属性的时态逻辑可以通过同时显式量化多个计算路径来表达这种关系。在本文中，我们研究了扩展的时间逻辑的频谱与过程等价的线性分支谱的新的逻辑。
Abstract The family of temporal logics has recently been extended with logics for the specification of hyperproperties, such as noninterference or observational determinism. Hyperproperties relate multiple computation paths of a system by requiring that they satisfy a certain relationship, 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 logics by relating the new logics to the linear-branching spectrum of process equivalences.
DOI：
10.1007/978-3-642-27940-9_12
发表时间：
2012-01
期刊：
--
影响因子：
--
作者：
Rayna Dimitrova;B. Finkbeiner;Máté Kovács;M. Rabe;H. Seidl
通讯作者：
Rayna Dimitrova;B. Finkbeiner;Máté Kovács;M. Rabe;H. Seidl