Modelling and verifying BDI agents with bigraphs

Bratman, 1987 Rao, 1996, AgentSpeak (L): BDI agents speak out in a logical computable language, 42 Hindriks, 1999, Agent programming in 3APL, Auton. Agents Multi-Agent Syst., 2, 357, 10.1023/A:1010084620690 Dastani, 2008, 2APL: a practical agent programming language, Auton. Agents Multi-Agent Syst., 16, 214, 10.1007/s10458-008-9036-y Bordini, 2007 Sardina, 2006, Hierarchical planning in BDI agent programming languages: a formal approach, 1001 Benfield, 2006, Making a strong business case for multiagent technology, 10 Braubach, 2014, Negotiation-based patient scheduling in hospitals, 107 McArthur, 2007, Multi-agent systems for power engineering applications – part i: concepts, approaches, and technical challenges, vol. 22, IEEE, 22, 1743 Brat, 2006, Verification of autonomous systems for space applications Lestingi, 2020, Formal verification of human-robot interaction in healthcare scenarios, 303 Bordini, 2006, Verifying multi-agent programs by model checking, Auton. Agents Multi-Agent Syst., 12, 239, 10.1007/s10458-006-5955-7 Holzmann, 1991 Holzmann, 1997, The model checker SPIN, IEEE Trans. Softw. Eng., 23, 279, 10.1109/32.588521 Dennis, 2008, A flexible framework for verifying agent programs, 1303 Brat, 2000, Model checking programs, 3 Milner, 2008, Bigraphs and their algebra, Electron. Notes Theor. Comput. Sci., 209, 5, 10.1016/j.entcs.2008.04.002 Bundgaard, 2006, Typed polyadic pi-calculus in bigraphs, 1 Sevegnani, 2016, BigraphER: rewriting and analysis engine for bigraphs, 494 Archibald, 2020, Conditional bigraphs, 3 Clavel, 2020, Maude manual (version 3.0) Benford, 2016, On lions, impala, and bigraphs: modelling interactions in physical/virtual spaces, ACM Trans. Comput.-Hum. Interact., 23, 1, 10.1145/2882784 Sardina, 2011, A BDI agent programming language with failure handling, declarative goals, and planning, Auton. Agents Multi-Agent Syst., 18, 10.1007/s10458-010-9130-9 Milner, 2009 Meseguer, 2012, Twenty years of rewriting logic, J. Log. Algebraic Methods Program., 81, 721, 10.1016/j.jlap.2012.06.003 Calder, 2014, Modelling IEEE 802.11 CSMA/CA RTS/CTS with stochastic bigraphs with sharing, Form. Asp. Comput., 26, 537, 10.1007/s00165-012-0270-3 Plotkin, 1981, A Structural Approach to Operational Semantics Logan, 2017, Progressing intention progression: a call for a goal-plan tree contest, 768 Xu, 2019, Intention interleaving via classical replanning, 85 Archibald Groote, 1993, Transition system specifications with negative premises, Theor. Comput. Sci., 118, 263, 10.1016/0304-3975(93)90111-6 van Glabbeek, 2004, The meaning of negative premises in transition system specifications ii, J. Log. Algebraic Program., 60, 229, 10.1016/j.jlap.2004.03.007 Clarke, 1981, Design and synthesis of synchronization skeletons using branching time temporal logic, 52 Mosses, 2004, Modular structural operational semantics, J. Log. Algebraic Methods Program., 60–61, 195, 10.1016/j.jlap.2004.03.008 Harland, 2014, An operational semantics for the goal life-cycle in BDI agents, Auton. Agents Multi-Agent Syst., 28, 682, 10.1007/s10458-013-9238-9 Harland, 2017, Aborting, suspending, and resuming goals and plans in BDI agents, Auton. Agents Multi-Agent Syst., 31, 288, 10.1007/s10458-015-9322-4 Archibald, 2021, Practical bigraphs via subgraph isomorphism Emerson, 1990, Temporal and modal logic, 995 Dennis, 2017 Dennis, 2012, Model checking agent programming languages, Autom. Softw. Eng., 19, 5, 10.1007/s10515-011-0088-x Dennis, 2018, The MCAPL framework including the agent infrastructure layer and agent Java PathFinder, J. Open Sour. Softw. Dennis, 2016, Formal verification of ethical choices in autonomous systems, Robot. Auton. Syst., 77, 1, 10.1016/j.robot.2015.11.012 Hindriks, 2000, Agent programming with declarative goals, 228 Dennis, 2018, Two-stage agent program verification, J. Log. Comput., 28, 499, 10.1093/logcom/exv002 Kwiatkowska, 2011, PRISM 4.0: verification of probabilistic real-time systems, 585 Izzo, 2016, A stochastically verifiable autonomous control architecture with reasoning, 4985 Dennis, 2016, Practical verification of decision-making in agent-based autonomous systems, Autom. Softw. Eng., 23, 305, 10.1007/s10515-014-0168-9 Wooldridge, 2006, Model checking for multiagent systems: the MABLE language and its applications, Int. J. Artif. Intell. Tools, 15, 195, 10.1142/S0218213006002631 Shapiro, 2002, The cognitive agents specification language and verification environment for multiagent systems, 19 Eker, 2004, The Maude LTL model checker, Electron. Notes Theor. Comput. Sci., 71, 162, 10.1016/S1571-0661(05)82534-4 Van Riemsdijk, 2006, Prototyping 3APL in the Maude term rewriting language, 95 Doan, 2014, Verifying heterogeneous multi-agent programs, 149 Jongmans, 2010, Model checking agent programs by using the program interpreter, 219 Bordini, 2004, State-space reduction techniques in agent verification, 896 Bordini, 2009, Property-based slicing for agent verification, J. Log. Comput., 19, 1385, 10.1093/logcom/exp029 Winikoff, 2018, Slicing agent programs for more efficient verification, 139 Jongmans, 2011, State space reduction for model checking agent programs, 133 Milner, 2006, Pure bigraphs: structure and dynamics, Inf. Comput., 204, 60, 10.1016/j.ic.2005.07.003 Jensen, 2006 Sevegnani, 2014, Towards a bigraphical encoding of actors Mansutti, 2014, Multi-agent systems design and prototyping with bigraphical reactive systems, 201 Dib, 2015, Model checking of multi-agent system architectures using BigMC, 1717, 10.15439/2015F300 Archibald Bianco, 1995, Model checking of probabilistic and nondeterministic systems, 499 Archibald, 2021, Probabilistic BDI agents: actions, plans and intentions De Silva, 2020, An operational semantics for true concurrency in BDI agent systems, 34, 7119 Archibald, 2021, Observable and attention-directing BDI agents for human-autonomy teaming, vol. 348, 167