[2017]  [2016]  [2015]  [2014]  [2013]  [2012]  [2011]  [2010] 

 [2009]  [2008]  [2007]  [2006]  [2005]  [2004]  [2003]  [2002]  [2001]  [2000]

 [1999]  [1998]  [1997]  [1996]  [1995]  [1994]  [1993]  [1992]  [1991]  [pre-1990]

2017

• Kamali, M., Dennis, L. A., McAree, O., Fisher, M. and Veres, S. M. Formal Verification of Autonomous Vehicle Platooning Science of Computer Programming 148:88-106. [Abstract]

  The coordination of multiple autonomous vehicles into convoys or platoons is expected on our highways in the near future. However, before such platoons can be deployed, the behaviours of the vehicles in these platoons must be certified. This is non-trivial and goes beyond current certification requirements, for human-controlled vehicles, in that these vehicles can act autonomously. In this paper, we show how formal verification can contribute to the analysis of these new, and increasingly autonomous, systems. An appropriate overall representation for vehicle platooning is as a multi-agent system in which each agent captures the “autonomous decisions” carried out by each vehicle. In order to ensure that these autonomous decision-making agents in vehicle platoons never violate safety requirements, we use formal verification. However, as the formal verification technique used to verify the individual agent's code does not scale to the full system, and as the global system verification technique does not capture the essential verification of autonomous behaviour, we use a combination of the two approaches. This mixed strategy allows us to verify safety requirements not only of a model of the system, but of the actual agent code used to program the autonomous vehicles.

• Gainer, P., Linker, S., Dixon, C., Hustadt, U., and Fisher, M. Investigating Parametric Influence on Discrete Synchronisation Protocols Using Quantitative Model Checking In Proc. 14th International Conference on Quantitative Evaluation of Systems, pp224-239, 2017. [Abstract]

  Synchronisation is an emergent phenomenon observable in nature. Natural synchronising systems have inspired the development of protocols for achieving coordination in a diverse range of distributed dynamic systems. Spontaneously synchronising systems can be mathematically modelled as coupled oscillators. In this paper we present a novel approach using model checking to reason about achieving synchrony for different models of synchronisation. We describe a general, formal population model where oscillators interact at discrete moments in time, and whose cycles are sequences of discrete states. Using the probabilistic model checker Prism, we investigate the influence of various parameters of the model on the likelihood of, and time required for, achieving synchronisation.

• Fernandes, L. E. R., Custodio, V., Alves, G. V., and Fisher, M. A Rational Agent Controlling an Autonomous Vehicle: Implementation and Formal Verification In Proc. First Workshop on Formal Verification of Autonomous Vehicles (FVAV), Electronic Proceedings in Theoretical Computer Science 257, pp35–42, 2017. [Abstract]

  The development and deployment of Autonomous Vehicles (AVs) on our roads is not only realistic in the near future but can also bring significant benefits. In particular, it can potentially solve several problems relating to vehicles and traffic, for instance: (i) possible reduction of traffic congestion, with the consequence of improved fuel economy and reduced driver inactivity; (ii) possible reduction in the number of accidents, assuming that an AV can minimise the human errors that often cause traffic accidents; and (iii) increased ease of parking, especially when one considers the potential for shared AVs. In order to deploy an AV there are significant steps that must be completed in terms of hardware and software. As expected, software components play a key role in the complex AV system and so, at least for safety, we should assess the correctness of these components. In this paper, we are concerned with the high-level software component(s) responsible for the decisions in an AV. We intend to model an AV capable of navigation; obstacle avoidance; obstacle selection (when a crash is unavoidable) and vehicle recovery, etc, using a rational agent. To achieve this, we have established the following stages. First, the agent plans and actions have been implemented within the Gwendolen agent programming language. Second, we have built a simulated automotive environment in the Java language. Third, we have formally specified some of the required agent properties through LTL formulae, which are then formally verified with the AJPF verification tool. Finally, within the MCAPL framework (which comprises all the tools used in previous stages) we have obtained formal verification of our AV agent in terms of its specific behaviours. For example, the agent plans responsible for selecting an obstacle with low potential damage, instead of a higher damage obstacle (when possible) can be formally verified within MCAPL. We must emphasise that the major goal (of our present approach) lies in the formal verification of agent plans, rather than evaluating real-world applications. For this reason we utilised a simple matrix representation concerning the environment used by our agent.

• Gainer, P., Dixon, C., Dautenhahn, K., Fisher, M., Hustadt, U., Saunders, J., and Webster, M. CRutoN: Automatic Verification of a Robotic Assistant's Behaviours In Proc. FMICS-AVoCS, pp119-133, 2017. [Abstract]

  The Care-O-bot is an autonomous robotic assistant that can support people in domestic and other environments. The behaviour of the robot can be defined by a set of high level control rules. The adoption and further development of such robotic assistants is inhibited by the absence of assurances about their safety. In previous work, formal models of the robot behaviour and its environment were constructed by hand and model checkers were then used to check whether desirable formal temporal properties were satisfied for all possible system behaviours. In this paper we describe the details of the software CRutoN, that provides an automatic translation from sets of robot control rules into input for the model checker NuSMV. We compare our work with previous attempts to formally verify the robot control rules, discuss the potential applications of the approach, and consider future directions of research..

2016

• Dennis, L. A., Fisher, M., Lincoln, N., Lisitsa, A., and Veres, S. M. Practical Verification of Decision-Making in Agent-Based Autonomous Systems Journal of Automated Software Engineering 23(3):305-359. [Abstract]

  The coordination of multiple autonomous vehicles into convoys or platoons is expected on our highways in the near future. However, before such platoons can be deployed, the behaviours of the vehicles in these platoons must be certified. This is non-trivial and goes beyond current certification requirements, for human-controlled vehicles, in that these vehicles can act autonomously. In this paper, we show how formal verification can contribute to the analysis of these new, and increasingly autonomous, systems. An appropriate overall representation for vehicle platooning is as a multi-agent system in which each agent captures the “autonomous decisions” carried out by each vehicle. In order to ensure that these autonomous decision-making agents in vehicle platoons never violate safety requirements, we use formal verification. However, as the formal verification technique used to verify the individual agent's code does not scale to the full system, and as the global system verification technique does not capture the essential verification of autonomous behaviour, we use a combination of the two approaches. This mixed strategy allows us to verify safety requirements not only of a model of the system, but of the actual agent code used to program the autonomous vehicles.

• Fisher, M., List, C., Slavkovik, M., and Winfield, A. F. T. Engineering Moral Agents -- from Human Morality to Artificial Morality Dagstuhl Reports 6(5):114-137. [Abstract]

  This report documents the programme of, and outcomes from, the Dagstuhl Seminar 16222 on "Engineering Moral Agents -- from Human Morality to Artificial Morality". Artificial morality is an emerging area of research within artificial intelligence (AI), concerned with the problem of designing artificial agents that behave as moral agents, i.e. adhere to moral, legal, and social norms. Context-aware, autonomous, and intelligent systems are becoming a presence in our society and are increasingly involved in making decisions that affect our lives. While humanity has developed formal legal and informal moral and social norms to govern its own social interactions, there are no similar regulatory structures that apply to non-human agents. The seminar focused on questions of how to formalise, "quantify", qualify, validate, verify, and modify the ``ethics" of moral machines. Key issues included the following: How to build regulatory structures that address (un)ethical machine behaviour? What are the wider societal, legal, and economic implications of introducing AI machines into our society? How to develop "computational" ethics and what are the difficult challenges that need to be addressed? When organising this workshop, we aimed to bring together communities of researchers from moral philosophy and from artificial intelligence most concerned with this topic. This is a long-term endeavour, but the seminar was successful in laying the foundations and connections for accomplishing it.

• Dennis, L. A., Aitken, J. M., Collenette, J., Cucco, E., Kamali, M., McAree, O., Shaukat, A., Atkinson, K. M., Gao, Y, Veres, S. M., and Fisher, M. Agent-Based Autonomous Systems and Abstraction Engines: Theory Meets Practice. In Proc. 17th Conference on Towards Autonomous Robotic Systems (TAROS). LNAI Volume 9716, pages 75-86, Springer, 2016. [Abstract]

  We report on experiences in the development of hybrid autonomous systems where high-level decisions are made by a rational agent. This rational agent interacts with other sub-systems via an abstraction engine. We describe three systems we have developed using the EASS BDI agent programming language and framework which supports this architecture. As a result of these experiences we recommend changes to the theoretical operational semantics that underpins the EASS framework and present a fourth implementation using the new semantics.

• Dennis, L. A., Fisher, M., Slavkovik, M., and Webster, M. Formal Verification of Ethical Choices in Autonomous Systems. Robotics and Autonomous Systems 77:1-14, 2016. [Abstract]

  Autonomous systems such as unmanned vehicles are begining to operate within society. All participants in society are required to follow specific regulations and laws. An autonomous system cannot be an exception. Inevitably an autonomous system will find itself in a situation in which it needs to not only choose to obey a rule or not, but also make a complex ethical decision. However, there exists no obvious way to implement the human understanding of ethical behaviour in computers. Even if we enable autonomous systems to distinguish between more and less ethical alternatives, how can we be sure that they would choose right? We consider autonomous systems with a hybrid architecture in which the highest level of reasoning is executed by a rational (BDI) agent. For such a system, formal verification has been used successfully to prove that specific rules of behaviour are observed when making decisions. We propose a theoretical framework for ethical plan selection that can be formally verified. We implement a rational agent that incorporates a given ethical policy in its plan selection and show that we can formally verify that the agent chooses to execute, to the best of its beliefs, the most ethical available plan.

