AI 中文总结
研究提出分解时态逻辑（DTL）用于表达概率超属性，基于测度分解概念支持对随机系统推理。阐述其在多方面应用及与现有逻辑关系，虽完整DTL模型检查不可判定，但确定两个可判定片段，线性片段基于线性代数技术，定性片段扩展标准算法。
AI 中文摘要
我们引入了分解时态逻辑（DTL），这是一种新的概率时态逻辑，能够表达多种概率超属性，包括概率非干扰和完美不可区分性。DTL基于概率论中的测度分解概念，允许根据程序执行期间发生的有限或无限事件序列来条件化概率。这自然支持对相互作用的随机系统进行推理，其中一个组件的完整执行会在另一个组件上诱导条件概率分布。我们说明了DTL在与随机环境交互的系统、马尔可夫决策过程的分布属性以及无限单词上的概率自动机中的应用，并讨论了它与现有概率逻辑的关系。虽然针对完整DTL对马尔可夫链进行模型检查是不可判定的，但我们确定了两个可判定的片段，它们捕获了许多感兴趣的超属性。线性片段允许基于线性代数技术的多项式时间模型检查过程，并捕获诸如完美不可区分性和基于历史的概率非干扰等概率信息流属性。定性片段允许自动机理论模型检查过程，该过程通过对底部强连通组件的推理扩展了$\mathit{HyperCTL}^*$的标准算法。
英文摘要
We introduce Disintegration Temporal Logic (DTL), a new probabilistic temporal logic that can express a wide range of probabilistic hyperproperties, including probabilistic non-interference and perfect indistinguishability. DTL is based on the notion of measure disintegration from probability theory, which allows for conditioning probabilities on a finite or infinite sequence of events occurring during a program execution. This naturally supports reasoning about interacting stochastic systems, where complete executions of one component induce conditional probability distributions over another. We illustrate applications of DTL to systems interacting with stochastic environments, distributional properties of Markov decision processes, and probabilistic automata on infinite words, and discuss its relationship to existing probabilistic logics. While model checking Markov chains against full DTL is undecidable, we identify two decidable fragments that capture many hyperproperties of interest. The linear fragment admits a polynomial-time model-checking procedure based on linear-algebraic techniques and captures probabilistic information-flow properties such as perfect indistinguishability and history-based probabilistic non-interference. The qualitative fragment admits an automata-theoretic model-checking procedure that extends the standard algorithm for $\mathit{HyperCTL}^*$ with reasoning about bottom strongly connected components.
