Automated planning as an early verification tool for distributed control. (English) Zbl 1315.68178
Summary: We present a new modelling formalism which is suitable for capturing high level functional specifications and requirements of reactive control systems. This formalism is a simple extension of the classical planning formalism. We show that if specifications are thus formalized, then it is possible to use existing automated planners and model checkers to find logical faults in them. Our extension to classical planning consists of introducing a separate class of actions, referred as control actions, which have higher priority than regular actions. We present several illustrative examples of high-level modelling and verification of modern automotive features with our proposed formalism. We present several compilation schemes to solve the proposed problem using well-known planners and the model checkers. We present a comparative study of the performance of a number of well-known tools on our problem.We also present some novel optimization techniques which help the solution scale much better with most of the studied tools.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68T20 | Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) |
Keywords:
automated planning; model checking; action priority; formal verification; early verification; distributed control; component based systems; logical faults; automotive; reactive control; requirements engineeringReferences:
| [1] | Albore, A., Palacios, H., Geffner, H.: A translation-based approach to contingent planning. In: Proceedings of the 21st International Joint Conference on AI (IJCAI-09), pp. 1623-1628 (2009) · Zbl 1017.68533 |
| [2] | Applegate, C., Elsaesser, C., Sanborn, J.: An architecture for adversarial planning. IEEE Trans. Syst. Man Cybern. 20(1), 186-194 (1990) · doi:10.1109/21.47820 |
| [3] | Bacchus, F., Kabanza, F.: Using temporal logics to express search control knowledge for planning. Artif. Intell. 116(1-2), 123-191 (2000) · Zbl 0939.68827 |
| [4] | Baier, J.A., McIlraith, S.A.: Planning with first-order temporally extended goals using heuristic search. In: Proceedings of the National Conference on Artificial Intelligence, Vol. 21, p. 788. AAAI Press; MIT Press, Menlo Park (1999) |
| [5] | Baier, J.A., McIlraith, S.A.: Planning with temporally extended goals using heuristic search. In: ICAPS, pp. 342-345 (2006) · Zbl 1080.68657 |
| [6] | Baier, J.A., Fritz, C, McIlraith, S.A.: Exploiting procedural domain control knowledge in state-of-the-art planners. In: Proceedings of the 17th International Conference on Automated Planning and Scheduling (ICAPS’07), pp. 26-33 (2007) |
| [7] | Berry, G., Moisan, S., Rigault, J.: Esterel: towards a synchronous and semantically sound high-level language for real-time applications. In: Proceedings of the IEEE Real-Time Systems Symposium, pp. 30-40 (1983) · Zbl 0970.68044 |
| [8] | Bertoli, P., Cimatti, A., Pistore, M., Roveri, M., Traverso, P.: Mbp: a model based planner. In: Proceedings of the IJCAI01 Workshop on Planning under Uncertainty and Incomplete Information (2001) · Zbl 0562.68071 |
| [9] | Blum, A., Furst, M.: Fast planning through planning graph analysis. Artif. Intell. 90(1-2), 281-300 (1997) · Zbl 1017.68533 · doi:10.1016/S0004-3702(96)00047-1 |
| [10] | Botea, A., Enzenberger, M., Müller, M., Schaeffer, J.: Macro-ff: improving AI planning with automatically learned macro-operators. J. Artif. Intell. Res. 24(1), 581-621 (2005) · Zbl 1080.68657 |
| [11] | Broy, M.: Challenges in automotive software engineering. In: Proceedings of the 28th International Conference on Software Engineering, pp. 33-42. ACM (2006) · Zbl 0971.68151 |
| [12] | Bylander, T.: The computational complexity of propositional strips planning. Artif. Intell. 69(1-2), 165-204 (1994) · Zbl 0821.68065 · doi:10.1016/0004-3702(94)90081-7 |
| [13] | Caspi, P., Pilaud, D., Halbwachs, N., Plaice, J.A.: Lustre: a declarative language for real-time programming. In: Proceedings of the 14th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL ’87), pp. 178-188. ACM, New York (1987) · Zbl 1182.68245 |
| [14] | Chen, Y., Xing, Z., Zhang, W.: Long-distance mutual exclusion for propositional planning. In: Proceedings of the 20th International Joint Conference on Artifical Intelligence (IJCAI’07), pp. 1840-1845. Morgan Kaufmann Publishers Inc., San Francisco (2007) · Zbl 0234.68036 |
| [15] | Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: a new symbolic model verifier. In: Halbwachs, N., Peled, D. (eds.) Proceedings of the Eleventh Conference on Computer-Aided Verification (CAV’99), n0. 1633 in LNCS, pp. 495-499. Springer, Trento (1999) · Zbl 1046.68587 |
| [16] | Cimatti, A., Pistore, M., Roveri, M., Traverso, P.: Weak, strong, and strong cyclic planning via symbolic model checking. Artif. Intell. 147(1), 35-84 (2003) · Zbl 1082.68800 · doi:10.1016/S0004-3702(02)00374-0 |
| [17] | Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Computer Aided Verification, pp. 154-169. Springer (2000) · Zbl 0974.68517 |
| [18] | Dal Lago, U., Pistore, M., Traverso, P.: Planning with a language for extended goals. In: AAAI/IAAI, pp. 447-454 (2002) |
| [19] | Edelkamp, S.: On the compilation of plan constraints and preferences. In: ICAPS, pp. 374-377 (2006) |
| [20] | Edelkamp, S., Helmert, M.: Mips: the model-checking integrated planning system. AI Mag. 22(3), 67 (2001) |
| [21] | Edelkamp, S., Jabbar, S.: Action planning for directed model checking of petri nets. Electron. Notes Theor. Comput. Sci. 149(2), 3-18 (2006) · Zbl 1273.68255 · doi:10.1016/j.entcs.2005.07.023 |
| [22] | Fawcett, C., Helmert, M., Hoos, H., Karpas, E., Röger, G., Seipp, J.: Fd-autotune: domain-specific configuration using fast-downward. In: Proceedings of the ICAPS-PAL 2011(8) (2011) |
| [23] | Fikes, R., Nilsson, N.: STRIPS: a new approach to the application of theorem proving to problem solving. Artif. Intell. 2(3/4), 189-208 (1971) · Zbl 0234.68036 · doi:10.1016/0004-3702(71)90010-5 |
| [24] | Gazen, B., Knoblock, C.: Combining the expressivity of ucpop with the efficiency of graphplan. In: Steel, S., Alami, R. (eds.) Recent Advances in AI Planning, Lecture Notes in Computer Science, Vol. 1348, pp 221-233. Springer, Berlin / Heidelberg (1997) · Zbl 0962.91011 |
| [25] | Gerevini, A., Long, D.: Plan Constraints and Preferences in pddl3 - the Language of the Fifth International Planning Competition. Tech. rep., Department of Electronics for Automation. University of Brescia, Italy (2005) |
| [26] | Gerevini, A., Serina, I.: LPG: a planner based on local search for planning graphs with action costs. In: Proceedings of the Sixth International Conference on AI Planning and Scheduling, pp. 12-22 (2002) |
| [27] | Gerth, R.: Concise Promela Reference (1997). http://spinroot.com/spin/Man/Quick.html |
| [28] | Ghosh, K., Dasgupta, P., Ramesh, S.: Planning with action prioritization and new benchmarks for classical planning. In: Thielscher, M., Zhang, D. (eds.) Australasian Conference on Artificial Intelligence. Lecture Notes in Computer Science, Vol. 7691, pp. 779-790. Springer (2012) |
| [29] | Giunchiglia, F., Traverso, P.: Planning as model checking. In: Biundo, S., Fox, M. (eds.) Recent Advances in AI Planning, Lecture Notes in Computer Science, Vol. 1809, pp. 1-20. Springer, Berlin / Heidelberg (2000) · Zbl 0971.68151 |
| [30] | Grimm, C.: Languages for System Specification: Selected Contributions on UML, SystemC, System Verilog, Mixed-signal Systems, and Property Specification from FDL’03. Springer (2004) · Zbl 1049.68085 |
| [31] | Helmert, M.: The fast downward planning system. J. Artif. Intell. Res. (JAIR) 26, 191-246 (2006) · Zbl 1182.68245 · doi:10.1007/s10462-007-9049-y |
| [32] | Hoffmann, J., Nebel, B.: The FF planning system: fast plan generation through heuristic search. J. Artif. Intell. Res. (JAIR) 14, 253-302 (2001) · Zbl 0970.68044 |
| [33] | Holzmann, G.: The model checker spin. IEEE Trans. Softw. Eng. 23(5), 279 -295 (1997) · doi:10.1109/32.588521 |
| [34] | Holzmann, G.: Spin Model Checker, The: Primer and Reference Manual, 1st edn. Addison-Wesley Professional (2003) |
| [35] | Holzmann, G.J., Joshi, R., Groce, A.: Swarm verification. In: Proceedings of the 2008 23rd IEEE/ACM International Conference on Automated Software Engineering, pp. 1-6. IEEE Computer Society (2008) · Zbl 1002.68158 |
| [36] | Johnson, S.: Formal methods in embedded design. Computer 36(11), 104-106 (2003) · doi:10.1109/MC.2003.1244539 |
| [37] | Junghanns, A., Schaeffer, J.: Sokoban: enhancing general single-agent search methods using domain knowledge. Artif. Intell. 129(1), 219-251 (2001) · Zbl 0971.68151 · doi:10.1016/S0004-3702(01)00109-6 |
| [38] | Kautz, H., Selman, B.: Planning as satisfiability. In: Proceedings of the 10th European Conference on Artificial Intelligence (ECAI ’92), pp. 359-363. Wiley, New York (1992) |
| [39] | Kautz, H., Selman, B., Hoffmann, J.: Satplan: planning as satisfiability. In: 5th International Planning Competition (2006) |
| [40] | Kautz, H.A., Mcallester, D., Selman, B.: Encoding plans in propositional logic. In: Proceedings of the 50th International Conference on the Principle of Knowledge Representation and Reasoning (KR’96), pp. 374-384 (1996) |
| [41] | Kissmann, P., Edelkamp, S.: Gamer, a general game playing agent. KI 25(1), 49-52 (2011) |
| [42] | Korf, R.E.: Macro-operators: a weak method for learning. Artif. Intell. 26(1), 35-77 (1985) · Zbl 0562.68071 · doi:10.1016/0004-3702(85)90012-8 |
| [43] | Kupferschmid, S., Hoffmann, J., Dierks, H., Behrmann, G.: Adapting an AI planning heuristic for directed model checking. In: Valmari, A. (ed.) Model Checking Software, Lecture Notes in Computer Science, Vol. 3925, pp. 35-52. Springer, Berlin / Heidelberg (2006) · Zbl 1178.68347 |
| [44] | Kvarnström, J., Doherty, P.: Talplanner: a temporal logic based forward chaining planner. Ann. Math. Artif. Intell. 30(1-4), 119-169 (2000) · Zbl 1002.68158 · doi:10.1023/A:1016619613658 |
| [45] | Marsden, G., McDonald, M., Brackstone, M.: Towards an understanding of adaptive cruise control. Transp. Res. Part C Emerg. Technol. 9(1), 33-51 (2001) · doi:10.1016/S0968-090X(00)00022-X |
| [46] | Mcdermott, D., Ghallab, M., Howe, A., Knoblock, C., Ram, A., Veloso, M., Weld, D., Wilkins, D.: Pddl - the Planning Domain Definition Language. Tech. rep., CVC TR-98-003/DCS TR-1165, Yale Center for Computational Vision and Control (1998) |
| [47] | McElligott, P., Mjeda, A., Thiel, S.: Can formal methods make automotive business sense? A classification of formal methods by usefulness. SAE SP 2173, 83 (2008) |
| [48] | Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science, pp. 46-57 (1977), 10.1109/SFCS.1977.32 |
| [49] | Prestl, W., Sauer, T., Steinle, J., Tschernoster, O.: The bmw active cruise control acc. In: SAE International Congressional Exposure, 2000, Society of Automotive Engineers, 400 Commonwealth Dr, Warrendale, PA, 15096, USA (2000) |
| [50] | Richter, S., Westphal, M., Helmert, M.: Lama 2008 and 2011. The 2011 International Planning Competition, p. 50 (2011) |
| [51] | Rintanen, J.: Madagascar: efficient planning with sat. The 2011 International Planning Competition, p. 61 (2011) |
| [52] | Schätz, B., Fleischmann, A., Geisberger, E., Pister, M.: Model-based requirements engineering with autoraid. In: Workshop Modellbasierte Qualitätssicherung (QUAM), Lecture Notes in Informatics (LNI), pp. 511-516 (2005) |
| [53] | Shaparau, D., Pistore, M., Traverso, P.: Fusing procedural and declarative planning goals for nondeterministic domains. In: Proceedings of the 23rd National Conference on Artificial Intelligence (AAAI’08), pp. 983-990. AAAI Press (2008) |
| [54] | Slaney, J.: Randomnet: A Specific-purpose Tool that Generates Random Descriptions of Power Distribution Networks as Part of the PSR (Power Supply Restoration) Benchmark for AI Planning (2005). http://rsise.anu.edu.au/jks/software/randomnet.tar.gz · Zbl 0445.68072 |
| [55] | Somenzi, F.: CUDD: CU Decision Diagram Package Release 2.4. 1. University of Colorado at Boulder (2005) |
| [56] | Thiébaux, S., Cordier, M.: Supply restoration in power distribution systems-a benchmark for planning under uncertainty. In: Pre-Proceedings of the 6th European Conference on Planning (ECP-01), pp. 85-96 (2001) · Zbl 1002.68158 |
| [57] | Thiébaux, S., Hoffmann, J., Nebel, B.: In defense of pddl axioms. Artif. Intell. 168(1-2), 38-69 (2005) · Zbl 1132.68714 · doi:10.1016/j.artint.2005.05.004 |
| [58] | Wilkins, D.: Using patterns and plans in chess. Artif. Intell. 14(2), 165-203 (1980) · Zbl 0445.68072 · doi:10.1016/0004-3702(80)90039-9 |
| [59] | Willmott, S., Richardson, J., Bundy, A., Levine, J.: An adversarial planning approach to go. Comput. Games 1558, 93-112 (1999) · Zbl 0962.91011 · doi:10.1007/3-540-48957-6_6 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