• Webster, M., Dixon, C., Fisher, M., Salem, M., Saunders, J., Koay, K-L., Dautenhahn, K., and Saez-Pons, J. Toward Reliable Autonomous Robotic Assistants Through Formal Verification: A Case Study IEEE Transactions on Human-Machine Systems 46(2):186-196. [Abstract]

  It is essential for robots working in close proximity to people to be both safe and trustworthy. We present a case study on formal verification for a high-level planner/scheduler for the Care-O-bot, an autonomous personal robotic assistant. We describe how a model of the Care-O-bot and its environment was developed using Brahms, a multiagent workflow language. Formal verification was then carried out by automatically translating this model to the input language of an existing model checker. Four sample properties based on system requirements were verified. We then refined the environment model three times to increase its accuracy and the persuasiveness of the formal verification results. The first refinement uses a user activity log based on real-life experiments, but is deterministic. The second refinement uses the activities from the user activity log nondeterministically. The third refinement uses “conjoined activities” based on an observation that many user activities can overlap. The four samples properties were verified for each refinement of the environment model. Finally, we discuss the approach of environment model refinement with respect to this case study.

• Dennis, L. A., Slavkovik, M., and Fisher, M. “How Did They Know” - Model-Checking for Analysis of Information Leakage in Social Networks. In Proc. Workshop on Coordination, Organizations, Institutions, and Norms in Agent Systems (COIN@AAMAS/ECAI), pp42-59, 2016. [Abstract]

  We examine the use of model-checking in the analysis of information leakage in social networks. We take previous work on the formal analysis of digital crowds and show how a variation on the formalism can naturally model the interaction of people and groups of followers in intersecting social networks. We then show how probabilistic models of the forwarding and reposting behaviour of individuals can be used to analyse the risk that information will leak to unwanted parties. We illustrate our approach by analysing several simple examples.

2015

• Dennis, L. A., Fisher, M., and Webster, M. Two-stage Agent Program Verification. Journal of Logic and Computation, 2015. [Abstract]

  We describe an extension to the AJPF agent program model-checker so that it may be used to generate models for input into other, non-agent, model-checkers. We motivate this adaptation, arguing that it potentially improves the efficiency of the model-checking process and provides access to richer property specification languages. We illustrate the approach by describing the export of AJPF program models to both the SPIN and Prism model-checkers. We also investigate, experimentally, the effect the process has on the overall efficiency of model-checking.

• Konur, S., and Fisher, M. A Roadmap to Pervasive Systems Verification. Knowledge Engineering Review 30(3):324-341, 2015. [Abstract]

  The complexity of pervasive systems arises from the many different aspects that such systems possess. A typical pervasive system may be autonomous, distributed, concurrent and context based, and may involve humans and robotic devices working together. If we wish to formally verify the behaviour of such systems, the formal methods for pervasive systems will surely also be complex. In this paper, we move towards being able to formally verify pervasive systems and outline our approach wherein we distinguish four distinct dimensions within pervasive system behaviour and utilize different, but appropriate, formal techniques for verifying each one..

• Slavkovik, M., Dennis, L. A., and Fisher, M. An Abstract Formal Basis for Digital Crowds. Distributed and Parallel Databases 33(1):3-31, 2015. [Abstract]

  Crowdsourcing, together with its related approaches, has become very popular in recent years. All crowdsourcing processes involve the participation of a digital crowd, a large number of people that access a single Internet platform or shared service. In this paper we explore the possibility of applying formal methods, typically used for the verification of software and hardware systems, in analysing the behaviour of a digital crowd. More precisely, we provide a formal description language for specifying digital crowds. We represent digital crowds in which the agents do not directly communicate with each other. We further show how this specification can provide the basis for sophisticated formal methods, in particular formal verification.

• Dennis, L. A., Fisher, M., and Winfield, A. F. T. Towards Verifiably Ethical Robot Behaviour. To appear in AAAI-15 Workshop on AI and Ethics.

• Fisher, M., Reed, N., and Savirimuthu, J. Misplaced Trust?. Engineering & Technology Reference, 2015. Pre-publication version available here

• Patchett, C., Jump, M. and Fisher, M. Safety and Certification of Unmanned Air Systems. Engineering & Technology Reference, 2015. Pre-publication version available here

• van Riemsdijk, M. Birna, Dennis, L. A., Fisher, M., and Hindriks, K. V. A Semantic Framework for Socially Adaptive Agents: Towards strong norm compliance. In Proc. 14th International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS), 2015. [Abstract]

  We address the question of how an agent can adapt its behavior to comply with newly adopted norms. This is particularly relevant in the case of open systems where agents may enter and leave norm-governed social contexts not known at design time. This requires norms to be explicitly and separately stated and presented to an agent as rules to which it then can try to adapt its behavior. We propose a formal semantic framework that specifies an execution mechanism for such socially adaptive agents. This framework is based on expressing norms using Linear Temporal Logic. The formality of the framework allows us to rigorously study its norm compliance properties. A weak form of norm compliance allows agents to abort execution in order to prevent norm violation. In this paper we investigate a stronger notion of norm compliance that is evaluated over infinite traces. We show that it is not possible for all agents to be strongly compliant with any arbitrary set of norms. We then investigate situations when strong norm compliance can be guaranteed.

2014

• Dixon, C., Webster, M., Saunders J., Fisher, M., and Dautenhahn, K. “The Fridge Door is Open” -- Temporal Verification of a Robotic Assistant's Behaviours. In Advances in Autonomous Robotic Systems ( Proc. TAROS). LNAI Volume 8717, pages 97-108, Springer, 2014. (Paper won the Springer Best Paper Award.) [Abstract]

  Robotic assistants are being designed to help, or work with, humans in a variety of situations from assistance within domestic situations, through medical care, to industrial settings. Whilst robots have been used in industry for some time they are often limited in terms of their range of movement or range of tasks. A new generation of robotic assistants have more freedom to move, and are able to autonomously make decisions and decide between alternatives. For people to adopt such robots they will have to be shown to be both safe and trustworthy. In this paper we focus on formal verification of a set of rules that have been developed to control the Care-O-bot, a robotic assistant located in a typical domestic environment. In particular, we apply model-checking, an automated and exhaustive algorithmic technique, to check whether formal temporal properties are satisfied on all the possible behaviours of the system. We prove a number of properties relating to robot behaviours, their priority and interruptibility, helping to support both safety and trustworthiness of robot behaviours.

• Dennis, L. A. and Fisher, M. Actions with Durations and Failures in BDI Languages. In Proc. 21st European Conference on Artificial Intelligence (ECAI). Frontiers in Artificial Intelligence and Applications, vol 263, pp995-996, 2014. [Abstract]

  BDI programming languages provide a well developed route to implementing intelligent agents. However, as such agents are increasingly being used in physical environments their treatment of external actions needs to be improved. In this paper we outline a mechanism for handling actions which have durations and failures.

• Webster, M., Dixon, C., Fisher, M., Salem, M., Saunders, J., Koay, K-L., and Dautenhahn, K. Formal Verification of an Autonomous Personal Robotic Assistant. In Formal Verification and Modeling in Human-Machine Systems: Papers from the AAAI Spring Symposium (FVHMS 2014). ISBN 978-1-57735-655-4.

• Dennis, L. A. and Fisher, M. Safe Autonomous Space Software. In Space Safety Magazine, February 2014. ISSN: 2214-0379.

• Fisher, M., van der Torre, L., Dastani, M., and Governatori, G. Guest editorial: Computational Logic in Multi-Agent Systems. Journal of Logic and Computation 24(6):1251-1252 Springer, 2014.

• Konur, S., Fisher, M., Dobson, S., and Knox, S. Formal Verification of a Pervasive Messaging System. Formal Aspects of Computing 26(4):677-694, 2014. [Abstract]

  As ubiquitous computing becomes a reality, its applications are increasingly being used in business-critical, mission-critical and even in safety-critical, areas. Such systems must demonstrate an assured level of correctness. One approach to the exhaustive analysis of the behaviour of systems is formal verification, whereby each important requirement is logically assessed against all possible system behaviours. While formal verification is often used in safety analysis, it has rarely been used in the analysis of deployed pervasive applications. Without such formality it is difficult to establish that the system will exhibit the correct behaviours in response to its inputs and environment. In this paper, we show how model-checking techniques can be applied to analyse the probabilistic behaviour of pervasive systems. As a case study we apply this technique to an existing pervasive message-forwarding system, Scatterbox. Scatterbox incorporates many typical characteristics of pervasive systems, such as dependence on sensor reliability and dependence on context. We assess the dynamic temporal behaviour of the system, including the analysis of probabilistic elements, allowing us to verify formal requirements even in the presence of uncertainty in sensors. We also draw some tentative conclusions concerning the use of formal verification for pervasive computing in general.

• Fisher, M. If you want to trust a robot, look at how it makes decisions. The Conversation, 10th March 2014.

• Dennis, L. A., Fisher, M., Aitken, J., Veres, S. M., Gao, Y., Shaukat, A., and Burroughes, G. Reconfigurable Autonomy. KI - Künstliche Intelligenz, 2014. [Abstract]

  This position paper describes ongoing work at the Universities of Liverpool, Sheffield and Surrey in the UK on developing hybrid agent architectures for controlling autonomous systems, and specifically for ensuring that agent-controlled dynamic reconfiguration is viable. The work outlined here forms part of the Reconfigurable Autonomy research project.

  Webster, M., Dixon, C., and Fisher, M. Safe and Trustworthy Autonomous Robotic Assistants. In Space Safety Magazine, Issue 9, Winter 2014. ISSN: 2214-0379.

• Dennis, L. A., Fisher, M., Slavkovik, M., and Webster, M. Ethical Choice in Unforeseen Circumstances. In Proc. 14th Annual Conference on Towards Autonomous Robotic Systems (TAROS) LNCS 8069, pp433-445. Springer, 2014. [Abstract]

  For autonomous systems to be allowed to share environments with people, their manufacturers need to guarantee that the system behaves within acceptable legal, but also ethical, limits. Formal verification has been used to test if a system behaves within specified legal limits. This paper proposes an ethical extension to a rational agent controlling an Unmanned Aircraft(UA). The resulting agent is able to distinguish among possible plans and execute the most ethical choice it has. We implement a prototype and verify that when an agent does behave unethically, it does so because no more-ethical possibility is available.

  Dixon, C. and Fisher, M. On and On the Temporal Way. In, Voronkov and Korovina (eds), HOWARD-60. A Festschrift on the Occasion of Howard Barringer's 60th Birthday, pp85-111. EasyChair, 2014.

