Resolution-based Methods for Linear Temporal Reasoning

RiSE will host a talk by Martin Suda on January 12, 2016

ABSTRACT

In this talk I will give an overview of my PhD work, in which I explored the potential of resolution-based methods for linear temporal reasoning. On the abstract level, this means the development of new algorithms for automated reasoning about properties of systems which evolve in time. More concretely, I will: 1) show how to adapt the superposition framework to proving theorems in propositional Linear Temporal Logic (LTL), 2) use a connection between superposition and the CDCL calculus of modern SAT solvers to come up with an efficient LTL prover, 3) specialize the previous to reachability properties and discover a close connection to Property Directed Reachability (PDR), an algorithm recently developed for model checking of hardware circuits, 4) further improve PDR by providing a new technique for enhancing clause propagation phase of the algorithm, and 5) adapt PDR to automated planning by replacing the SAT solver inside with a planning-specific procedure.