Reachability analysis plays a central role in system design and verification. The reachability problem, denoted $\Diamond^J\,\Phi$, asks whether the system will meet the property $\Phi$ after some time in a given time interval $J$. Recently, it has been considered on a novel kind of real-time systems -- quantum continuous-time Markov chains (QCTMCs), and embedded into the model-checking algorithm. In this paper, we further study the repeated reachability problem in QCTMCs, denoted $\Box^I\,\Diamond^J\,\Phi$, which concerns whether the system starting from each \emph{absolute} time in $I$ will meet the property $\Phi$ after some coming \emph{relative} time in $J$. First of all, we reduce it to the real root isolation of a class of real-valued functions (exponential polynomials), whose solvability is conditional to Schanuel's conjecture being true. To speed up the procedure, we employ the strategy of sampling. The original problem is shown to be equivalent to the existence of a finite collection of satisfying samples. We then present a sample-driven procedure, which can effectively refine the sample space after each time of sampling, no matter whether the sample itself is successful or conflicting. The improvement on efficiency is validated by randomly generated instances. Hence the proposed method would be promising to attack the repeated reachability problems together with checking other $\omega$-regular properties in a wide scope of real-time systems.

翻译：可达性分析在系统设计与验证中占据核心地位。可达性问题（记为$\Diamond^J\,\Phi$）询问系统是否会在给定时间区间$J$内的某个时刻满足属性$\Phi$。近年来，该问题被应用于一类新型实时系统——量子连续时间马尔可夫链（QCTMCs），并嵌入到模型检测算法中。本文进一步研究QCTMC中的重复可达性问题（记为$\Box^I\,\Diamond^J\,\Phi$），该问题关注系统从$I$中的每个*绝对*时间点出发，是否会在后续$J$中的某个*相对*时间点满足属性$\Phi$。首先，我们将其归约为一类实值函数（指数多项式）的实根隔离问题，而该类函数的可解性依赖于Schanuel猜想是否成立。为加速求解过程，我们采用采样策略。原问题被证明等价于存在有限个满足条件的采样点。我们进而提出一种样本驱动过程，该过程无论样本本身成功与否或是否存在冲突，均能在每次采样后有效精炼样本空间。通过随机生成的实例验证了其效率提升。因此，所提方法有望在更广泛的实时系统中攻克重复可达性问题，并辅助检验其他$\omega$-正则性质。