• Webster, M., Cameron, N., Jump, M., Fisher, M. Generating Certification Evidence for Autonomous Unmanned Aircraft Using Model Checking and Simulation. Journal of Aerospace Information Systems 11(5):258-279, May 2014. [Abstract]

  The usage of unmanned aircraft for civil applications is expected to increase over the next decade, particularly for the so-called "dull, dirty and dangerous" missions, and unmanned aircraft will undoubtedly require some form of autonomy in order to ensure safe operations for all airspace users. However, in order to be used for civil applications, unmanned aircraft must gain regulatory approval in a process known as certification. This paper presents a proof-of-concept approach to the gathering of certification evidence for autonomous unmanned aircraft based on formal model checking and flight simulation. In particular, rational agent-based autonomous systems are examined. We give examples of twenty-three different properties, based on the Rules of the Air and notions of Airmanship, which can be used for the formal verification of rational agents for autonomous unmanned aircraft. Our model checking can be based on either (i) implicit models of the aircraft's physical environment specified in terms of the range of sensor inputs the autonomous system may receive, or (ii) more explicit physical models of the environment. Finally, we provide a description of how such formal verification can be used to refine the implementation of autonomous systems for unmanned aircraft.

2013

• Fisher, M., Dennis, L. A., and Webster, M. Verifying Autonomous Systems. Communications of the ACM 56(9):84-93, 2013. [Abstract]

  In this article we consider the question: How should autonomous systems be analyzed? In particular, we describe how the confluence of developments in two areas --- autonomous systems architectures and formal verification for rational agents --- can provide the basis for the formal verification of autonomous systems behaviors.

• Konur, S., Fisher, M., and Schewe, S. Combined Model Checking for Temporal, Probabilistic, and Real-time Logics. Theoretical Computer Science 503:61-88, 2013. [Abstract]

  Model checking is a well-established technique for the formal verification of concurrent and distributed systems. In recent years, model checking has been extended and adapted for multi-agent systems, primarily to enable the formal analysis of belief-desire-intention systems. While this has been successful, there is a need for more complex logical frameworks in order to verify realistic multi-agent systems. In particular, probabilistic and real-time aspects, as well as knowledge, belief, goals, etc., are required. However, the development of new model checking tools for complex combinations of logics is both difficult and time consuming. In this article, we show how model checkers for the constituent temporal, probabilistic, and real-time logics can be re-used in a modular way when we consider combined logics involving different dimensions. This avoids the re-implementation of model checking procedures. We define a modular approach, prove its correctness, establish its complexity, and show how it can be used to describe existing combined approaches and define yet-unimplemented combinations. We also demonstrate the feasibility of our approach on a case study.

• Dennis, L. A., Fisher, M., and Webster, M. Using Agent JPF to Build Models for Other Model Checkers. In Proc. International Workshop on Computational Logic in Multi-Agent Systems (CLIMA). Lecture Notes in Computer Science 8143, pages 273-289. Springer, 2013. [Abstract]

  We describe an extension to the AJPF agent program model-checker so that it may be used to generate models for input into other, non-agent, model-checkers. We motivate this adaptation, arguing that it improves the efficiency of the model-checking process and provides access to richer property specification languages. We illustrate the approach by describing the export of AJPF program models to Spin and Prism. In the case of Spin we also investigate, experimentally, the effect the process has on the overall efficiency of model-checking.

• Dennis, L. A., Fisher, M., Lincoln, N., Lisitsa, A., and Veres, S. M. Practical Verification of Decision-Making in Agent-Based Autonomous Systems. arXiv:1310.2431, 2013. [Abstract]

  We present a verification methodology for analysing the decision-making component in agent-based hybrid systems. Traditionally hybrid automata have been used to both implement and verify such systems, but hybrid automata based modelling, programming and verification techniques scale poorly as the complexity of discrete decision-making increases making them unattractive in situations where complex logical reasoning is required. In the programming of complex systems it has, therefore, become common to separate out logical decision-making into a separate, discrete, component. However, verification techniques have failed to keep pace with this development. We are exploring agent-based logical components and have developed a model checking technique for such components which can then be composed with a separate analysis of the continuous part of the hybrid system. Among other things this allows program model checkers to be used to verify the actual implementation of the decision-making in hybrid autonomous systems.

• van Riemsdijk, M. Birna, Dennis, L. A., Fisher, M., and Hindriks, K. V. Agent Reasoning for Norm Compliance: a Semantic Approach. Proc. 13th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS), pp499-506, 2013. [Abstract]

  A system of autonomous agents may exhibit undesirable or ineffective behavior if no form of regulation is imposed. Norms, describing how agents should ideally behave, can be used to address this issue if agents are able to reason about norms and adapt their behavior to comply with them (if they choose to do so). Assuming that which norms will have to be followed is unknown at design time, it is not possible to pre-program agents such that their behavior is norm compliant. Instead, we need a generic execution mechanism that allows agents to adapt their behavior at run-time, which is what we propose in this paper. The execution mechanism is defined on top of an abstract agent decision making mechanism. This is done by allowing the execution of actions by the agent decision making mechanism only if these are not forbidden according to norms, as well as triggering the execution of actions if this is required by norms. We specify norms using Linear Temporal Logic and define the operational semantics of the execution mechanism using techniques from executable temporal logic. We formally analyze properties of the execution mechanism, including norm compliance.

• Dixon, C., Konev, B., Fisher, M., and Nietiadi, S. Deductive Temporal Reasoning with Constraints. Journal of Applied Logic 11(1):30-51, 2013. [Abstract]

  When modelling realistic systems, physical constraints on the resources available are often required. For example, we might say that at most N processes can access a particular resource at any moment, exactly M participants are needed for an agreement, or an agent can be in exactly one mode at any moment. Such situations are concisely modelled where literals are constrained such that at most N, or exactly M, can hold at any moment in time. In this paper we consider a logic which is a combination of standard propositional linear time temporal logic with cardinality constraints restricting the numbers of literals that can be satisfied at any moment in time. We present the logic and show how to represent a number of case studies using this logic. We propose a tableau-like algorithm for checking the satisfiability of formulae in this logic, provide details of a prototype implementation and present experimental results using the prover.

• Lincoln, N., Veres, S. M., Dennis, L. A., Fisher, M., and Lisitsa, A. Autonomous Asteroid Exploration by Rational Agents. IEEE Computational Intelligence 8(4):25-38, 2013. [Abstract]

  The history of software agent architectures has been driven by the parallel requirements of real-time decision-making and the sophistication of the capabilities the agent can provide. Starting from reactive, rule based, subsumption through to layered and belief-desire-intention architectures, a compromise always has to be reached between the ability to respond to the environment in a timely manner and the provision of capabilities that cope with relatively complex environments. In the spirit of these past developments, this paper is proposing a novel "anthropomorphic" agent architecture that brings together the most desirable features: natural language definitions of agent reasoning and skill descriptions, shared knowledge with operators, the combination of fast reactive as well as long term planning, ability to explain why certain actions are taken by the autonomous agent and finally inherent formal verifiability. With these attributes, the proposed agent architecture can potentially cope with the most demanding autonomous space missions.

2012

• Stocker, R., Dennis, L. A., Dixon, C., and Fisher, M. Verification of Brahms Human-Robot Teamwork Models. In Proc. 13th European Conference on Logics in Artificial Intelligence (JELIA-2012). LNCS 7519, pp385-397. Springer, 2012. [Abstract]

  Collaboration between robots and humans is an increasingly important aspect of industrial and scientific settings. In addition, significant effort is being put into the development of robot helpers for more general use in the workplace, at home, and in health-care environments. However, before such robots can be fully utilised, a comprehensive analysis of their safety is necessary. Formal verification techniques are regularly used to exhaustively assess system behaviour. Our aim is to apply such techniques to Brahms, a human-agent-robot modelling language. We show how to translate from Brahms scenarios, using a formal semantics for Brahms, into the input language of a model checker.We illustrate the approach by defining, translating, and verifying a domestic robot helper example.

• Niknafs-Kermani, A., Konev, B., and Fisher, M. Symmetric Temporal Theorem Proving. In Proc. 19th International Symposium on Temporal Representation and Reasoning (TIME-2012) pp21-28, IEEE Computer Society Press, 2012. [Abstract]

  In this paper we consider the deductive verification of propositional temporal logic specifications of symmetric systems. In particular, we provide a heuristic approach to the scalability problems associated with analysing properties of large numbers of processes. Essentially, we use a temporal resolution procedure to verify properties of a system with few processes and then generalise the outcome in order to reduce the verification complexity of the same system with much larger numbers of processes. This provides a practical route to deductive verification for many systems comprising identical processes.

• Dixon, C., Fisher, M., Winfield, A. F. T., and Zeng, C. Towards Temporal Verification of Swarm Robotic Systems. Robotics and Autonomous Systems 60(11):1429-1441, 2012. [Abstract]

  A robot swarm is a collection of simple robots designed to work together to carry out some task. Such swarms rely on: the simplicity of the individual robots; the fault tolerance inherent in having a large population of identical robots; and the self-organised behaviour of the swarm as a whole. Although robot swarms present an attractive solution to demanding real-world applications, designing individual control algorithms that can guarantee the required global behaviour is a difficult problem. In this paper we assess and apply the use of formal verification techniques for analysing the emergent behaviours of robotic swarms. These techniques, based on the automated analysis of systems using temporal logics, allow us to analyse whether all possible behaviours within the robot swarm conform to some required specification. In particular, we apply model-checking, an automated and exhaustive algorithmic technique, to check whether temporal properties are satisfied on all the possible behaviours of the system. We target a particular swarm control algorithm that has been tested in real robotic swarms, and show how automated temporal analysis can help to refine and analyse such an algorithm.

• Dennis, L. A., Fisher, M., Webster, M., and Bordini, R. H. Model Checking Agent Programming Languages. Journal of Automated Software Engineering 19(1):5-63, 2012. [Abstract]

  In this paper we describe a verification system for multi-agent programs. This is the first comprehensive approach to the verification of programs developed using programming languages based on the BDI (belief-desire-intention) model of agency. In particular, we have developed a specific layer of abstraction, sitting between the underlying verification system and the agent programming language, that maps the semantics of agent programs into the relevant model-checking framework. Crucially, this abstraction layer is both flexible and extensible; not only can a variety of different agent programming languages be implemented and verified, but even heterogeneous multi-agent programs can be captured semantically. In addition to describing this layer, and the semantic mapping inherent within it, we describe how the underlying model-checker is driven and how agent properties are checked. We also present several examples showing how the system can be used. As this is the first system of its kind, it is relatively slow (although recent work shows that its performance is comparable to a similar system implemented in Maude), so we also indicate further work that needs to be tackled to improve performance.

