The paper presents a methodology for temporal logic verification of continuous-time switched stochastic systems. Our goal is to find the lower bound on the probability that a complex temporal property is satisfied over a finite time horizon. The required temporal properties of the system are expressed using a fragment of linear temporal logic, called safe-LTL with respect to finite traces. Our approach combines automata-based verification and the use of barrier certificates. It relies on decomposing the automaton associated with the negation of specification into a sequence of simpler reachability tasks and compute upper bounds for these reachability probabilities by means of common or multiple barrier certificates. Theoretical results are illustrated by applying a counter-example guided inductive synthesis framework to find barrier certificates.

翻译：本文介绍了对连续时间转换的随机系统进行时间逻辑核查的方法。我们的目标是找到在一定时间范围内满足复杂时间属性的可能性的较低约束值。该系统所需的时间特性使用线性时间逻辑碎片来表示,在有限痕迹方面称为安全LTL。我们的方法是将基于自动的核查和使用屏障证书结合起来。它依靠将与拒绝规格相关的自动图解析成一系列更简单的可达性任务,并通过共同或多重屏障证书来计算这些可达性的可能性的上限值。理论结果通过应用反典型的、以导导导导导的合成框架来寻找屏障证书来说明。