Resolution-based methods for linear temporal reasoning

Abstract

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.

Das Ziel dieser Doktorarbeit ist es, das Potential resolutionsbasierter Methoden zur linearer, temporaler Beweisführung zu untersuchen. Von einem abstrakten Gesichtspunkt aus gesehen bedeutet dies, neue Algorithmen über die Eigenschaften von sich zeitlich entwicklenden Systemen im Bereich des automatischen Theorembeweisens zu entwickeln. Konkreter gesagt werden wir 1) aufzeigen, wie sich das Rahmenprogramm der Superposition so anpassen lässt, damit es Theoreme in propositionaler Linear Temporal Logic (LTL) beweist, 2) eine Verbindung zwischen der Superposition und dem CDCL-Kalkül moderner SAT-Solver nutzen, um mit einem effizienten LTL-Prover aufzuwarten, 3) das Vorangegangene auf Erreichbarkeitseigenschaften spezialisieren, und eine starke Verbindung zu der Property Directed Reachability (PDR), einem jüngst eintwickeltem Model-Checking-Algorithmus für Hardware-Schaltkreise, aufzudecken, 4) PDR durch die Einführung neuer Technik verbessern, die die Clause-Propagation-Phase des Algorithmus beschleunigt, und 5) PDR für das automatisierte Planen anpassen, indem wir den inneren SAT-Solver durch eine planungsspezifische Prozedur ersetzen. Wir haben die vorgeschlagenen Ideen implementiert, und es werden experimentelle Ergebnisse angegeben, die das praktische Potential dieser Ideen auf repräsentativen Benchmarks aufzeigt. Es hat sich herausgestellt, dass unser System LS4 der staerkste öffentlich zugängliche LTL-Prover ist. Die erwähnte Erweiterung von PDR verbessern die Leistungsfähigkeit unserer Implementierung des Hardware-Model-Checking-Algorithmus substantiell im Bereich der Multi-Property-Einstellungen. Wir erwarten, dass andere Implementierungen in ähnlicher Weise profitieren würden. Schließlich haben wir viel versprechende Ergebnisse durch den Vergleich unser Planer PDRplan mit anderen state-of-the-art Planer auf den Benchmarks der International Planning Competition erzielt.