We formulate, in lattice-theoretic terms, two novel algorithms inspired by Bradley's property directed reachability algorithm. For finding safe invariants or counterexamples, the first algorithm exploits over-approximations of both forward and backward transition relations, expressed abstractly by the notion of adjoints. In the absence of adjoints, one can use the second algorithm, which exploits lower sets and their principals. As a notable example of application, we consider quantitative reachability problems for Markov Decision Processes.

翻译：我们以格论术语表述了两种受Bradley属性导向可达性算法启发的新算法。为寻找安全不变式或反例，第一种算法利用前向与后向转移关系的过逼近，这些关系通过伴随算子的概念抽象表达。当伴随算子不可用时，可采用第二种算法，该算法利用下集及其主元。作为典型应用案例，我们考虑了马尔可夫决策过程中的定量可达性问题。