{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T04:01:40Z","timestamp":1775880100693,"version":"3.50.1"},"reference-count":91,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2014,9,6]],"date-time":"2014-09-06T00:00:00Z","timestamp":1409961600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Autom Softw Eng"],"published-print":{"date-parts":[[2016,9]]},"DOI":"10.1007\/s10515-014-0168-9","type":"journal-article","created":{"date-parts":[[2014,9,5]],"date-time":"2014-09-05T19:07:36Z","timestamp":1409944056000},"page":"305-359","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":84,"title":["Practical verification of decision-making in agent-based autonomous systems"],"prefix":"10.1007","volume":"23","author":[{"given":"Louise A.","family":"Dennis","sequence":"first","affiliation":[]},{"given":"Michael","family":"Fisher","sequence":"additional","affiliation":[]},{"given":"Nicholas K.","family":"Lincoln","sequence":"additional","affiliation":[]},{"given":"Alexei","family":"Lisitsa","sequence":"additional","affiliation":[]},{"given":"Sandor M.","family":"Veres","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,9,6]]},"reference":[{"key":"168_CR1","doi-asserted-by":"crossref","unstructured":"Alechina, N., Logan, B., Nguyen, H.N., Rakib, A.: Automated verification of resource requirements in multi-agent systems using abstraction. In: Proceedings of the 6th International Workshop on Model-Checking AI, Springer, LNAI, vol. 6572, pp. 69\u201384 (2010)","DOI":"10.1007\/978-3-642-20674-0_5"},{"issue":"1","key":"168_CR2","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R Alur","year":"1995","unstructured":"Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theor. Comput. Sci. 138(1), 3\u201334 (1995)","journal-title":"Theor. Comput. Sci."},{"issue":"7","key":"168_CR3","doi-asserted-by":"crossref","first-page":"971","DOI":"10.1109\/5.871304","volume":"88","author":"R Alur","year":"2000","unstructured":"Alur, R., Henzinger, T.A., Lafferriere, G., Pappas, G.J.: Discrete abstractions of hybrid systems. Proc. IEEE 88(7), 971\u2013984 (2000)","journal-title":"Proc. IEEE"},{"key":"168_CR4","unstructured":"Barringer, H., Giannakopoulou, D.: Proof rules for automated compositional verification through learning. In: Proceedings of SAVCBS Workshop, pp. 14\u201321 (2003)"},{"key":"168_CR5","doi-asserted-by":"crossref","unstructured":"Bauer, K.: A New Modelling Language for Cyber-Physical Systems. PhD thesis, Technische Universit\u00e4t Kaiserlautern (2012)","DOI":"10.1145\/2530544.2530547"},{"key":"168_CR6","volume-title":"Handbook of Modal Logic","year":"2006","unstructured":"Blackburn, P., van Benthem, J., Wolter, F. (eds.): Handbook of Modal Logic. Elsevier, Amsterdam (2006)"},{"key":"168_CR7","volume-title":"Readings in Distributed Artificial Intelligence","year":"1988","unstructured":"Bond, A.H., Gasser, L. (eds.): Readings in Distributed Artificial Intelligence. Morgan Kaufmann, San Mateo, CA (1988)"},{"key":"168_CR8","doi-asserted-by":"crossref","unstructured":"Bordini, R.H., H\u00fcbner, J.F., Vieira, R.: Jason and the Golden Fleece of agent-oriented programming. In: Bordini, R.H., Dastani, M., Dix, J., El Fallah-Seghrouchni, A. (eds.) Multi-Agent Programming: Languages, Platforms and Applications, chap. 1, pp. 3\u201337. Springer, Berlin (2005)","DOI":"10.1007\/0-387-26350-0_1"},{"issue":"2","key":"168_CR9","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1007\/s10458-006-5955-7","volume":"12","author":"RH Bordini","year":"2006","unstructured":"Bordini, R.H., Fisher, M., Visser, W., Wooldridge, M.: Verifying multi-agent programs by model checking. J. Auton. Agents Multi Agent Syst. 12(2), 239\u2013256 (2006)","journal-title":"J. Auton. Agents Multi Agent Syst."},{"key":"168_CR10","volume-title":"Programming Multi-agent Systems in AgentSpeak Using Jason","author":"RH Bordini","year":"2007","unstructured":"Bordini, R.H., H\u00fcbner, J.F., Wooldridge, M.: Programming Multi-agent Systems in AgentSpeak Using Jason. Wiley, Hoboken, NJ (2007)"},{"issue":"6","key":"168_CR11","doi-asserted-by":"crossref","first-page":"1385","DOI":"10.1093\/logcom\/exp029","volume":"19","author":"RH Bordini","year":"2009","unstructured":"Bordini, R.H., Fisher, M., Wooldridge, M., Visser, W.: Property-based slicing for agent verification. J. Log. Comput. 19(6), 1385\u20131425 (2009)","journal-title":"J. Log. Comput."},{"key":"168_CR12","volume-title":"The Correctness Problem in Computer Science","year":"1981","unstructured":"Boyer, R.S., Moore, J.S. (eds.): The Correctness Problem in Computer Science. Academic Press, London (1981)"},{"issue":"1","key":"168_CR13","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1109\/9.654885","volume":"43","author":"MS Branicky","year":"1998","unstructured":"Branicky, M.S., Borkar, V.S., Mitter, S.: A unified framework for hybrid control: model and optimal control theory. IEEE Trans. Automat. Contr. 43(1), 31\u201345 (1998)","journal-title":"IEEE Trans. Automat. Contr."},{"key":"168_CR14","volume-title":"Intentions, Plans, and Practical Reason","author":"ME Bratman","year":"1987","unstructured":"Bratman, M.E.: Intentions, Plans, and Practical Reason. Harvard University Press, Cambridge, MA (1987)"},{"key":"168_CR15","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1111\/j.1467-8640.1988.tb00284.x","volume":"4","author":"ME Bratman","year":"1988","unstructured":"Bratman, M.E., Israel, D.J., Pollack, M.E.: Plans and resource-bounded practical reasoning. Comput. Intell. 4, 349\u2013355 (1988)","journal-title":"Comput. Intell."},{"key":"168_CR16","doi-asserted-by":"crossref","unstructured":"Briand, X., Jeannet, B.: Combining control and data abstraction in the verification of hybrid systems. In: Formal Methods and Models for Codesign (MEMOCODE), pp. 141\u2013150. IEEE Computer Society (2009)","DOI":"10.1109\/MEMCOD.2009.5185390"},{"key":"168_CR17","doi-asserted-by":"crossref","unstructured":"Bujorianu, M.L.: Stochastic reachability analysis of hybrid systems. In: Communications and Control Engineering. Springer, London, UK (2012)","DOI":"10.1007\/978-1-4471-2795-6"},{"issue":"5","key":"168_CR18","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"EM Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512\u20131542 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"168_CR19","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge, MA (1999)"},{"key":"168_CR20","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1016\/0004-3702(90)90055-5","volume":"42","author":"PR Cohen","year":"1990","unstructured":"Cohen, P.R., Levesque, H.J.: Intention is choice with commitment. Artif. Intell. 42, 213\u2013261 (1990)","journal-title":"Artif. Intell."},{"key":"168_CR21","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C Courcoubetis","year":"1992","unstructured":"Courcoubetis, C., Vardi, M., Wolper, P., Yannakakis, M.: Memory-efficient algorithms for the verification of temporal properties. Form. Methods Syst. Des. 1, 275\u2013288 (1992)","journal-title":"Form. Methods Syst. Des."},{"key":"168_CR22","doi-asserted-by":"crossref","unstructured":"Damm, W., Disch, S., Hungar, H., Jacobs, S., Pang, J., Pigorsch, F., Scholl, C., Waldmann, U., Wirtz, B.: Exact state set representations in the verification of linear hybrid systems with large discrete state space. In: Proceedings of Automated Technology for Verification and Analysis, LNCS, vol. 4762, pp. 425\u2013440. Springer (2007)","DOI":"10.1007\/978-3-540-75596-8_30"},{"key":"168_CR23","doi-asserted-by":"crossref","unstructured":"Dastani, M., van Riemsdijk, M.B., Meyer, J.J.C.: Programming multi-agent systems in 3APL. In: Bordini, R.H., Dastani, M., Dix, J., El Fallah-Seghrouchni, A. (eds.) Multi-Agent Programming: Languages, Platforms and Applications, chap. 2, pp. 39\u201367. Springer, Berlin (2005)","DOI":"10.1007\/0-387-26350-0_2"},{"issue":"1","key":"168_CR24","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1016\/0004-3702(83)90015-2","volume":"20","author":"R Davis","year":"1983","unstructured":"Davis, R., Smith, R.G.: Negotiation as a metaphor for distributed problem solving. Artif. Intell. 20(1), 63\u2013109 (1983)","journal-title":"Artif. Intell."},{"issue":"2","key":"168_CR25","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1016\/j.jal.2005.12.014","volume":"5","author":"FS Boer de","year":"2007","unstructured":"de Boer, F.S., Hindriks, K.V., van der Hoek, W., Meyer, J.J.C.: A verification framework for agent programming with declarative goals. J. Appl. Log. 5(2), 277\u2013302 (2007)","journal-title":"J. Appl. Log."},{"issue":"5","key":"168_CR26","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1145\/359104.359106","volume":"22","author":"RA DeMillo","year":"1979","unstructured":"DeMillo, R.A., Lipton, R.J., Perlis, A.J.: Social processes and proofs of theorems of programs. ACM Commun. 22(5), 271\u2013280 (1979)","journal-title":"ACM Commun."},{"key":"168_CR27","unstructured":"Dennis, L.A., Farwer, B.: Gwendolen: A BDI language for verifiable agents. In: Workshop on Logic and the Simulation of Interaction and Reasoning, AISB (2008)"},{"key":"168_CR28","doi-asserted-by":"crossref","unstructured":"Dennis, L.A., Farwer, B., Bordini, R.H., Fisher, M., Wooldridge, M.: A Common Semantic Basis for BDI Languages. In: Proceedings of the 7th International Workshop on Programming Multiagent Systems (ProMAS), LNAI, vol. 4908, pp. 124\u2013139. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-79043-3_8"},{"key":"168_CR29","doi-asserted-by":"crossref","unstructured":"Dennis, L.A., Fisher, M., Lincoln, N., Lisitsa, A., Veres, S.M.: Declarative abstractions for agent based hybrid control systems. In: Proceedings of the 8th International Workshop on Declarative Agent Languages and Technologies (DALT), LNCS, vol. 6619, pp. 96\u2013111. Springer, Berlin (2010a)","DOI":"10.1007\/978-3-642-20715-0_6"},{"key":"168_CR30","unstructured":"Dennis, L.A., Fisher, M., Lincoln, N., Lisitsa, A., Veres, S.M.: Reducing code complexity in hybrid control systems. In: Proceedings of the 10th International Symposium on Artificial Intelligence, Robotics and Automation in Space (i-Sairas) (2010b)"},{"issue":"3","key":"168_CR31","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1109\/MIS.2010.88","volume":"25","author":"LA Dennis","year":"2010","unstructured":"Dennis, L.A., Fisher, M., Lisitsa, A., Lincoln, N., Veres, S.M.: Satellite control using rational agent programming. IEEE Intell. Syst. 25(3), 92\u201397 (2010c)","journal-title":"IEEE Intell. Syst."},{"issue":"1","key":"168_CR32","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/s10515-011-0088-x","volume":"19","author":"LA Dennis","year":"2012","unstructured":"Dennis, L.A., Fisher, M., Webster, M.P., Bordini, R.H.: Model checking agent programming languages. Autom. Softw. Eng. 19(1), 5\u201363 (2012)","journal-title":"Autom. Softw. Eng."},{"key":"168_CR33","doi-asserted-by":"crossref","unstructured":"Dennis, L.A., Fisher, M., Slavkovik, M., Webster, M.P.: Ethical choice in unforeseen circumstances. In: Proceedings Towards Autonomous Robotic Systems (TAROS), Oxford, UK (2013a)","DOI":"10.1007\/978-3-662-43645-5_45"},{"key":"168_CR34","doi-asserted-by":"crossref","unstructured":"Dennis, L.A., Fisher, M., Webster, M.P.: Using agent JPF to build models for other model checkers. In: Proceedings of Workshop on Computational Logic in Multi-Agent Systems (CLIMA), Corunna, Spain (2013b)","DOI":"10.1007\/978-3-642-40624-9_17"},{"issue":"1","key":"168_CR35","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1109\/69.43404","volume":"1","author":"EH Durfee","year":"1989","unstructured":"Durfee, E.H., Lesser, V.R., Corkill, D.D.: Trends in cooperative distributed problem solving. IEEE Trans. Knowl. Data Eng. 1(1), 63\u201383 (1989)","journal-title":"IEEE Trans. Knowl. Data Eng."},{"key":"168_CR36","first-page":"996","volume-title":"Handbook of Theoretical Computer Science","author":"EA Emerson","year":"1990","unstructured":"Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, pp. 996\u20131072. Elsevier, Amsterdam (1990)"},{"key":"168_CR37","unstructured":"Ezekiel, J., Lomuscio, A., Molnar, L., Veres, S.M., Peabody, M.: Verifying fault tolerance and self-diagnosability of an autonomous underwater vehicle. In: AI in Space: Intelligence beyond Planet Earth (IJCAI-11 Workshop) (2011)"},{"issue":"9","key":"168_CR38","doi-asserted-by":"crossref","first-page":"1048","DOI":"10.1145\/48529.48530","volume":"31","author":"JH Fetzer","year":"1988","unstructured":"Fetzer, J.H.: Program verification: the very idea. ACM Commun. 31(9), 1048\u20131063 (1988)","journal-title":"ACM Commun."},{"key":"168_CR39","doi-asserted-by":"crossref","DOI":"10.1002\/9781119991472","volume-title":"An introduction to practical formal methods using temporal logic","author":"M Fisher","year":"2011","unstructured":"Fisher, M.: An introduction to practical formal methods using temporal logic. Wiley, Hoboken, NJ (2011)"},{"issue":"9","key":"168_CR40","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1145\/2500468.2494558","volume":"56","author":"M Fisher","year":"2013","unstructured":"Fisher, M., Dennis, L.A., Webster, M.P.: Verifying autonomous systems. ACM Commun. 56(9), 84\u201393 (2013)","journal-title":"ACM Commun."},{"key":"168_CR41","doi-asserted-by":"crossref","unstructured":"Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. In: Proceedings of Hybrid Systems: Computation and Control, LNCS, vol. 3414, pp. 258\u2013273. Springer, Berlin (2005)","DOI":"10.1007\/978-3-540-31954-2_17"},{"key":"168_CR42","doi-asserted-by":"crossref","unstructured":"Frehse, G., Han, Z., Krogh, B.: Assume-guarantee reasoning for hybrid I\/O-automata by over-approximation of continuous interaction. In: Proceedings of 43rd IEEE Conference on Decision and Control (CDC), vol. 1, pp. 479\u2013484 (2004)","DOI":"10.1109\/CDC.2004.1428676"},{"key":"168_CR43","doi-asserted-by":"crossref","unstructured":"Gammie, P., van der Meyden, R.: MCK: model checking the logic of knowledge. In: Proceedings of the 16th International Conference on Computer Aided Verification (CAV), pp. 479\u2013483. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-27813-9_41"},{"key":"168_CR44","doi-asserted-by":"crossref","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Proceedings fo the 15th IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification, pp. 3\u201318. Chapman & Hall, London (1996)","DOI":"10.1007\/978-0-387-34892-6_1"},{"issue":"2","key":"168_CR45","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1109\/MCS.2008.931718","volume":"29","author":"R Goebel","year":"2009","unstructured":"Goebel, R., Sanfelice, R., Teel, A.: Hybrid dynamical systems. IEEE Control Syst. Mag. 29(2), 28\u201393 (2009)","journal-title":"IEEE Control Syst. Mag."},{"key":"168_CR46","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 278\u2013292. IEEE Computer Society Press (1996)","DOI":"10.1109\/LICS.1996.561342"},{"issue":"1\u20132","key":"168_CR47","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"TA Henzinger","year":"1997","unstructured":"Henzinger, T.A., Ho, P.H., Wong-Toi, H.: HYTECH: a model checker for hybrid systems. Int. J. Softw. Tools Technol. Transf. 1(1\u20132), 110\u2013122 (1997)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"2","key":"168_CR48","doi-asserted-by":"crossref","first-page":"53","DOI":"10.3233\/AIC-1996-9203","volume":"9","author":"A Heuerding","year":"1996","unstructured":"Heuerding, A., J\u00e4ger, G., Schwendimann, M., Seyfried, M.: A logics workbench. AI Commun. 9(2), 53\u201358 (1996)","journal-title":"AI Commun."},{"issue":"4","key":"168_CR49","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1023\/A:1010084620690","volume":"2","author":"KV Hindriks","year":"1999","unstructured":"Hindriks, K.V., de Boer, F.S., van der Hoek, W., Meyer, J.J.: Agent programming in 3APL. Auton. Agent Multi Agent Syst. 2(4), 357\u2013401 (1999)","journal-title":"Auton. Agent Multi Agent Syst."},{"key":"168_CR50","doi-asserted-by":"crossref","unstructured":"Hindriks, K.V., de Boer, F.S., van der Hoek, W., Meyer, J.J.: Agent programming with declarative goals. In: Intelligent Agents VII (Proceedings of the 6th Workshop on Agent Theories, Architectures, and Languages), LNAI, vol. 1986, pp. 228\u2013243. Springer, Berlin (2001)","DOI":"10.1007\/3-540-44631-1_16"},{"key":"168_CR51","volume-title":"Spin Model Checker: Primer and Reference Manual","author":"G Holzmann","year":"2004","unstructured":"Holzmann, G.: Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2004)"},{"key":"168_CR52","unstructured":"Hunter, J., Raimondi, F., Rungta, N., Stocker, R.: A synergistic and extensible framework for multi-agent system verification. In: Proceedings of the 13th International Conference on Autonomous Agents and Multiagent Systems (AAMAS), pp. 869\u2013876. IFAAMAS (2013)"},{"issue":"4","key":"168_CR53","doi-asserted-by":"crossref","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"CB Jones","year":"1983","unstructured":"Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5(4), 596\u2013619 (1983)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"168_CR54","volume-title":"Systematic Software Development Using VDM","author":"CB Jones","year":"1986","unstructured":"Jones, C.B.: Systematic Software Development Using VDM. Prentice Hall Int, Englewood Cliffs (1986)"},{"key":"168_CR55","doi-asserted-by":"crossref","unstructured":"Jongmans, S.S.T.Q., Hindriks, K.V., van Riemsdijk, M.B.: Model checking agent programs by using the program interpreter. In: Proceedings of the 11th International Workshop on Computational Logic in Multi-Agent Systems (CLIMA), LNCS, vol. 6245, pp. 219\u2013237. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-14977-1_17"},{"key":"168_CR56","doi-asserted-by":"crossref","unstructured":"Karim, S., Heinze, C.: Experiences with the design and implementation of an agent-based autonomous UAV controller. In: Proceedings of the 4th International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS), pp 19\u201326. ACM (2005)","DOI":"10.1145\/1082473.1082799"},{"issue":"1","key":"168_CR57","first-page":"39","volume":"22","author":"H Kitano","year":"2001","unstructured":"Kitano, H., Tadokoro, S.: RoboCup rescue: a grand challenge for multiagent and intelligent systems. AI Mag. 22(1), 39\u201352 (2001)","journal-title":"AI Mag."},{"key":"168_CR58","doi-asserted-by":"crossref","unstructured":"Kohn, W., Nerode, A.: Multiple agent autonomous hybrid control systems. In: Proceedings of the 31st Conference on Decision and Control (CDC), Tucson, USA, pp. 2956\u20132964 (1992)","DOI":"10.1109\/CDC.1992.371270"},{"key":"168_CR59","first-page":"869","volume-title":"Handbook of Modal Logic","author":"A Kurucz","year":"2006","unstructured":"Kurucz, A.: Combining modal logics. In: Blackburn, P., van Benthem, J., Wolter, F. (eds.) Handbook of Modal Logic, pp. 869\u2013924. Elsevier, Amsterdam (2006)"},{"key":"168_CR60","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM: probabilistic symbolic model checker. In: Proceedings of the 12th International Conference on Modelling Techniques and Tools for Computer Performance Evaluation (TOOLS), LNCS, vol. 2324. Springer, Berlin (2002)","DOI":"10.1007\/3-540-46029-2_13"},{"key":"168_CR61","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"L Lamport","year":"2003","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison Wesley, Reading (2003)"},{"issue":"2\u20133","key":"168_CR62","first-page":"237","volume":"21","author":"NK Lincoln","year":"2006","unstructured":"Lincoln, N.K., Veres, S.M.: Components of a vision assisted constrained autonomous satellite formation flying control system. Int. J. Adapt. Control Signal Process. 21(2\u20133), 237\u2013264 (2006)","journal-title":"Int. J. Adapt. Control Signal Process."},{"issue":"4","key":"168_CR63","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1109\/MCI.2013.2279559","volume":"8","author":"NK Lincoln","year":"2013","unstructured":"Lincoln, N.K., Veres, S.M., Dennis, L.A., Fisher, M., Lisitsa, A.: Autonomous asteroid exploration by rational agents. IEEE Comput. Intell. Mag. 8(4), 25\u201338 (2013)","journal-title":"IEEE Comput. Intell. Mag."},{"key":"168_CR64","doi-asserted-by":"crossref","unstructured":"Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: a model checker for the verification of multi-agent systems. In: Proceedings of the 21st International Conference on Computer Aided Verification (CAV), LNCS, vol. 5643, pp. 682\u2013688. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-02658-4_55"},{"key":"168_CR65","doi-asserted-by":"crossref","unstructured":"Lomuscio, A., Strulo, B., Walker, N., Wu, P.: Assume-guarantee reasoning with local specifications. In: Proceedings of the 12th International Conference on Formal Engineering Methods and Software Engineering (ICFEM), pp. 204\u2013219. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-16901-4_15"},{"key":"168_CR66","doi-asserted-by":"crossref","unstructured":"Loos, S.M., Platzer, A., Nistor, L.: Adaptive cruise control: hybrid, distributed, and now formally verified. In: Proceeding of the FM, LNCS, vol. 6664, pp. 42\u201356. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-21437-0_6"},{"key":"168_CR67","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Berlin (1992)"},{"key":"168_CR68","doi-asserted-by":"crossref","unstructured":"McMillan, K.: Circular compositional reasoning about liveness. In: Pierre, L., Kropf, T. (eds.) Correct Hardware Design and Verification Methods, Lecture Notes in Computer Science, vol. 1703, pp. 342\u2013346. Springer, Berlin, Heidelberg (1999). doi: 10.1007\/3-540-48153-2_30","DOI":"10.1007\/3-540-48153-2_30"},{"issue":"4","key":"168_CR69","doi-asserted-by":"crossref","first-page":"417","DOI":"10.1109\/TSE.1981.230844","volume":"7","author":"J Misra","year":"1981","unstructured":"Misra, J., Chandy, K.M.: Proofs of networks of processes. IEEE Trans. Softw. Eng. 7(4), 417\u2013426 (1981)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"1\u20132","key":"168_CR70","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1016\/S0004-3702(98)00068-X","volume":"103","author":"N Muscettola","year":"1998","unstructured":"Muscettola, N., Nayak, P.P., Pell, B., Williams, B.: Remote agent: to boldly go where no AI system has gone before. Artif. Intell. 103(1\u20132), 5\u201348 (1998)","journal-title":"Artif. Intell."},{"key":"168_CR71","doi-asserted-by":"crossref","unstructured":"Patchett, C., Ansell, D.: The development of an advanced autonomous integrated mission system for uninhabited air systems to meet UK airspace requirements. In: Proceedings of the International Conference on Intelligent Systems, Modelling and Simulation (ISMS), pp. 60\u201364 (2010)","DOI":"10.1109\/ISMS.2010.22"},{"key":"168_CR72","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-14509-4","volume-title":"Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics","author":"A Platzer","year":"2010","unstructured":"Platzer, A.: Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer, Heidelberg (2010)"},{"key":"168_CR73","doi-asserted-by":"crossref","unstructured":"Pokahr, A., Braubach, L., Lamersdorf, W.: Jadex: a BDI reasoning engine. In: Bordini, R.H., Dastani, M., Dix, J., El Fallah-Seghrouchni, A. (eds.) Multi-Agent Programming: Languages, Platforms and Applications, pp. 149\u2013174. Springer, Berlin (2005)","DOI":"10.1007\/0-387-26350-0_6"},{"issue":"3","key":"168_CR74","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/s10703-008-0049-6","volume":"32","author":"CS P\u0103s\u0103reanu","year":"2008","unstructured":"P\u0103s\u0103reanu, C.S., Giannakopoulou, D., Bobaru, M.G., Cobleigh, J.M., Barringer, H.: Learning to divide and conquer: applying the L* algorithm to automate assume-guarantee reasoning. Form. Methods Syst. Des. 32(3), 175\u2013205 (2008)","journal-title":"Form. Methods Syst. Des."},{"key":"168_CR75","doi-asserted-by":"crossref","unstructured":"Rao, A.: AgentSpeak(L): BDI agents speak out in a logical computable language. In: Agents Breaking Away: Proceedings of the 7th European Workshop on Modelling Autonomous Agents in a Multi-Agent World, LNCS, vol. 1038, pp. 42\u201355. Springer, Berlin (1996)","DOI":"10.1007\/BFb0031845"},{"key":"168_CR76","unstructured":"Rao, A.S., Georgeff, M.P.: Modeling agents within a BDI-architecture. In: Proceedings of the 2nd International Conference on Principles of Knowledge Representation and Reasoning (KR&R), pp. 473\u2013484. Morgan Kaufmann, San Mateo, CA (1991)"},{"key":"168_CR77","unstructured":"Rao, A.S., Georgeff, M.P.: An abstract architecture for rational agents. In: Proceedings of the International Conference on Knowledge Representation and Reasoning (KR&R), pp. 439\u2013449. Morgan Kaufmann, San Mateo, CA (1992)"},{"key":"168_CR78","unstructured":"Rao, A.S., Georgeff, M.P.: BDI agents: from theory to practice. In: Proceedings of the 1st International Conference on Multi-Agent Systems (ICMAS), San Francisco, USA, pp. 312\u2013319 (1995)"},{"issue":"1","key":"168_CR79","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/0004-3702(93)90034-9","volume":"60","author":"Y Shoham","year":"1993","unstructured":"Shoham, Y.: Agent-oriented programming. Artif. Intell. 60(1), 51\u201392 (1993)","journal-title":"Artif. Intell."},{"key":"168_CR80","unstructured":"Sierhuis, M.: Modeling and Simulating Work Practice. BRAHMS: a Multiagent Modeling and Simluation Language for Work System Analysis and Design. PhD thesis, Social Science and Informatics (SW), University of Amsterdam (2001)"},{"key":"168_CR81","doi-asserted-by":"crossref","unstructured":"Silva, P.S., Melo, A.C.: A formal environment model for multi-agent systems. In: Formal Methods: Foundations and Applications, LNCS, vol. 6527, pp 64\u201379. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-19829-8_5"},{"key":"168_CR82","doi-asserted-by":"crossref","unstructured":"Stocker, R., Dennis, L.A., Dixon, C., Fisher, M.: Verifying brahms human-robot teamwork models. In: Proceedings of the 13th European Conference on Logics in Artificial Intelligence (JELIA), LNCS, vol. 7519, pp. 385\u2013397. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-33353-8_30"},{"key":"168_CR83","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4419-0224-5","volume-title":"Verification and Control of Hybrid Systems: A Symbolic Approach","author":"P Tabuada","year":"2009","unstructured":"Tabuada, P.: Verification and Control of Hybrid Systems: A Symbolic Approach. Springer, Berlin (2009)"},{"key":"168_CR84","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1007\/s10703-007-0044-3","volume":"32","author":"A Tiwari","year":"2008","unstructured":"Tiwari, A.: Abstractions for hybrid systems. Form. Methods Syst. Des. 32, 57\u201383 (2008)","journal-title":"Form. Methods Syst. Des."},{"issue":"3","key":"168_CR85","doi-asserted-by":"crossref","first-page":"471","DOI":"10.1007\/s10458-008-9067-4","volume":"18","author":"MB Riemsdijk van","year":"2009","unstructured":"van Riemsdijk, M.B., Dastani, M., Meyer, J.J.: Goals in conflict: semantic foundations of goals in agent programming. Auton. Agent Multi Agent Syst. 18(3), 471\u2013500 (2009)","journal-title":"Auton. Agent Multi Agent Syst."},{"key":"168_CR86","doi-asserted-by":"crossref","unstructured":"Varaiya, P.: Design, simulation, and implementation of hybrid systems. In: Proceedings of the 20th International Conference on Application and Theory of Petri Nets (ICATPN), LNCS, vol. 1639, pp. 1\u20135. Springer, Berlin (1999)","DOI":"10.1007\/3-540-48745-X_1"},{"issue":"2","key":"168_CR87","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1023\/A:1022920129859","volume":"10","author":"W Visser","year":"2003","unstructured":"Visser, W., Havelund, K., Brat, G.P., Park, S., Lerda, F.: Model checking programs. Autom. Softw. Eng. 10(2), 203\u2013232 (2003)","journal-title":"Autom. Softw. Eng."},{"key":"168_CR88","doi-asserted-by":"crossref","unstructured":"Webster, M.P., Fisher, M., Cameron, N., Jump, M.: Formal methods for the certification of autonomous unmanned aircraft systems. In: Proceedings of the 30th International Conference on Computer Safety, Reliability and Security (SAFECOMP), LNCS, vol. 6894, pp. 228\u2013242. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-24270-0_17"},{"key":"168_CR89","doi-asserted-by":"crossref","unstructured":"Wei, C., Hindriks, K.V.: An agent-based cognitive robot architecture. In: Programming Multi-Agent Systems, LNCS, vol. 7837, pp. 54\u201371. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-38700-5_4"},{"key":"168_CR90","volume-title":"An Introduction to Multiagent Systems","author":"M Wooldridge","year":"2002","unstructured":"Wooldridge, M.: An Introduction to Multiagent Systems. Wiley, Hoboken, NJ (2002)"},{"key":"168_CR91","volume-title":"Foundations of Rational Agency. Applied Logic Series","year":"1999","unstructured":"Wooldridge, M., Rao, A. (eds.): Foundations of Rational Agency. Applied Logic Series. Kluwer Academic Publishers, Dordrecht (1999)"}],"container-title":["Automated Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-014-0168-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10515-014-0168-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-014-0168-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,24]],"date-time":"2020-08-24T03:23:58Z","timestamp":1598239438000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10515-014-0168-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,9,6]]},"references-count":91,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2016,9]]}},"alternative-id":["168"],"URL":"https:\/\/doi.org\/10.1007\/s10515-014-0168-9","relation":{},"ISSN":["0928-8910","1573-7535"],"issn-type":[{"value":"0928-8910","type":"print"},{"value":"1573-7535","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,9,6]]}}}