• Konur, S., Dixon, C., and Fisher, M. Analysing Robot Swarm Behaviour via Probabilistic Model Checking. Robotics and Autonomous Systems 60(2):199-213, 2012. [Abstract]

  An alternative to deploying a single robot of high complexity can be to utilize robot swarms comprising large numbers of identical, and much simpler, robots. Such swarms have been shown to be adaptable, fault-tolerant and widely applicable. However, designing individual robot algorithms to ensure effective and correct overall swarm behaviour is actually very difficult. While mechanisms for assessing the effectiveness of any swarm algorithm before deployment are essential, such mechanisms have traditionally involved either computational simulations of swarm behaviour, or experiments with robot swarms themselves. However, such simulations or experiments cannot, by their nature, analyse all possible swarm behaviours. In this paper, we will develop and apply the use of automated probabilistic formal verification techniques to robot swarms, involving an exhaustive mathematical analysis, in order to assess whether swarms will indeed behave as required. In particular we consider a foraging robot scenario to which we apply probabilistic model checking.

2011

• Dix, J. and Fisher, M. Where Logic and Agents Meet. Annals of Mathematics and Artificial Intelligence 61(1):15-28. Springer, 2011. [Abstract]

  In this paper we provide a short, and very subjective, description of how mathematical techniques, primarily those from logical foundations, have been used in multi-agent systems. This is certainly not a comprehensive survey, but gives some indication of where the fields of "Logic" and "Agents" have met in recent years. The Annals of Mathematics and Artificial Intelligence contain a surprising number of articles in this area, among them several special issues focusing on computational logic and its use in agent systems.

• Webster, M., Fisher, M., Cameron, N., and Jump, M. Formal Methods and the Certification of Autonomous Unmanned Aircraft Systems. In Proc. 30th International Conference on Computer Safety, Reliability and Security (SAFECOMP). Lecture Notes in Computer Science 6894, pages 228-242. Springer, 2011. [Abstract]

  In this paper we assess the feasibility of using formal methods, and model checking in particular, for the certification of Unmanned Aircraft Systems (UAS) within civil airspace. We begin by modelling a basic UAS control system in PROMELA, and verify it against a selected subset of the CAA's Rules of the Air using the SPIN model checker. Next we build a more advanced UAS control system using the autonomous agent language Gwendolen, and verify it against the small subset of the Rules of the Air using the agent model checker AJPF. We introduce more advanced autonomy into the UAS agent and show that this too can be verified. Finally we compare and contrast the various approaches, discuss the paths towards full certification, and present directions for future research.

• Stocker, R., Sierhuis, M., Dennis, L. A., Dixon, C., and Fisher, M. A Formal Semantics for Brahms. In Proc. 12th International Workshop on Computational Logic in Multi-Agent Systems (CLIMA). Lecture Notes in Computer Science 6814, pages 259-274. Springer, 2011. An extended version is available as a technical report. [Abstract]

  The formal analysis of computational processes is by now a well established field. However, in practical scenarios, the problem of how we can formally verify interactions with humans still remains. In this paper we are concerned with addressing this problem. Our overall goal is to provide formal verification techniques for human-agent teamwork, particularly astronaut-robot teamwork on future space missions and human-robot interactions in health-care scenarios. However, in order to carry out our formal verification, we must first have some formal basis for this activity. In this paper we provide this by detailing a formal operational semantics for Brahms, a modelling/simulation framework for human-agent teamwork that has been developed and extensively used within NASA. This provides a first, but important, step towards our overall goal by establishing a formal basis for describing human-agent teamwork, which can then lead on to verification techniques.

• Konur, S. and Fisher, M. Formal Analysis of a VANET Congestion Control Protocol through Probabilistic Verification. In Proc. 73rd IEEE Vehicular Technology Conference (VTC2011-Spring), pp1-5. IEEE Press, 2011. [Abstract]

  Vehicular ad hoc networks (VANETs), which are a class of Mobile ad hoc networks, have recently been developed as a standard means of communication among moving vehicles. Since VANETs are vital to the safety of the vehicles, the infrastructure, and the humans involved, a deep analysis of their potential behaviours is clearly required. In this paper we provide this analysis through the use of formal verification. Specifically, we formally analyse a specific congestion control protocol for VANETs using a probabilistic model checking technique, and investigate its correctness and effectiveness.

• Cameron, N., Webster, M., Jump, M., and Fisher, M. Certification of Civil UAS as a Virtual Engineering Approach. To appear in Proc. American Institute of Aeronautics and Astronautincs Modelling and Simulation Technologies Conference (AIAA-MST), August 2011.

• Fisher, M. Agent Deliberation in an Executable Temporal Framework. Journal of Applied Logic 9(4):223-238. Elsevier, December 2011. [Abstract]

  Autonomous agents are not so difficult to construct. Constructing autonomous agents that will work as required is much harder. A clear way in which we can design and analyze autonomous systems so that we can be more confident that their behaviour is as required is to use formal methods. These can, in principle, allow us to exactly specify the behaviour of the agent, and verify that any implementation has the properties required. In addition to using a more formal approach, it is clear that problems of conceptualization and analysis can be aided by the use of an appropriate abstraction. In this article we tackle one particular aspect of formal methods for agent-based systems, namely the formal representation and implementation of deliberation within agents. The key aspect here is simplicity. Agents are specified using a relatively simple temporal logic and are executed by directly interpreting such temporal formulae. Deliberation is captured by modifying the way in which execution handles its temporal goals. Thus, in this article we provide motivations, theoretical underpinnings, implementation details, correctness arguments, and comparisons with related work.

2010

• Lincoln, N., and Veres, S. M., Dennis, L. A., Fisher, M., and Lisitsa, A. An Agent Based Framework for Adaptive Control and Decision Making of Autonomous Vehicles. To appear in Proc. IFAC Workshop on Adaptation and Learning in Control and Signal Processing (ALCOSP), 2010. [Abstract]

  The paper addresses the problem of defining a theoretical physical agent framework that combines rational agent decision making with abstractions from predictions and planning of the future of the physical environment. The objective of the new framework is to reduce complexity of logical inference of agents controlling autonomous vehicles and robots in space exploration, deep underwater exploration, defense reconnaissance, automated manufacturing and household automation. An essential feature of the framework is automated realtime evaluations of abstractions on the effects of future actions. Comparison is made with hybrid automaton based solutions in terms of computational complexity.

• Bujorianu, M. and Fisher, M. (Eds). Proc. FM-09 Workshop on Formal Methods for Aerospace (FMA). Electronic Proceedings in Theoretical Computer Science 20. March 2010.

• Bordini, R. H., Dennis, L. A., Farwer, B., and Fisher, M. Directions for Agent Model Checking. In Dastani, M., Hindriks, K., and Meyer, J-J. (eds) Specification and Verification of Multi-agent Systems pp103-123. Springer, 2010.

• Dennis, L. A., Fisher, M., Lisitsa, A., Lincoln, N., and Veres, S. M. Satellite Control Using Rational Agent Programming. IEEE Intelligent Systems 25(3):92-97, May/June, 2010.

• Konur, S., Dixon, C., and Fisher, M. Formal Verification of Probabilistic Swarm Behaviours. In Proc. 7th International Conference on Swarm Intelligence (ANTS). Lecture Notes in Computer Science 6234, pages 440-447. Springer, 2010. [Abstract]

  Robot swarms provide a way for a number of simple robots to work together to carry out a task. While swarms have been found to be adaptable, fault-tolerant and widely applicable, designing individual robot algorithms so as to ensure effective and correct swarm behaviour is very difficult. In order to assess swarm effectiveness, either experiments with real robots or computational simulations of the swarm are usually carried out. However, neither of these involve a deep analysis of all possible behaviours. In this paper we will utilise automated formal verification techniques, involving an exhaustive mathematical analysis, in order to assess whether our swarms will indeed behave as required.

• Dennis, L. A., Fisher, M., Lincoln, N., Lisitsa, A., and Veres, S. M.. Declarative Abstractions for Agent Based Hybrid Control Systems. In Proc. 8th International Workshop on Declarative Agent Languages and Technologies (DALT). Lecture Notes in Computer Science 6619, pages 96-111. Springer, 2010

• Fisher, M. and Ghidini, C. Executable Specifications of Resource-Bounded Agents. Journal of Autonomous Agents and Multi-Agent Systems 21(3):368-396, 2010. [Abstract]

  Logical theories of intelligent (or rational) agents have been refined and improved over the past 20 years of research. Such logical theories are used in many ways, one of which is as the basis for executable agent specifications. Here, agents are specified using a logical description and then this description is directly executed in order to implement the agent's behaviour. This provides strong correctness results for the implemented agent, directly corresponding the formal specification with the implementation.
  
  With increased application, it has become clear that such specifications of idealised agents are inappropriate in practical situations. An agent may have many resource-bounds to contend with, both in terms of time and memory, and this should be taken into account within the agent's formal specification. Thus, in this paper, we tackle the problem of representing and executing resource-bounded agents. The framework developed here allows the restriction of the amount of reasoning, both temporal and doxastic, that the agent is permitted. We address the formal properties of the framework, present results concerning the execution of such specifications, and consider the practical outcome of such restrictions.

• Dennis, L. A., Fisher, M., Lincoln, N., Lisitsa, A., and Veres, S. M.. Reducing Code Complexity in Hybrid Control Systems. In Proc. 10th International Symposium on Artificial Intelligence, Robotics and Automation in Space (i-Sairas). 2010 [Abstract]

  Modern control systems are limited in their ability to react flexibly and autonomously to changing situations by the complexity inherent in handling situations where many variables are present.
  
  We present an architecture based on a combination of agent programming and hybrid systems for managing high level decisions in such systems. Our preliminary case study concerns satellites maintaining geo-stationary orbits. This case study suggests that the complexity of the code of such a system increases much more slowly in the face of increasing complexity of the scenario, than in a more traditional approach based on finite state machines over controller options.

