Kerjean, SylvainKabanza, FrodualdSt-Denis, RichardThiebaux, Sylvie2015-12-071571-0661http://hdl.handle.net/1885/19559In 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 checkKeywords: Benchmarking; Mathematical models; Program translators; Formula progression; Model checking; Synthesis; Verification; Control equipment Formula progression; LTL2Bchi translators; Model checking; Synthesis; VerificationAnalyzing LTL model checking techniques for plan synthesis and controller synthesis200610.1016/j.entcs.2005.07.0282015-12-07