This paper studies satisfying temporal logic specifications on stochastic dynamical systems, where the predicates evolve randomly over time. Such randomness may arise from uncertain environment models or external stochastic processes causing the sets associated with predicate satisfaction to vary in a non-deterministic manner. As a result, verifying whether a stochastic dynamical system satisfies a temporal specification depends also on the uncertainty in the predicates. We develop a certificate-based framework to bound the probability of satisfying temporal logic specifications with randomly evolving predicates. We first show that temporal logic specifications with stochastic predicates can be transformed to specifications with deterministic predicates on an augmented space which is extended to include the stochastic space of predicate's uncertainty. We then utilize barrier certificates on an augmented space to provide tractable optimization-based conditions and to avoid the computational burden of dynamic programming. Focusing on linear dynamics and safety-type specifications, we derive analytical conditions under which barrier certificates guarantee bounds on the probability of violating the stochastic safety predicates. The approach is demonstrated on numerical case studies.

翻译：本文研究了随机动力系统上的时序逻辑规范满足问题，其中谓词随时间随机演化。这种随机性可能源于不确定的环境模型或外部随机过程，导致与谓词满足相关的集合以非确定性方式变化。因此，验证随机动力系统是否满足时序规范也取决于谓词中的不确定性。我们开发了一个基于证书的框架，用于约束具有随机演化谓词的时序逻辑规范的满足概率。我们首先证明，具有随机谓词的时序逻辑规范可以转化为增广空间上具有确定性谓词的规范，该空间通过扩展以包含谓词不确定性的随机空间。然后，我们利用增广空间上的障碍证书提供可处理的基于优化的条件，以避免动态规划的计算负担。针对线性动力学和安全型规范，我们推导了障碍证书能保证违反随机安全谓词概率界限的解析条件。该方法通过数值案例研究进行了验证。