2009

• Bordini, R. H., Fisher, M., Wooldridge, M., and Visser, W. Property-based Slicing for Agent Verification. Journal of Logic and Computation 19(6):1385-1425. December 2009.

• Arapinis, M., Calder, M., Dennis, L. A., Fisher, M., Gray, P., Konur, S., Miller, A., Ritter, E., Ryan, M., Schewe, S., Unsworth, C., and Yasmin, R. Towards the Verification of Pervasive Systems. In Proc. FM-2009 Workshop on Formal Methods for Interactive Systems (FMIS). Electronic Communications of the EASST, Volume 22.

• Behdenna, A., Dixon, C., and Fisher, M. Deductive Verification of Simple Foraging Robotic Behaviours. International Journal of Intelligent Computing and Cybernetics 2(4):604-643. Emerald Publishing, December 2009.

• Ballarini, P., Fisher, M. and Wooldridge, M. Uncertain Agent Verification through Probabilistic Model-Checking. In Safety and Security in Multiagent Systems. Lecture Notes in Computer Science 5454, pages 162-174. Springer, September 2009.

• Dixon, C., Fisher, M., and Konev, B. Taming the Complexity of Temporal Epistemic Reasoning. In Proc. 7th International Symposium on Frontiers of Combining Systems (FroCoS). Lecture Notes in Computer Science 5749, pp198-213. Springer, September 2009.

• Fisher, M., Sadri, F., and Thielscher, M. (Eds). Computational Logic in Multi-Agent Systems. Lecture Notes in Artificial Intelligence 5405. Springer, August 2009.

• Fisher, M. and Hepple, A. Executing Logical Agent Specifications. In, Rafael H. Bordini, Mehdi Dastani, Jürgen Dix, and Amal El Fallah-Seghrouchni (eds), Multi-Agent Programming: Languages, Tools and Applications, pp1-27. Springer, June 2009.

• Bordini, R. H., Fisher, M., and Sierhuis, M. Formal Verification of Human-Robot Teamwork. In Proc. 4th ACM/IEEE International Conference on Human-Robot Interaction, pp 267-268. ACM Press, March 2009.

• Fisher, M., Konev, B., and Lisitsa, A. Temporal Verification of Fault-Tolerant Protocols. In Methods, Models and Tools for Fault Tolerance. Lecture Notes in Computer Science 5454, pages 44-56. Springer, March 2009.

• Webster, M., Dennis, L. A., and Fisher, M. Model-Checking Auctions, Coalitions and Trust. Technical Report number ULCS-09-004. Department of Computer Science, University of Liverpool, February 2009.

• Fisher, M. and Ghidini, C. Exploring the Future with Resource-Bounded Agents. Journal of Logic, Language and Information 18(1):3-21. Springer, January 2009.

• Fisher, M., Dennis, L. A., and Hepple, A. Modular Multi-Agent Design. Technical Report number ULCS-09-002. Department of Computer Science, University of Liverpool, January 2009.

2008

• Bordini, R. H., Dennis, L. A., Farwer, B., and Fisher, M. Automated Verification of Multi-Agent Programs. In Proc. 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE) pp69-78. IEEE, 2008.

• Hepple, A., Dennis, L. A., and Fisher, M. A Common Basis for Agent Organisations in BDI Languages. In Proc. 1st International Workshop on LAnguages, methodologies and Development tools for multi-agent systemS (LADS). Lecture Notes in Artificial Intelligence 5118, pages 171-88, Springer, 2008.

• de Carvahlo Ferreira, N., Fisher, M., and van der Hoek, W. Specifying and Reasoning about Uncertain Agents. International Journal of Approximate Reasoning 49(1):35-51. September 2008, Elsevier.

• Dennis, L. A., Farwer, B., Bordini, R. H., and Fisher, M. A Flexible Framework for Verifying Agent Programs. In Proc. 7th International Conference on Autonomous Agents and Multiagent Systems (AAMAS), pp 1303-1306, 2008.

• Dennis, L. A., Hepple, A., and Fisher, M. Language Constructs for Multi-Agent Programming. In Proc. 8th International Workshop on Computational Logic in Multi-Agent Systems (CLIMA). Lecture Notes in Artificial Intelligence 5056, pp137-156. Springer, 2008.

• Dixon, C., Fisher, M., Konev, B., and Lisitsa, A. Practical First-Order Temporal Reasoning. In Proc. International Symposium on Temporal Representation and Reasoning (TIME), pp 156-163. IEEE Computer Society, 2008.

• Dennis, L. A., and Fisher, M. Programming Verifiable Heterogeneous Agent Systems. In Proc. Sixth International Workshop on Programming in Multi-Agent Systems (ProMAS). Lecture Notes in Artificial Intelligence 5442, pp40-55. Springer, 2008.

• Dennis, L. A., Farwer, B., Bordini, R. H., Fisher, M., and Wooldridge, M. A Common Semantic Basis for BDI Languages. In Proc. 5th International Workshop on Programming Multi-Agent Systems (ProMAS), Lecture Notes in Computer Science 4908, pages 124-139. Springer-Verlag, 2008.

2007

• Dixon, C., Fisher, M., and Konev, B. Temporal Logic with Capacity Contraints In Proc. 6th International Symposium on Frontiers of Combining Systems (FroCoS). Lecture Notes in Computer Science 4720, pages 163-177, Springer, 2007.

• Fisher, M.and van der Hoek, W. Guest editorial: Logics in AI -- post-proceedings JELIA06. Annals of Mathematics in Artificial Intelligence 50(3-4): 227-229. Springer, August 2007.

• Dixon, C., Fernández Gago, M-C., Fisher, M., and van der Hoek, W. Temporal Logics of Knowledge and their Applications in Security. Electronic Notes in Theoretical Computer Science 186:27-42. Elsevier, 2007.

• Fisher, M., Singh, M. P., Spears, D., and Wooldridge, M. Guest editorial: Logic-Based Agent Verification. Journal of Applied Logic 5(2):193-195. Elsevier, June 2007.

• Fisher, M., Bordini, R. H., Hirsch, B., and Torroni, P. Computational Logics and Agents: A Roadmap of Current Technologies and Future Trends. Computational Intelligence 23(1):61-91. Blackwell Publishing, February 2007.

• Dixon, C., Fisher, M., and Konev, B. Tractable Temporal Reasoning In Proc. International Joint Conference on Artificial Intelligence (IJCAI), pages 318-323. AAAI Press, 2007.

2006

• Fisher, M., van der Hoek, W., Konev, B., and Lisitsa, A. (eds) Proc. Tenth European Conference on Logics in Artificial Intelligence (JELIA), Lecture Notes in Computer Science 4160, Springer-Verlag, 2006. ISBN 0302-9743.

• Bouzid, M., Combi, C., Fisher, M., and Ligozat, G. Guest editorial: Temporal Representation and Reasoning. Annals of Mathematics in Artificial Intelligence 46(3):231-234. Springer, March 2006.

• Fisher, M. Implementing Temporal Logics: Tools for Execution and Proof. In Proc. 6th International Workshop on Computational Logic in Multi-Agent Systems (CLIMA). Lecture Notes in Artificial Intelligence 3900, pages 129-142. Springer-Verlag, 2006.

• Wooldridge, M., Fisher, M., Huget, M.-P. and Parsons, S. Model Checking for Multiagent Systems: The MABLE Language and its Applications. International Journal of Artificial Intelligence Tools 15(2):195-225. World Scientific, April 2006.

• Dixon, C., Fisher, M., and Konev, B. Is There a Future for Deductive Temporal Verification? In Proc. International Symposium on Temporal Representation and Reasoning (TIME), pages 11-18. IEEE CS Press, 2006. An extended version is available as University of Liverpool Technical Report number ULMS-06-01.

• Bordini, R. H., Fisher, M., Visser, W., and Wooldridge, M. Verifying Multi-Agent Programs by Model Checking. Journal of Autonomous Agents and Multi-Agent Systems 12(2):239-256. Springer, March 2006.

• Degtyarev, A., Fisher, M., and Konev, B. Monodic Temporal Resolution. ACM Transactions on Computational Logic 7(1):108-150. ACM, January 2006.

• Ballarini, P., Fisher, M., and Wooldridge, M. Automated Game Analysis via Probabilistic Model Checking: a case study.Electronic Notes in Theoretical Computer Science 149(2):125-137. Elsevier, February 2006.

• Hustadt, U., Dixon, C., Schmidt, R., Fisher, M., Meyer, J-J., and van der Hoek, W. Verification Within the KARO Agent Theory. In Agent Technology from a Formal Perspective. Springer-Verlag, 2006.

• Fisher, M., Ghidini, C. and Kakoudakis, T. Dynamic Team Formation in Executable Agent-Based Systems. Agent Technology from a Formal Perspective. Springer-Verlag, 2006.

2005

• de Carvahlo Ferreira, N., Fisher, M., and van der Hoek, W. A Logical Implementation of Uncertain Agents. In Proceedings of Twelfth Portuguese Conference on Artificial Intelligence (EPIA), Covilha, Portugal, December 2005. Lecture Notes in Artificial Intelligence 3808, Springer-Verlag, pages 536-547.

• Fisher, M. Temporal Development Methods for Agent-Based Systems. Journal of Autonomous Agents and Multi-Agent Systems 10(1):41-66, January 2005.

• Dixon, C., Fisher, M., and Bolotov, A. Alternating Automata and Temporal Logic Normal Forms. Annals of Pure and Applied Logic 135(1-3): 263-285. Elsevier Science, 2005.

• Winfield, A. F. T., Sa, J., Fernández Gago, M-C., Dixon, C., and Fisher, M. On Formal Specification of Emergent Behaviours in Swarm Robotic Systems. International Journal of Advanced Robotic Systems 2(4):363-370, December 2005.

