Martin Suda — Resolution-based Methods for Linear Temporal Reasoning CZ | EN

The aim of this thesis is to explore the potential of resolution-based methods for linear temporal reasoning. On the abstract level, this means to develop new algorithms for automated reasoning about properties of systems which evolve in time. More concretely, we 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.

We implemented the proposed ideas and provide experimental results which demonstrate their practical potential on representative benchmark sets. Our system LS4 is shown to be the strongest LTL prover currently publicly available. The mentioned enhancement of PDR substantially improves the performance of our implementation of the algorithm for hardware model checking in the multi-property setting. It is expected that other implementations would benefit from it in an analogous way. Finally, our planner PDRplan has been compared with the state-of-the-art planners on the benchmarks from the International Planning Competition with very promising results.