Home page: Michael Fisher

Research Outputs

: [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]

2013

Konur, S., Fisher, M., Dobson, S., and Knox, S. Formal Verification of a Pervasive Messaging System. Formal Aspects of Computing, 2013. [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.
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.

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. To appear 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.

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 2002-2-1 (1.71)

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 by Michael Fisher on 2013-05-23

MFisher@liverpool.ac.uk