• Fisher, M. METATEM: The Story so Far. In Proceedings of the Third International Workshop on Programming Multiagent Systems (ProMAS-03), Utrecht, Netherlands. Lecture Notes in Artificial Intelligence 3862, pages 3-22, Springer Verlag, 2005.

• Ballarini, P., Fisher, M., and Wooldridge, M. Probabilistic Model-Checking for Games of Imperfect information. In Online Proceedings of the Process Algebras and Stochastically Timed Activities (PASTA), Septmber 2005.

• Nalon, C., Dixon, C., and Fisher, M. Resolution for Synchrony and No Learning. To appear in Proceedings of AiML-5, Kings College Publications, 2005.

• Fisher, M. Agents out of control? Towards the formal verification of autonomous agent teams. In Proc. IEE Seminar on Autonomous Agents in Control, pp75-83, 2005.

• Hirsch, B., Fisher, M., Ghidini, C., and P. Busetta. Organising Software in Active Environments. In Computational Logic in Multi-Agent Systems (CLIMA-V). Lecture Notes in Computer Science 3487, Springer-Verlag, 2005.

• Fisher, M., Lisitsa, A., and Konev, B. Practical Infinite-state Verification with Temporal Reasoning. In, Clarke, E., Minea, M., and Tiplea, F. (eds) Verification of Infinite-State Systems with Applications to Security. Volume 1 of the NATO Security through Science Series: Information and Communication Security. IOS Press, January 2006. (Proceedings of the NATO Advance Reasearch Workshop on Verification of Infinite-State Systems with Applications to Security (VISSAS), 2005.)

• Konev, B., Degtyarev, A., Dixon, C., Fisher, M., and Hustadt, U. Mechanizing First-Order Temporal Resolution. Information and Computation 199(1-2):55-86. Elsevier Science, 2005.

• Fisher, M., Gabbay, D., and Vila, L. (editors) Handbook of Temporal Reasoning in Artificial Intelligence, Elsevier Science, 2005.

• Winfield, A. F. T., Sa, J., Fernández Gago, M-C., Dixon, C., and Fisher, M. Using Temporal Logic to Specify Emergent Behaviours in Swarm Robotic Systems. In Proceedings of Towards Autonomous Robotic Systems (TAROS), 2005.

• Fernández Gago, M-C., Hustadt, U., Dixon, C., Fisher, M., and Konev, B. First-Order Temporal Verification in Practice. Journal of Automated Reasoning 34(3):295-321, April 2005.

2004

• Fisher, M., Ghidini, C., and Hirsch, B. Programming Groups of Rational Agents. In Computational Logic in Multi-Agent Systems (CLIMA-IV). Lecture Notes in Computer Science 3259, Springer-Verlag, November 2004.

• Bordini, R. H., Fisher, M., Visser, W., and Wooldridge, M. Model Checking Rational Agents. IEEE Intelligent Systems 19(5):46-52, September/October 2004.

• de Carvahlo Ferreira, N., Fisher, M., and van der Hoek, W.. Practical Reasoning for Uncertain Agents. In Proceedings of Ninth European Conference on Logics in Artificial Intelligence (JELIA), Lisbon, Portugal, September 2004. Lecture Notes in Artificial Intelligence 3229, Springer-Verlag, pages 82-94.

• Dixon, C., Nalon, C., and Fisher, M.. Tableau for Logics of Time and Knowledge with Interactions Relating to Synchrony. Journal of Applied Non-Classical Logics 14(4): 397-446, 2004.

• Fisher, M., Ghidini, C., and Hirsch, B. Organising Computation through Dynamic Grouping. In Objects, Agents and Features. Lecture Notes in Computer Science 2975, pages 117-136, Springer Verlag 2004.

• Fisher, M. Multi-Agent programming Based on Distributed Deduction. In Zhang, W., and Sorge, V. (eds) Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems, volume 112 of Frontiers in Artificial Intelligence and Applications. IOS Press, November 2004.

• Dixon, C., Fernández Gago, M-C., Fisher, M., and van der Hoek, W.. Using Temporal Logics of Knowledge in the Formal Verification of Security Protocols. In Proceedings of TIME 2004, 1st-3rd July 2004, Tatihou, Normandie, France. IEEE.

• Dix, J., Fisher, M., Levesque, H., and Sterling, L. Special Issue on Logic-Based Agent Implementation -- Editorial. Annals of Mathematics and Artificial Intelligence 41 (2-4): 131-133, August 2004. Kluwer Academic Publishers

• Bordini, R. H., Fisher, M., Visser, W., and Wooldridge, M.. State-Space Reduction Techniques in Agent Verification. In Proceedings of the Third International Joint Conference on Autonomous Agents and Multi-Agent Systems (AAMAS-2004), New York, USA.

• Fisher, M., and Lisitsa, A. Monodic ASMs and Temporal Verification. In Proc. International Workshop on Abstract State Machines (ASM 2004). Volume 3065 of Lecture Notes in Computer Science. Springer-Verlag, 2004. (Version also available as Technical Report ULCS-03-011 from Department of Computer Science at the University of Liverpool.)

• Artale, A., Dixon, C., Fisher, M. and Franconi, E. Special Issue on Temporal Representation and Reasoning -- Editorial. Journal of Logic and Computation 14(1):1-2, February 2004.

2003

• Dixon, C., Nalon, C., and Fisher, M. Tableaux for Temporal Logics of Knowledge: Synchronous Systems of Perfect Recall or No Learning. In Proceedings of TIME-ICTL 2003, July 2003, Cairns, Queensland, Australia. IEEE CS Press. (Preliminary version)

• Konev, B., Degtyarev, A., Dixon, C., Fisher, M., and Hustadt, U. Towards the Implementation of First-Order Temporal Resolution: the Expanding Domain Case. In Proceedings of TIME-ICTL 2003, July 2003, Cairns, Queensland, Australia. IEEE CS Press. (Preliminary version)

• Bordini, R. H., Visser, W., Fisher, M., Pardavila, C., and Wooldridge, M. Model Checking Multi-Agent Programs with CASP. In Proceedings of the Fifteenth Conference on Computer-Aided Verification (CAV-2003). Tool description. Springer-Verlag, to appear. (Preliminary version)

• Bordini, R. H., Fisher, M., Pardavila, C., and Wooldridge, M. Model Checking AgentSpeak. In Proceedings of the Second International Joint Conference on Autonomous Agents and Multi-Agent Systems (AAMAS-2003), Melbourne, Australia, July 2003. (Preliminary version)

• Degtyarev, A., Fisher, M., and Konev, B.. Monodic Temporal Resolution. In Proceedings of CADE-03, July 2003, Miami. Springer-Verlag, to appear.

• Bordini, R. H., Visser, W., Fisher, M., and Wooldridge, M. Verifiable multi-agent programs. In Proceedings of the First International Workshop on Programming Multiagent Systems: languages, frameworks, techniques and tools (ProMAS-03), held with AAMAS-03, 15 July, 2003, Melbourne, Australia. Volume 3067 of Lecture Notes in Artificial Intelligence, Springer Verlag. (Pre-proceedings version)

• Bordini, R. H., Visser, W., Fisher, M., Pardavila, C., and Wooldridge, M. Model Checking Multi-Agent Programs with CASP. In Pre-proceedings of Third Workshop on Automated Verification of Critical Systems (AVoCS 2003). (Preliminary version)

• Degtyarev, A., Fisher, M., and Konev, B. Handling Equality in Monodic Temporal Resolution. In Proc. 10th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), pp 214-228, Lecture Notes in Computer Science, 2850. Springer-Verlag, 2003.

2002

• Hirsch, B., Fisher, M., and Ghidini, C. Organising Logic-Based Agents. In Proc. Second NASA/IEEE Goddard Workshop on Formal Approaches to Agent-Based Systems (FAABS-II), pp 15-27, Lecture Notes in Computer Science 2699. Springer-Verlag, 2002.

• Artale, A., and Fisher, M. (eds) Ninth International Symposium on Temporal Representation and Reasoning - TIME-02. IEEE Computer Society Press, 2002.

• d'Inverno, M., Luck, M., Fisher, M., and Preist, C. (eds) Foundations and Applications of Multi-Agent Systems: UKMAS Workshop 1996-2000, Selected Papers. Lecture Notes in Computer Science 2403, Springer-Verlag, 2002. ISBN 3-540-43962-5

• Bennett, B., Dixon, C., Fisher, M., Hustadt, U., Franconi, E., Horrocks, I., and de Rijke, M. Combinations of Modal Logics. Artificial Intelligence Review 17(1):1-20. Kluwer Academic Publishers, March 2002. (Preliminary version)

• Fisher, M., and Visser, W. Verification of Autonomous Spacecraft Control -- A logical vision of the future. In Workshop on AI Planning and Scheduling for Autonomy in Space Applications - AIPS-ASA, Manchester, July 2002.

• Dixon, C., Fisher, M., and Bolotov, A. Clausal Resolution in a Logic of Rational Agency. Artificial Intelligence 139(1):47-89. Elsevier Science, July 2002.

• Fisher, M., and Ghidini, C. Agents with Bounded Temporal Resources. In Foundations and Applications of Multi-Agent Systems. Volume 2403 of Lecture Notes in Computer Science, pp169-184. Springer-Verlag, July 2002. (Preliminary version)

• Bolotov, A., Fisher, M., and Dixon, C. On the Relationship Between Omega-Automata and Temporal Logic Normal Forms. Journal of Logic and Computation 12(4):561-581. Oxford University Press, August 2002. (Preliminary version)

• Degtyarev, A., Fisher, M., and Konev, B. A Simplified Clausal Resolution Procedure for Propositional Linear-Time Temporal Logic. In Proc. TABLEAUX-02. LNCS 2381, pp 85-99. Springer-Verlag, 2002. (Preliminary version)

• Brotherson, J., Degtyarev, A., Fisher, M., and Lisitsa, A. Searching for Invariants using Temporal Resolution. In Proc. LPAR-02. Lecture Notes in Computer Science, Springer-Verlag, 2002.

• Fernández Gago, M-C., Fisher, M., and Dixon, C. Algorithms for Guiding Clausal Temporal Resolution. In Proc. 25th German Conference on Artificial Intelligence (KI-2002). Lecture Notes in Artificial Intelligence, Springer-Verlag, 2002.

