Analyzing LTL Model Checking Techniques for Plan Synthesis and Controller Synthesis (Work in Progress) |
| |
| Authors: | Sylvain Kerjean, Froduald Kabanza, Richard St-Denis,Sylvie Thi baux |
| |
| Affiliation: | Département d'informatique, Université de Sherbrooke, Sherbrooke (Québec), Canada J1K 2R1;National ICT Australia and Computer Science Laboratory, The Australian National University, Canberra ACT 0200 Australia |
| |
| Abstract: | 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. |
| |
| Keywords: | LTL2Bü chi translators formula progression model checking verification synthesis |
| 本文献已被 ScienceDirect 等数据库收录！ |
|
