Analyzing LTL Model Checking Techniques for Plan Synthesis and Controller Synthesis (Work in Progress)

In this paper, we present alternative means of handling invariances in reachability testing, either by formula progression or compilation into Büchi automata. These alternatives are presented in connection with three different applications of model checking: verification, plan synthesis as well as heuristic guidance of AI planning, and controller synthesis. We include results from benchmarks obtained from preparatory experiments with model checking using a family of LTL2Büchi translators and formula progression.