doi:10.1017/S0269888914000228

Arapinis M., Calder M., Dennis L. A., Fisher M., Gray P. D., Konur S., Miller A., Ritter E., Ryan M., Schewe S., Unsworth C. & Yasmin R.2009. Towards the verification of pervasive systems. ECEASST Electronic Communications of the EASST22, 1–15.

Bakhouya M., Campbell R., Coronato A., de Pietro G. & Ranganathan A.2012. Introduction to special section on formal methods in pervasive computing. ACM Transactions on Autonomous and Adaptive Systems6(1–6), 9.

Birkedal L., Bundgaard M., Damgaard T. C., Debois S., Elsborg E., Glenstrup A. J., Hildebr T., Milner R. & Niss H.2006. Bigraphical programming languages for pervasive computing. In Proceedings of the International Workshop on Combining Theory and Systems Building in Pervasive Computing, 653–658.

Bordini R. H., Dastani M., Dix J. & El Fallah Seghrouchni A. (eds) 2005. Multi-Agent Programming: Languages, Platforms and Applications, Springer.

Bordini R. H., Dastani M., Dix J. & El Fallah-Seghrouchni A. (eds) 2009. Multi-Agent Programming: Languages, Tools and Applications, Springer.

Bordini R. H., Dennis L. A., Farwer B. & Fisher M.2008. Automated verification of multi-agent programs. In Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE), 69–78.

Bordini R. H., Fisher M., Visser W. & Wooldridge M.2006. Verifying multi-agent programs by model checking. Journal of Autonomous Agents and Multi-Agent Systems12(2), 239–256.

Bordini R. H., Hübner J. F. & Vieira R.2005. Jason and the Golden Fleece of agent-oriented programming, chapter 1. In Bordini, R. H., Dastani, M., Dix, J. & Seghrouchni, E. F (eds), 3–37.

Boytsov A. & Zaslavsky A.2011. Formal Verification of the Context Model — Enhanced Context Spaces Theory Approach. Technical report, Department of Computer Science, Space and Electrical Engineering, SE-971 87, Lulea University of Technology.

Chen H., Finin T. & Joshi A.2003. An ontology for context-aware pervasive computing environments. Knowledge Engineering Review. Special Issue on Ontologies for Distributed Systems, 18, 197–207.

Clancey W., Sierhuis M., Kaskiris C. & van Hoof R.2003. Advantages of Brahms for specifying and implementing a multiagent human-robotic exploration system. In Proceedings of the Sixteenth International Florida Artificial Intelligence Research Society Conference (FLAIRS), 7–11. AAAI Press.

Clarke E. M., Grumberg O. & Peled D. A.1999. Model Checking, MIT Press.

Dastani M., van Riemsdijk M. B. & Meyer J.-J. C.2005. Programming multi-agent systems in 3APL, chapter 2. In Multi-Agent Programming, Bordini, R. H., Dastani, M., Dix, J. & Seghrouchni, E. F (eds), Springer, 39–67.

Dennis L. A. & Farwer B.2008. Gwendolen: a BDI language for verifiable agents. In Proceedings of the AISB’08 Workshop on Logic and the Simulation of Interaction and Reasoning, Löwe, B. (ed.). AISB.

Dennis L. A., Fisher M. & Hepple A.2008. Language constructs for multi-agent programming. In Proceedings of the 8th Workshop on Computational Logic in Multi-Agent Systems (CLIMA), LNAI 5056, 137–156. Springer.

Dennis L. A., Fisher M., Webster M. & Bordini R. H.2012. Model checking agent programming languages. Automated Software Engineering19(1), 5–63.

Dobson S., Denazis S., Fernández A., Gati D., Gelenbe E., Massacci F., Nixon P., Saffre F., Schmidt N. & Zambonelli F.2006. A survey of autonomic communications. ACM Transactions on Autonomous and Adaptive Systems1(2), 223–259.

Dobson S., Sterritt R., Nixon P. & Hinchey M.2010. Fulfilling the vision of autonomic computing. IEEE Computer43(1), 35–41.

Finger M. & Gabbay D. M.1996. Combining temporal logic systems. Notre Dame Journal of Formal Logic37(2), 204–232.

Fisher M., Dennis L. & Webster M.2013. Verifying autonomous systems. Communications of the ACM56(9), 84–93.

Fisher M. & Hepple A.2009. Executing logical agent specifications. In Multi-Agent Programming: Languages, Tools and Applications R. H. Bordini, M. Dastani, J. Dix & A. El Fallah-Seghrouchni (eds), 1–27Springer.

Fisher M., Singh M., Spears D. & Wooldridge M.2007. Guest editorial: logic-based agent verification. Journal of Applied Logic5(2), 193–195.

Gabbay D., Kurucz A., Wolter F. & Zakharyaschev M.2003. Many-Dimensional Modal Logics: Theory and Applications. Studies in Logic and the Foundations of Mathematics, 148Elsevier Science.

Georgeff M. P. & Lansky A. L.1987. Reactive reasoning and planning. In Proceedings of the 6th National Conference on Artificial Intelligence (AAAI), 677–682. AAAI Press, .

Gorrieri R., Herzog U. & Hillston J.2002. Unified specification and performance evaluation using stochastic process algebras. Performance Evaluation50(2/3), 79–82.

Greenfield A.2006. Everyware, New Riders Publishing.

Henricksen K. & Indulska J.2004. A software engineering framework for context-aware pervasive computing. In Proceedings 2nd IEEE Conference on Pervasive Computing and Communications, 77–86.

Hepple A.2010. Agents, Context, and Logic. PhD thesis, Department of Computer Science, University of Liverpool.