• Fisher, M., and Ghidini, C. The ABC of Rational Agent Programming. In Proc. First International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS), Bologna, Italy, July 2002.

• Wooldridge, M., Fisher, M., Huget, M.-P. and Parsons, S. Model Checking Multiagent systems with MABLE. In Proc. First International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS), Bologna, Italy, July 2002.

• Degtyarev, A., Fisher, M., and Lisitsa, A. Equality and Monodic First-Order Temporal Logic. Studia Logica 72(2):147-156, November 2002.

• Kellett, A. and Fisher, M. Coordinating Heterogeneous Components Using Executable Temporal Logic. In, Meyer, J.-J., and Treur, J. (eds), Agent-based Defeasible Control in Dynamic Environments. Vol. 7 in Series of Handbooks in Defeasible Reasoning and Uncertainty Management Systems. Kluwer Academic Publishers, 2002.

• Hustadt, U., Dixon, C., Schmidt, R., Fisher, M., Meyer, J-J., and van der Hoek, W. Verification Within the KARO Agent Theory. In Selected Papers from the First Goddard Workshop on Formal Approaches to Agent-Based Systems. Kluwer Academic Publishers, to appear. (Preliminary version)

• Fisher, M., and Ghidini, C.. Dynamic Team Formation in Executable Agent-Based Systems. In Selected Papers from the First Goddard Workshop on Formal Approaches to Agent-Based Systems. Kluwer Academic Publishers, to appear.

2001

• Fisher, M., Dixon, C., and Peim, M. Clausal Temporal Resolution. ACM Transactions on Computational Logic 2(1):12-56. January 2001.

• Degtyarev, A., and Fisher, M. Towards First-Order Temporal Resolution. In Proc. 24th German/Austrian Conference on Artificial Intelligence (KI-2001), Volume 2174 of Lecture Notes in Artificial Intelligence pp18-32, Springer Verlag, 2001.

• Hustadt, U., Dixon, C., Schmidt, R., Fisher, M., Meyer, J-J., and van der Hoek, W. Reasoning about agents in the KARO framework. In Proc. Eighth International Symposium on Temporal Representation and Reasoning (TIME-01), pp 206-213. IEEE Computer Society Press, 2001.

• Fernández Gago, M-C., Fisher, M., and Dixon, C. An Algorithm for Guiding Clausal Temporal Resolution. In Proc. 4th International Workshop on Strategies in Automated Deduction [STRATEGIES 2001], held in conjunction with IJCAR 2001, Siena, Italy.

