Exploiting Adjoints in Property Directed Reachability Analysis

TL;DR

This paper introduces two new algorithms for property directed reachability analysis, leveraging lattice theory and adjoint concepts to improve the identification of invariants and counterexamples, with applications to Markov Decision Processes.

Contribution

The paper presents novel algorithms based on lattice-theoretic adjoints for reachability analysis, extending the scope of property directed reachability methods.

Findings

Algorithms effectively find safe invariants and counterexamples.

Application to quantitative reachability in Markov Decision Processes.

Use of adjoints enhances abstraction capabilities.

Abstract

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.