Hepple A., Dennis L. A. & Fisher M.2008. A common basis for agent organisations in BDI languages. In Proceedings of the International Workshop on Languages, Methodologies and Development Tools for Multi-Agent Systems (LADS), Lecture Notes in Artificial Intelligence 5118, 171–188. Springer-Verlag.

Hindriks K., de Boer F., van der Hoek W. & Meyer J.-J.2001. Agent programming with declarative goals. In Intelligent Agents VII, Lecture Notes in Artificial Intelligence 1986, 228–243. Springer-Verlag.

Holzmann G.2003. Spin Model Checker, The: Primer and Reference Manual, 1st edition. Addison-Wesley Professional.

Hunter J., Raimondi F., Rungta N. & Stocker R.2013. A synergistic and extensible framework for multi-agent system verification. In Proceedings of International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS), 869–876. IFAAMAS.

Isern D., Moreno A., Sanchez D., Hajnal A., Pedone G. & Varga L.2011. Agent-based execution of personalised home care treatments. Applied Intelligence34, 155–180.

Jongmans S.-S. T. Q., Hindriks K. V. & van Riemsdijk M. B.2010. 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 6245, 219–237. Springer.

Knox S., Shannon R., Coyle L., Clear A., Dobson S., Quigley A. & Nixon P.2008. Scatterbox: context-aware message management. Revue d’Intelligence Artificielle22(5), 549–568.

Konur S.2013. A survey on temporal logics for specifying and verifying real-time systems. Frontiers of Computer Science7(3), 370–403.

Konur S., Fisher M., Dobson S. & Knox S.2014. Formal verification of a pervasive messaging system. Formal Aspects of Computing26(4), 677–694.

Konur S., Fisher M. & Schewe S.2013. Combined model checking for temporal, probabilistic, and real-time logics. Theoretical Computer Science503, 61–88.

Kwiatkowska M., Norman G. & Parker D.2002. PRISM: probabilistic symbolic model checker, Lecture Notes in Computer Science 2324, 200–204. Springer.

NASA (Astronaut-Robot-Team-Concept). NASA astronaut robot partner. http://history.nasa.gov/DPT/DPT.htm.

PRISM2013. Probabilistic symbolic model checker. http://www.cs.bham.ac.uk/ dxp/prism.

Ranganathan A. & Campbell R. H.2008. Provably correct pervasive computing environments. In IEEE International Conference on Pervasive Computing and Communications, 160–169.

Rao A. S.1996. AgentSpeak(L): BDI agents speak out in a logical computable language. In Proceedings of the 7th European Workshop on Modelling Autonomous Agents in a Multi-Agent World, (MAAMAW), LNAI 1038, 748–752. Springer-Verlag.

Rao A. S. & Georgeff M. P.1991. Modeling agents within a BDI-architecture. In Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning (KR). Morgan Kaufmann.

Rao A. S. & Georgeff M. P.1992. An abstract architecture for rational agents. In Proceedings of the International Conference on Knowledge Representation and Reasoning (KR), 439–449.

Rao A. S. & Georgeff M. P.1995. BDI agents: from theory to practice. In Proceedings of the 1st International Conference on Multi-Agent Systems (ICMAS), 312–319. IEEE Press.

RoboSafe2013. Trustworthy robotic assistants project. http://www.robosafe.org.

Rosa P. M. P., Dias J. A., Lopes I. M. C., Rodrigues J. J. P. C. & Lin K.2012. An ubiquitous mobile multimedia system for events agenda. In WCNC, 2103–2107.

Sierhuis M.2001. Modeling and Simulating Work Practice. BRAHMS: A Multiagent Modeling and Simulation Language for Work System Analysis and Design. PhD thesis, SIKS Dissertation Series No. 2001-10, Social Science and Informatics (SWI), University of Amsterdam.

Sierhuis M.2006. Multiagent modeling and simulation in human-robot mission operations. http://ic.arc.nasa.gov/ic/publications).

Sierhuis M., Bradshaw J. M., Acquisti A., Hoof R. V., Jeffers R. & Uszok A.2003. Human-agent teamwork and adjustable autonomy in practice. In Proceedings of the 7th International Symposium on Artificial Intelligence, Robotics and Automation in Space (i-SAIRAS).

Sierhuis M. & Clancey W. J.2002. Modeling and simulating work practice: a human-centered method for work systems design. IEEE Intelligent Systems17(5), 32–41.

Stocker R., Dennis L., Dixon C. & Fisher M.2012. Verifying Brahms human-robot teamwork models. In Proceedings of the 13th European Conference on Logics in Artificial Intelligence, JELIA’12, 385–397. Springer-Verlag.

Stocker R., Sierhuis M., Dennis L., Dixon C. & Fisher M.2011. A formal semantics for Brahms. In Proceedings of the 12th International Conference on Computational Logic in Multi-Agent Systems, CLIMA’11, 259–274. Springer-Verlag.

Strang T. & Popien C. L.2004. A context modeling survey. In Workshop on Advanced Context Modelling, Reasoning and Management, UbiComp 2004 – The Sixth International Conference on Ubiquitous Computing.

Turner K. J.2012. Advances in Home Care Technologies: Results of the MATCH Project, IOS Press.

van Hoof R.2000. Brahms website. http://www.agentisolutions.com.

Visser W., Havelund K., Brat G. & Park S.2000. Model checking programs. In Proceedings of the 15th International Conference on Automated Software Engineering (ASE), 3–12. IEEE Computer Society.

Want R., Pering T., Borriello G. & Farkas K.2002. Disappearing hardware. Pervasive Computing1(1), 36–47.

Weiser M.1993. Some computer science issues in ubiquitous computing. Communications of the ACM36(7), 74–84.

Wooldridge M.2002. An Introduction to Multiagent Systems, John Wiley & Sons.