A loop acceleration technique to speed up verification of automatically generated plans
Tóm tắt
The CIRCA planning system automatically creates reactive plans and uses formal verification techniques to prove that those plans will preserve system safety. CIRCA’s timed automata verification system is highly efficient, yet can display pathologically bad behavior when reasoning about reaction loops, a particular form of interacting cycles of states. In this paper, we describe a loop acceleration technique that recognizes these state-space structures during the verification process and bypasses the process of expanding an arbitrarily large cycle of states, effectively compressing loops of arbitrary size into a compact, finite set of states. The resulting performance improvement can be very dramatic: in domains where tight loops of short-duration transitions interact with long-duration transitions, our new loop acceleration methods can reduce verification time (and hence planning time) from hours to below a second.
Tài liệu tham khảo
Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126, 183–235 (1994)
Larsen, K.G., Pettersson, P., Yi, W.: Model-checking for real-time systems. In: Proceedings of Fundamentals of Computation Theory. Lecture Notes in Computer Science, vol. 965, pp. 62–88 (1995)
Behrmann, G., Bengtsson, J., David, A., Larsen, K.G., Pettersson, P., Yi, W.: Uppaal implementation secrets. In: Proceedings of 7th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems (2002)
Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: Bernardo, M., Corradini, F. (eds.) Formal Methods for the Design of Real-Time Systems: 4th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004, vol. 3185 in LNCS, pp. 200–236. Springer, Berlin (2004)
Yovine, S.: Kronos: a verification tool for real-time sytems. Springer Int J Softw Tools Technol Transf. 1, 123–133 (1997)
Hune, T.S.: Modeling a language for embedded systems in timed automata. Research Series RS-00-17, BRICS, Department of Computer Science, University of Aarhus, Aug. 2000, 26 pp. Earlier version entitled Modelling a Real-Time Language appeared in Fourth International Workshop on Formal Methods for Industrial Critical Systems (FMICS99), pp. 259–282 (2000)
Iversen, T.K., Kristoffersen, K.J., Larsen, K.G., Laursen, M., Madsen, R.G., Mortensen, S.K., Pettersson, P., Thomasen, C.B.: Model-checking real-time control programs—verifying LEGO MINDSTORMS systems using UPPAAL. In: Proceedings of 12th Euromicro Conference on Real-Time Systems, pp. 147–155. IEEE Computer Society Press, New York (2000)
Hendriks, M., Larsen, K.G.: Exact acceleration of real-time model checking. Electronic Notes in Theoretical Computer Science, vol. 65 (2002)
Musliner, D.J., Durfee, E.H., Shin, K.G.: CIRCA: a cooperative intelligent real-time control architecture. IEEE Trans. Syst. Man Cybern. 23(6), 1561–1574 (1993)
Musliner, D.J., Durfee, E.H., Shin, K.G.: World modeling for the dynamic construction of real-time control plans. Artif. Intell. 74, 83–127 (1995)
Musliner, D.J., Pelican, M.J.S., Goldman, R.P., Krebsbach, K.D., Durfee, E.H.: The evolution of CIRCA, a theory-based AI architecture with real-time performance guarantees. In: AAAI Spring Symposium on Architectures for Intelligent Theory-Based Agents (2008)
Kortenkamp, D., Bonasso, P., Musliner, D.J., Pelican, M.J.S., Hostetler, J.: Embedding planning technology into satellite systems. In: AIAA Infotech@Aerospace (2011)
Hendriks, M.: Model Checking Timed Automata—Techniques and Applications. PhD thesis, Institute for Programming research and Algorithmics (IPA) (2006)
Fietzke, A., Kruglov, E., Weidenbach, C.: Automatic generation of inductive invariants by sup(la). Tech. Rep. MPII2012RG1-002, Max-Planck-Institut fur Informatik (2012)
Bozga, M., Konecny, F., Iosif, R.: Fast acceleration of ultimately periodic relations, Tech. Rep. TR-2010-3, Verimag Technical Report, 2010. Version: 1 (2010)
Bardin, S., Finkel, A., Leroux, J., Schnoebelen, P.: Flat acceleration in symbolic model checking. In: Peled, D.A., Tsay, Y.-K. (eds.) Proceedings of the 3rd International Symposium on Automated Technology for Verification and Analysis (ATVA’05), Lecture Notes in Computer Science, vol. 3707, pp. 474–488. Springer, Taipei, Taiwan (2005)
Bardin, S., Leroux, J., Point, G.: FAST extended release. In: Ball, T., Jones, R.B. (eds.) Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 4144 , pp. 63–66. Springer, Berlin (2006)
Salah, R.B.: On Timing Analysis Of Large Systems. PhD thesis, Institut National Polytechnique De Grenoble (2007)
Gat, E.: News from the trenches: an overview of unmanned spacecraft for AI. In: Nourbakhsh, I. (ed.) AAAI Technical Report SSS-96-04: Planning with Incomplete Information for Robot Problems. American Association for Artificial Intelligence (1996)
Musliner, D.J., Goldman, R.P.: CIRCA and the Cassini Saturn orbit insertion: Solving a prepositioning problem. In: Working Notes of the NASA Workshop on Planning and Scheduling for Space (1997)
Goldman, R.P., Pelican, M.J.S., Musliner, D.J.: Guiding planner backjumping using verifier traces. In: Zilberstein, S., Koehler, J., Koenig, S. (eds.) Proceedings of the Fourteenth International Conference on Automated Planning and Scheduling, pp. 279–286 (2004)
Potts, C.M., Krebsbach, K.D., Thayer, J.T., Musliner, D.J.: Improving trust estimates in planning domains with rare failure events. In: AAAI Spring Symposium on Trust and Autonomous Systems (2013)
Kortenkamp, D., Hudson, M.B., Bell, S., Musliner, D.J., Pelican, M.J.S., Hamell, J., Zetocha, P.: Embedding planning technology into satellite systems. In: International Symposium on Artificial Intelligence, Robotics and Automation in Space (2012)
Daws, C., Olivero, A., Tripakis, S., Yovine, S.: The tool kronos. In: Hybrid Systems III: Verification and, Control, pp. 208–219 (1996)
Alur, R.: Timed automata. Tech. Rep. MS-CIS-98-10, University of Pennsylvania, Philadelphia (1998)
Alur, R.: Timed automata. In: Working Notes of the NATO-ASI Summer School on Verification of Digital and Hybrid Systems (1998)
Dill, D.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) Automatic Verification Methods for Finite State Systems. Lecture Notes in Computer Science, vol. 407 , pp. 197–212. Springer, Berlin (1990)
Dechter, R., Meiri, I., Pearl, J.: Temporal constraint networks. Artif. Intell. 49(1–3), 61–95 (1991)
Ramadge, P.J., Wonham, W.M.: The control of discrete event systems. Proc. IEEE 77, 81–98 (1989)