• Nalon, C., Dixon, C., and Fisher, M. Resolution for Synchrony and No Learning: Preliminary Report. In Proc. 8th International Workshop on Logic Language, Information and Computation [WoLLIC'2001].

• Hustadt, U., Dixon, C., Schmidt, R., Fisher, M., Meyer, J-J., and van der Hoek, W. Verification within the KARO Agent Theory. In Proceedings of the First Goddard Workshop on Formal Approaches to Agent-Based Systems. Goddard Space Flight Center, Greenbelt, Maryland, USA. Volume 1871 of Lecture Notes in Artificial Intelligence, Springer-Verlag, 2001.

• Fisher, M. Direct Execution of Agent Specifications. In Proceedings of the First Goddard Workshop on Formal Approaches to Agent-Based Systems. Goddard Space Flight Center, Greenbelt, Maryland, USA. Volume 1871 of Lecture Notes in Artificial Intelligence, Springer-Verlag, 2001.

2000

• Fisher, M. and Kakoudakis, T.. Flexible Agent Grouping in Executable Temporal Logic. In, Gergatsoulis and Rondogiannis (eds), Intensional Programming II. World Scientific Publishers, March 2000. ISBN 981-02-4095-3.

• Fisher, M. Characterising Simple Negotiation as Distributed Agent-Based Theorem-Proving. In Proceedings of the Fifth International Conference on Multi-Agent Systems (ICMAS), Boston, USA, 2000.

• Hustadt, U., Dixon, C., Schmidt, R., and Fisher, M. Normal Forms and Proofs in Combined Modal and Temporal Logics. In Proceedings of the Third International Workshop on the Frontiers of Combining Systems (FroCoS'2000). Nancy, France. Volume 1794 of Lecture Notes in Artificial Intelligence. Springer-Verlag, 2000.

• Dixon, C., Fisher, M., and Bolotov, A. Resolution in a Logic of Rational Agency. In Proceedings of the 14th European Conference on Artificial Intelligence (ECAI 2000), Berlin, Germany 23rd-25th August 2000. IOS Press.

• Dixon, C., and Fisher, M. Resolution-Based Proof for Multi-Modal Temporal Logics of Knowledge. In Proceedings of the Seventh International Workshop on Temporal Representation and Reasoning (TIME'00), Cape Breton, Nova Scotia, Canada, July 7-9, 2000. IEEE Computer Society Press.

• Fisher, M., and Ghidini, C. Specifying and Implementing Agents with Dynamic Resource Bounds. In Proceedings of ECAI-2000 Workshop on Cognitive Robotics. Berlin, 2000.

1999

• Barringer, H., Fisher, M., Gabbay, D., and Gough, G. (eds) Advances in Temporal Logic.. Volume 16 of Applied logic series, Kluwer Academic Publishers, Dordrecht, December 1999. (ISBN 0-7923-6149-0)

• Fisher, M., and Dixon, C. Guiding Clausal Temporal Resolution. In Advances in Temporal Logic.. Kluwer Academic Publishers, Dordrecht, December 1999.

• Dixon, C., Fisher, M., and Reynolds, M. Execution and Proof in a Horn-Clause Temporal Logic. In Advances in Temporal Logic.. Kluwer Academic Publishers, Dordrecht, December 1999.

• Bolotov, A., Dixon, C., and Fisher, M. Clausal Resolution for CTL*. In Proceedings of the 24th International Symposium on Mathematical Foundations of Computer Science (MFCS). Volume 1672 of Lecture Notes in Computer Science.Springer-Verlag, 1999.

• Fisher, M., and Ghidini, C. Programming Resource-Bounded Deliberative Agents. In Proceedings of Sixteenth International Joint Conference on Artificial Intelligence. Morgan-Kaufmann, 1999.

1998

• Dixon, C., and Fisher, M. The Set of Support Strategy in Temporal Resolution. In Proceedings of the Fifth International Workshop on Temporal Reasoning (TIME'98). Sanibel Island, Florida, May 1998. IEEE Press.

• Scott, R., Fisher, M., and Keane, J. A. Parallel Temporal Tableaux. In Proceedings of Euro-Par Conference, Lecture Notes in Computer Science vol. 1470, Springer-Verlag, 1998.

• Mulder, M., Treur, J. and Fisher, M. Agent Modelling in Concurrent METATEM and DESIRE. In Intelligent Agents IV. LNAI, Springer-Verlag, 1998.

• Dixon, C., Fisher, M., and Wooldridge, M. Resolution for Temporal Logics of Knowledge. Journal of Logic and Computation 8(3):345-372, Oxford University Press, 1998. ISSN 0955-792X. (Preliminary version)

• Wooldridge, M., Dixon, C., and Fisher, M. A Tableau-Based Proof Method for Temporal Logics of Knowledge and Belief. Journal of Applied Non-Classical Logics 8(3):225-258, 1998.

• Fisher, M.. Representing Abstract Agent Architectures. In Intelligent Agents V. Springer-Verlag, 1999.

1997

• Fisher, M. A Normal Form for Temporal Logics and its Applications in Theorem-Proving and Execution. Journal of Logic and Computation 7(4):429-456, August 1997. Oxford University Press.

• Bolotov, A., and Fisher, M. A Resolution Method for CTL Branching-Time Temporal Logic. In Proceedings of the Fourth International Workshop on Temporal Representation and Reasoning (TIME). IEEE Press. 1997.

• Kellett, A. and Fisher, M. Automata Representations for Concurrent METATEM. In Proceedings of the Fourth International Workshop on Temporal Representation and Reasoning (TIME). IEEE Press. 1997.

• Kellett, A. and Fisher, M. Concurrent METATEM as a Coordination Language. In Coordination Languages and Models. Lecture Notes in Computer Science 1282, Springer-Verlag, 1997.

• Fisher, M. If Z is the answer, what could the question possibly be?. In J. Mueller, M. Wooldridge and N. R. Jennings, editors, Intelligent Agents III. Volume 1193 of Lecture Notes in Artificial Intelligence Springer-Verlag, January 1997.

• Fisher, M., and Wooldridge, M. Towards Formal Methods for Agent-Based Systems. In, D. Duke and A. Evans (eds), BCS-FACS Northern Formal Methods Workshop. Electronic Workshops in Computing, Springer-Verlag, 1997.

• Fisher, M., and Wooldridge, M., On the Formal Specification and Verification of Multi-Agent Systems. International Journal of Cooperative Information Systems 6(1):37-65. World Scientific Publishers. 1997.

• Fisher, M., Müller, J., Schroeder, M., Staniford, G., and Wagner, G. Methodological Foundations for Agent-Based Systems. Knowledge Engineering Review 12(3):323-329, 1997.

• Fisher, M. Refining Concurrent METATEM Objects. In, H. Bowman and J. Derrick, editors, Formal Methods for Open Object-Based Distributed Systems. Chapman and Hall, 1997.

• Fisher, M. An Open Approach to Concurrent Theorem-Proving. In Geller, Kitano and Suttner (eds) Parallel Processing for Artificial Intelligence, 3. Elsevier/North Holland, 1997.

• Fisher, M. and Kellett, A. Programming Dynamic Multi-Agent Systems. In J. Nealon and N. Taylor (eds) Proceedings of the UK Intelligent Agents Workshop, Oxford: SGES Publications, 1997.

• Fisher, M., and Wooldridge, M., Distributed Problem-Solving as Concurrent Theorem-Proving. In Boman and van de Velde, editors, Multi-Agent Rationality - Proceedings of the Eighth European Workshop on Modelling Autonomous Agents in a Multi-Agent World (MAAMAW-97), Springer-Verlag, 1997.

• Dixon, C., and Fisher, M. Tableaux for Synchronous Systems of Knowledge and Time with Interactions. In Proceedings of Scandinavian Conference on Artificial Intelligence (SCAI), Helsinki, Finland, 1997. IOS Press.

• Fisher, M. Implementing BDI-like Systems by Direct Execution. In Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence (IJCAI), Nagoya, Japan, August 1997. Published by Morgan Kaufmann.

1996

• Fisher, M., Kono, S., and Orgun, M., (eds). Journal of Symbolic Computation, Special Issue on Executable Temporal Logics, 22(5), November/December 1996, Academic Press.

• Barringer, H., Fisher, M., Gabbay, D., Owens, R., and Reynolds, M. (eds) The Imperative Future: Principles of Executable Temporal Logic. Research Studies Press, May 1996. (ISBN: 0-86380-190-0)

• Fisher, M. A Temporal Semantics for Concurrent METATEM. Journal of Symbolic Computation (Special Issue on Executable Temporal Logics) 22(5):627-648, November/December 1996, Academic Press.

• Johnson, R., Shen, K., Fisher, M., Keane, J. A., and Nisbet, A., An Abstract Machine For Prototyping Parallel Proof Mechanisms. In Proceedings of Abstract Machines Workshop, April 1996. IOS-Press (Concurrent Systems Engineering).

• Fisher, M., Wooldridge, M., and Dixon, C., A Resolution-Based Proof Method for Temporal Logics of Knowledge and Belief. In Proc. International Conference on Formal and Applied Practical Reasoning (FAPR), Bonn, Germany, June 1996. Published by Springer-Verlag as Lecture Notes in Computer Science vol. 1085.

• Fisher, M., An Introduction to Executable Temporal Logics. Knowledge Engineering Review 11(1). Cambridge University Press. March 1996

• Fisher, M., Hunter, A., Owens, R., Barringer, H., Gabbay, D., Gough, G., Hodkinson, I., McBrien, P., Reynolds, M., and Brough, D. Languages, Meta-languages, and METATEM. Journal of the IGPL 4(2), March 1996.

1995

• Fisher, M., and Owens, R. (eds) Executable Modal and Temporal Logics. Volume 897 of Lecture Notes in Artificial Intelligence. Springer-Verlag, 1995. (ISBN: 3-540-58976-7)

• Dixon, C., Fisher, M., and Johnson, R. Parallel Temporal Resolution. In Proceedings of the Second International Workshop on Temporal Representation and Reasoning (TIME). Melbourne Beach, Florida, April 1995.

• Fisher, M., and Keane, J. A. Realising a Concurrent Object-Based Programming Model on Parallel Virtual Shared Memory Architectures. In Programming Models for Massively Parallel Computers, IEEE Computer Society Press, 1995.

• Fisher, M. Towards a Semantics for Concurrent METATEM. In Executable Modal and Temporal Logics. Published by Springer-Verlag as Lecture Notes in Artificial Intelligence, volume 897. February 1995.

• Fisher, M., Johnson, R., and Keane, J. A. Graph Structure Management in Parallel Symbolic Systems, in Proceedings of Seventh IASTED International Conference on Parallel and Distributed Computing Systems, Washington D.C., USA, October 1995.

• Fisher, M., and Wooldridge, M., A Logical Approach to the Representation of Societies of Agents. In Gilbert and Conte (eds), Artificial Societies, UCL Press, 1995.

• Fisher, M., and Owens, R. An Introduction to Executable Modal and Temporal Logics. In Executable Modal and Temporal Logics. Volume 897 of Lecture Notes in Artificial Intelligence Springer-Verlag, February 1995.

• Barringer, H., Fisher, M., Gabbay, D., Gough, G., and Owens, R. METATEM: An Introduction. Formal Aspects of Computing 7(5):533-549, 1995. Springer Verlag. (Also, electronic supplement in Formal Aspects of Computing, 7(E))

• Fisher, M., Representing and Executing Agent-Based Systems, in Wooldridge, M., and Jennings, N. (eds), Intelligent Agents -- Proceedings of the International Workshop on Agent Theories, Architectures, and Languages, 1995. Published by Springer-Verlag as Lecture Notes in Computer Science vol. 890.

1994

• Dixon, C., Fisher, M., and Barringer, H. A Graph-Based Approach To Resolution In Temporal Logic. In Proceedings of First International Conference on Temporal Logic (ICTL). Bonn, Germany. Published by Springer-Verlag as Lecture Notes in Computer Science vol. 827. 1994.

• Fisher, M. A Survey of Concurrent METATEM -- The Language and its Applications. In Proceedings of First International Conference on Temporal Logic (ICTL). Bonn, Germany. Published by Springer-Verlag as Lecture Notes in Computer Science vol. 827. July 1994.

• Fisher, M., and Wooldridge, M., Specifying and Executing Protocols for Cooperative Action, In Proc. International Working Conference on Cooperating Knowledge-Based Systems (CKBS). Keele, U.K., June 1994.

• Wooldridge, M., and Fisher, M., A Decision Procedure for a Temporal Belief Logic. In Proc. First International Conference on Temporal Logic (ICTL). Bonn, Germany, July 1994. Published by Springer-Verlag as Lecture Notes in Computer Science vol. 827.

1993

• Fisher, M. Concurrent METATEM -- A Language for Modeling Reactive Systems. In Proceedings of Parallel Architectures and Languages Europe (PARLE). Munich, Germany. Published by Springer-Verlag as Lecture Notes in Computer Science vol. 694. June 1993.

• Finger, M., Fisher, M., and Owens, R. METATEM at Work: Modelling Reactive Systems Using Executable Temporal Logic. In Proceedings of Sixth International Conference on Industrial and Engineering Applications of Artificial Intelligence and Expert Systems (IEA-AIE). Edinburgh, U.K. Published by Gordon and Breach. June 1993.

• Fisher, M., and Wooldridge, M. Specifying and Verifying Distributed Intelligent Systems. In Progress in AI -- Proceedings of Portuguese Conference on Artificial Intelligence (EPIA). Porto, Portugal. Published by Springer-Verlag as Lecture Notes in Computer Science vol. 727. October 1993.

• Fisher, M., and Wooldridge, M., Temporal Logic Programming for Distributed A.I., in Proceedings of the Twelfth International Workshop on Distributed Artificial Intelligence (IWDAI), held in Hidden Valley Resort, Pennsylvania, May 1993.

1992

• Fisher, M. A Normal Form for First-Order Temporal Formulae. In Proceedings of Eleventh International Conference on Automated Deduction (CADE). Saratoga Springs, New York. Published by Springer-Verlag as Lecture Notes in Computer Science vol. 607. 1992.

• Fisher, M. A Model Checker for Linear Time Temporal Logic. Formal Aspects of Computing 4(3):299-319, 1992.

• Wooldridge, M., and Fisher, M., A First-Order Branching Time Logic of Multi-Agent Systems. In Proc. European Conference on Artificial Intelligence (ECAI). Vienna, Austria, August 1992. Published by Wiley and Sons.

• Fisher, M., and Noël P. Transformation and Synthesis in METATEM - Part I: Propositional METATEM. Technical Report UMCS-92-2-1, Department of Computer Science, University of Manchester, Manchester M13 9PL, U.K., February 1992.

• Fisher, M., and Owens, R. From the Past to the Future: Executing Temporal Logic Programs. In Proceedings of the Conference on Logic Programming and Automated Reasoning (LPAR). St. Petersberg, Russia. Published by Springer-Verlag as Lecture Notes in Computer Science vol. 624. July 1992.

1991

• Fisher, M. A Resolution Method for Temporal Logic. In Proceedings of Twelfth International Joint Conference on Artificial Intelligence (IJCAI). Sydney, Australia, August 1991. Published by Morgan Kaufmann. ISBN 1-55860-160-0

• Fisher, M., and Barringer, H. Concurrent METATEM Processes -- A Language for Distributed AI, in Proceedings of European Simulation Multiconference (ESM), held in Copenhagen, Denmark, June 1991. Published by SCS Press.

• Barringer, H., Fisher, M., Gabbay, D., and Hunter, A. Meta-Reasoning in Executable Temporal Logic. In Proceedings of Second International Conference on Principles of Knowledge Representation and Reasoning (KR). Cambridge, Massachusetts. Published by Morgan Kaufmann. April 1991.

• Fisher, M., Computerphobia and Adult Learners. Computer Education, vol. 68, June 1991.

Pre-1990

• Fisher, M. Characterising Temporal Logic, Technical Report UMCS-89-10-6, Department of Computer Science, University of Manchester, Manchester M13 9PL, U.K., October 1989.

• Barringer, H., Fisher, M., and Gough, G. Fair SMG and Linear Time Model Checking. In Proceedings of Workshop on Automatic Verification Methods for Finite State Systems. Grenoble, France. Published by Springer-Verlag as Lecture Notes in Computer Science vol. 407. June 1989.

• Barringer, H., Fisher, M., Gabbay, D., Gough, G., and Owens, R. METATEM: A Framework for Programming in Temporal Logic. In Proceedings of REX Workshop on Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness. Mook, Netherlands. Published by Springer-Verlag as Lecture Notes in Computer Science vol. 430. June 1989.

• Fisher, M. Temporal Logics for Abstract Semantics. Technical Report UMCS-87-12-4, Department of Computer Science, University of Manchester, Manchester M13 9PL, U.K., December 1987.

• Fisher, M., and Barringer, H. Program Logics: A Short Survey. Technical Report UMCS-86-11-1, Department of Computer Science, University of Manchester, Manchester M13 9PL, U.K., November 1986.

About this document ...

This document was generated using the LaTeX2HTML translator Version 2018 (Released Feb 1, 2018)

Copyright © 1993, 1994, 1995, 1996, Nikos Drakos, Computer Based Learning Unit, University of Leeds.
Copyright © 1997, 1998, 1999, Ross Moore, Mathematics Department, Macquarie University, Sydney.

The command line arguments were:
latex2html -no_navigation -t 'Home page: Michael Fisher' -split 1 -address MFisher@liverpool.ac.uk papers.tex

The translation was initiated on 2019-05-24