{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T15:13:18Z","timestamp":1648566798181},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2013,6,25]],"date-time":"2013-06-25T00:00:00Z","timestamp":1372118400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2014,2]]},"DOI":"10.1007\/s10009-013-0284-z","type":"journal-article","created":{"date-parts":[[2013,6,23]],"date-time":"2013-06-23T21:55:44Z","timestamp":1372024544000},"page":"13-29","source":"Crossref","is-referenced-by-count":1,"title":["A loop acceleration technique to speed up verification of automatically generated plans"],"prefix":"10.1007","volume":"16","author":[{"given":"Robert P.","family":"Goldman","sequence":"first","affiliation":[]},{"given":"Michael J. S.","family":"Pelican","sequence":"additional","affiliation":[]},{"given":"David J.","family":"Musliner","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,6,25]]},"reference":[{"key":"284_CR1","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126, 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"284_CR2","doi-asserted-by":"crossref","unstructured":"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\u201388 (1995)","DOI":"10.1007\/3-540-60249-6_41"},{"key":"284_CR3","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1007\/3-540-45739-9_1"},{"key":"284_CR4","doi-asserted-by":"crossref","unstructured":"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\u2013236. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"284_CR5","doi-asserted-by":"crossref","unstructured":"Yovine, S.: Kronos: a verification tool for real-time sytems. Springer Int J Softw Tools Technol Transf. 1, 123\u2013133 (1997)","DOI":"10.1007\/s100090050009"},{"key":"284_CR6","doi-asserted-by":"crossref","unstructured":"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\u2013282 (2000)","DOI":"10.7146\/brics.v7i17.20144"},{"key":"284_CR7","doi-asserted-by":"crossref","unstructured":"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\u2014verifying LEGO MINDSTORMS systems using UPPAAL. In: Proceedings of 12th Euromicro Conference on Real-Time Systems, pp. 147\u2013155. IEEE Computer Society Press, New York (2000)","DOI":"10.1109\/EMRTS.2000.854002"},{"key":"284_CR8","doi-asserted-by":"crossref","unstructured":"Hendriks, M., Larsen, K.G.: Exact acceleration of real-time model checking. Electronic Notes in Theoretical Computer Science, vol. 65 (2002)","DOI":"10.1016\/S1571-0661(04)80473-0"},{"issue":"6","key":"284_CR9","doi-asserted-by":"crossref","first-page":"1561","DOI":"10.1109\/21.257754","volume":"23","author":"DJ Musliner","year":"1993","unstructured":"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\u20131574 (1993)","journal-title":"IEEE Trans. Syst. Man Cybern."},{"key":"284_CR10","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1016\/0004-3702(94)00008-O","volume":"74","author":"DJ Musliner","year":"1995","unstructured":"Musliner, D.J., Durfee, E.H., Shin, K.G.: World modeling for the dynamic construction of real-time control plans. Artif. Intell. 74, 83\u2013127 (1995)","journal-title":"Artif. Intell."},{"key":"284_CR11","unstructured":"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)"},{"key":"284_CR12","doi-asserted-by":"crossref","unstructured":"Kortenkamp, D., Bonasso, P., Musliner, D.J., Pelican, M.J.S., Hostetler, J.: Embedding planning technology into satellite systems. In: AIAA Infotech@Aerospace (2011)","DOI":"10.2514\/6.2011-1564"},{"key":"284_CR13","unstructured":"Hendriks, M.: Model Checking Timed Automata\u2014Techniques and Applications. PhD thesis, Institute for Programming research and Algorithmics (IPA) (2006)"},{"key":"284_CR14","unstructured":"Fietzke, A., Kruglov, E., Weidenbach, C.: Automatic generation of inductive invariants by sup(la). Tech. Rep. MPII2012RG1-002, Max-Planck-Institut fur Informatik (2012)"},{"key":"284_CR15","unstructured":"Bozga, M., Konecny, F., Iosif, R.: Fast acceleration of ultimately periodic relations, Tech. Rep. TR-2010-3, Verimag Technical Report, 2010. Version: 1 (2010)"},{"key":"284_CR16","doi-asserted-by":"crossref","unstructured":"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\u201905), Lecture Notes in Computer Science, vol. 3707, pp. 474\u2013488. Springer, Taipei, Taiwan (2005)","DOI":"10.1007\/11562948_35"},{"key":"284_CR17","doi-asserted-by":"crossref","unstructured":"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\u201366. Springer, Berlin (2006)","DOI":"10.1007\/11817963_9"},{"key":"284_CR18","unstructured":"Salah, R.B.: On Timing Analysis Of Large Systems. PhD thesis, Institut National Polytechnique De Grenoble (2007)"},{"key":"284_CR19","unstructured":"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)"},{"key":"284_CR20","unstructured":"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)"},{"key":"284_CR21","unstructured":"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\u2013286 (2004)"},{"key":"284_CR22","unstructured":"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)"},{"key":"284_CR23","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.2514\/6.2011-1564"},{"key":"284_CR24","doi-asserted-by":"crossref","unstructured":"Daws, C., Olivero, A., Tripakis, S., Yovine, S.: The tool kronos. In: Hybrid Systems III: Verification and, Control, pp. 208\u2013219 (1996)","DOI":"10.1007\/BFb0020947"},{"key":"284_CR25","unstructured":"Alur, R.: Timed automata. Tech. Rep. MS-CIS-98-10, University of Pennsylvania, Philadelphia (1998)"},{"key":"284_CR26","unstructured":"Alur, R.: Timed automata. In: Working Notes of the NATO-ASI Summer School on Verification of Digital and Hybrid Systems (1998)"},{"key":"284_CR27","doi-asserted-by":"crossref","unstructured":"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\u2013212. Springer, Berlin (1990)","DOI":"10.1007\/3-540-52148-8_17"},{"issue":"1\u20133","key":"284_CR28","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1016\/0004-3702(91)90006-6","volume":"49","author":"R Dechter","year":"1991","unstructured":"Dechter, R., Meiri, I., Pearl, J.: Temporal constraint networks. Artif. Intell. 49(1\u20133), 61\u201395 (1991)","journal-title":"Artif. Intell."},{"key":"284_CR29","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1109\/5.21072","volume":"77","author":"PJ Ramadge","year":"1989","unstructured":"Ramadge, P.J., Wonham, W.M.: The control of discrete event systems. Proc. IEEE 77, 81\u201398 (1989)","journal-title":"Proc. IEEE"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-013-0284-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-013-0284-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-013-0284-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,15]],"date-time":"2019-07-15T22:50:02Z","timestamp":1563231002000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-013-0284-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,6,25]]},"references-count":29,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,2]]}},"alternative-id":["284"],"URL":"https:\/\/doi.org\/10.1007\/s10009-013-0284-z","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,6,25]]}}}