Analyzing LTL Model Checking Techniques for Plan Synthesis and Controller Synthesis (Work in Progress)
Sylvain Kerjean, Froduald Kabanza, Richard St‐Denis, Sylvie Thiébaux · Electronic Notes in Theoretical Computer Science · 2006
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.