A Common Basis for Agent Organisation in BDI Languages ⋆ (2009)
Abstract. Programming languages based on the BDI style of agent model are now common. Within these there appears to be some, limited, agreement on the core functionality of agents. However, when we...
Programming Verifiable Heterogeneous Agent Systems ⋆ (2009)
Louise A. Dennis, Michael Fisher
Abstract. Our overall aim is to provide a verification framework for practical multi-agent systems. To achieve practicality, we must be able to describe and implement heterogeneous multi-agent...
Agent Deliberation in an Executable Temporal Framework (2009)
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...
A Common Basis for Agent Organisation in BDI Languages ⋆ (2009)
Abstract. Programming languages based on the BDI style of agent model are now common. Within these there appears to be some, limited, agreement on the core functionality of agents. However, when we...
A Common Basis for Agent Organisation in BDI Languages ⋆ (2009)
Abstract. Programming languages based on the BDI style of agent model are now common. Within these there appears to be some, limited, agreement on the core functionality of agents. However, when we...
Exploring the Future with Resource-Bounded Agents ∗ [INVITED CONTRIBUTION] (2008)
Abstract. We here describe research into the formal specification and implementation of resource-bounded agents. In particular, we provide an overview of our work on incorporating resource...
Foundations of Flexible Multi-Agent Programming ⋆ (2008)
Abstract. In this paper we are concerned with proposing, analyzing and implementing simple, yet flexible, constructs for multi-agent programming. In particular, we wish to extend programming...
Computational Logics and Agents — A Roadmap of Current Technologies and Future Trends (2008)
Michael Fisher, Rafael H. Bordini, Benjamin Hirsch, Paolo Torroni
The concept of an agent is increasingly used in contemporary software applications, particularly those involving the Internet, autonomous systems, or cooperation. However, with dependability and...
Organising Software in Active Environments (2008)
Benjamin Hirsch, Michael Fisher, Chiara Ghidini, Paolo Busetta
Abstract. In this paper, we investigate the use of logic-based multi-agent systems for modelling active environments. Our case study is an intelligent support system for a so-called “active...
Rafael H. Bordini, Michael Fisher, Willem Visser, Mike Wooldridge
In this talk, I will introduce an agent-oriented programming language, then address the use of model-checking techniques for the verification of multi-agent systems implemented in that programming...
Organising Software in Active Environments (2008)
Benjamin Hirsch, Michael Fisher, Chiara Ghidini, Paolo Busetta
Abstract. In this paper, we investigate the use of logic-based multi-agent systems for modelling active environments. Our case study is an intelligent support system for a so-called “active...
extended version of AgentSpeak (2008)
Rafael H. Bordini, Jomi F. Hübner, Michael Fisher, Joyce Martins, Álvaro F. Moreira, Renata Vieira, ...
A Java-based interpreter for an
A Common Semantic Basis for BDI Languages ∗ (2008)
As the concept of an ‘agent ’ becomes more popular, so the variety of programming languages based upon this concept increases. These agent-based programming languages range from minimal...
State-Space Reduction Techniques in Agent Verification£ (2008)
Rafael H. Bordiniý, Michael Fisher, Willem Visser, Michael Wooldridge
We have developed a set of tools to allow the use of model-checking techniques for the verification of systems directly implemented in an agent-oriented programming language. The success of model...
Uncertain Agent Verification through Probabilistic Model-Checking (2008)
Paolo Ballarini, Michael Fisher, Michael Wooldridge
Abstract. In many situations an agent’s behaviour can sensibly be described only in terms of a distribution of probability over a set of possibilities. In such case (agents’) decision-making...
Implementing Temporal Logics: Tools for Execution and Proof (2008)
Here we present an overview of a selection of tools for execution and proof based on temporal logic, and will outline both the general techniques used and problems encountered in implementing them....
ABSTRACT TOWARDS THE VERIFICATION OF HUMAN-ROBOT TEAMS (2008)
Michael Fisher, Edward Pearce, Mike Wooldridge, Maarten Sierhuis, Willem Visser, Rafael H. Bordini
Human-Agent collaboration is increasingly important. Not only do high-profile activities such as NASA missions to Mars intend to employ such teams, but our everyday activities involving interaction...
Computational Logics and Agents — A Roadmap of Current Technologies and Future Trends (2008)
Michael Fisher, Rafael H. Bordini, Benjamin Hirsch, Paolo Torroni
The concept of an agent is increasingly used in contemporary software applications, particularly those involving the Internet, autonomous systems, or cooperation. However, with dependability and...
Presentation Overview 1. Introduce Shoham’s agent-oriented (2008)
Mike Wooldridge, Michael Fisher
programming paradigm, based on a societal
Using Temporal Logic to Specify Emergent Behaviours in Swarm Robotic Systems (2008)
Alan Ft, Winfield Jin Sa, Clare Dixon, Michael Fisher
It is a characteristic of swarm robotics that specifying overall emergent swarm behaviours in terms of the low-level behaviours of individual robots is very difficult. Yet if swarm robotics is to...
A Common Basis for Agent Organisations in BDI Languages ⋆ (2008)
Abstract. Programming languages based on the BDI style of agent model are now common. Within these there appears to be some, limited, agreement on the core functionality of agents. However, when we...
Temporal Logic has achieved a significant role in Computer Science, in particular, within the formal specification and verification of concurrent and distributed systems [Pnueli 1977; Manna and...
Uncertain Agent Verification through Probabilistic Model-Checking (2008)
Paolo Ballarini, Michael Fisher, Michael Wooldridge
Abstract. In many situations an agent’s behaviour can sensibly be described only in terms of a distribution of probability over a set of possibilities. In such case (agents’) decision-making...
Temporal Logic with Capacity Constraints (2008)
Clare Dixon, Michael Fisher, Boris Konev
Abstract. Often when modelling systems, physical constraints on the resources available are needed. For example, we might say that at most N processes can access a particular resource at any moment...
Specifying and Reasoning about Uncertain Agents (2008)
Logical formalisation of agent behaviour is desirable, not only in order to provide a clear semantics of agent-based systems, but also to provide the foundation for sophisticated reasoning techniques...
Computational Logics and Agents — A Roadmap of Current Technologies and Future Trends (2008)
Michael Fisher, Rafael H. Bordini, Benjamin Hirsch, Paolo Torroni
The concept of an agent is increasingly used in contemporary software applications, particularly those involving the Internet, autonomous systems, or cooperation. However, with dependability and...
A Logical Implementation of Uncertain Agents (2008)
Abstract. We consider the representation and execution of agents specified using temporal logics. Previous work in this area has provided a basis for the direct execution of agent specifications, and...
A Common Basis for Agent Organisation in BDI Languages ⋆ (2008)
Abstract. Programming languages based on the BDI style of agent model are now common. Within these there appears to be some, limited, agreement on the core functionality of agents. However, when we...
Alam, Md Rowshon, Dixit, Vidula, Kang, Hyunmin, Li, Zi-Bo, Chen, Xiaoyuan, Trejo, JoAnn, ...
We describe the synthesis and characterization of a 5′ conjugate between a 2′-O-Me phosphorothioate antisense oligonucleotide and a bivalent RGD (arginine–glycine–aspartic acid) peptide that...
A Logical Approach to Simulating Societies (2007)
Michael Fisher, Michael Wooldridge
This paper describes a novel language for programming societies of intelligent artificial agents. In this language, called Concurrent METATEM, individual agents are programmed by giving them a...
Michael Fisher, Lluis Vila, Mit Press, Alessandro Artale, Enrico Franconi
Temporal extensions of Description Logics (DL) are relevant to capture the evolving behaviour of dynamic domains, and they have been extensively considered in the literature. Several approaches for...
Using a Miura-Gardner-Kruskal type construction, we show that the Camassa-Holm equation has an infinite number of local conserved quantities. We explore the implications of these conserved quantities...
Propositional Temporal Resolution Revised (2007)
Anatoli Degtiarev, Michael Fisher, B An, Bn C L
4> g B 1 : : : An ) g Bn C ) l ( n W i=1 A i ) ^ C ) l (wtr) where the loop side conditions ` B i :l and ` B i n W j=1 A j for all i 2 f1; : : : ; ng: have to be satised 2 . Proposition 1 A...
Graph Structure Management in Parallel Symbolic Systems (2007)
Michael Fisher, Robert Johnson, John Keane
We discuss the efficient exploitation of parallelism in systems where a common data structure is accessed, using message-passing, by a set of parallel processes. In particular, we provide a framework...
In this paper, we investigate the suitability of parallel architectures for the realisation of a novel objectbased computational model [21] encapsulated within programming languages such as [11]....
Resolution for Temporal Logics of Knowledge with Interactions (2007)
Combined temporal and modal logics have been used in computer science for reasoning about complex situations such as, for instance, the specication and verication of distributed [5] and multi-agent...
Boris Konev, Clare Dixon, Michael Fisher, Ullrich Hustadt
First-order temporal logic is a concise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex, recent...
Anatoly Degtyarev, Michael Fisher, Boris Konev
Abstract. First-order temporal logic is a concise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex,...
Chapter 1 VERIFICATION WITHIN THE KARO AGENT THEORY (2007)
Ullrich Hustadt, Clare Dixon, Renate A. Schmidt, Michael Fisher, John-jules Meyer
Wiebe van der Hoek
Boris Konev, Clare Dixon, Michael Fisher, Ullrich Hustadt
First-order temporal logic is a concise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex, recent...
Michael Wooldridge, Michael Fisher, Simon Parsons
MABLE is a language for the design and automatic verification of multi-agent systems. MABLE is essentially a conventional imperative programming language, enriched by constructs from the...
A Simplied Clausal Resolution Procedure for Propositional Linear-Time Temporal Logic (2007)
Anatoly Degtyarev, Michael Fisher, Boris Konev
Abstract. The clausal resolution method for propositional linear-time temporal logics is well known and provides the basis for a number of temporal provers. The method is based on an intuitive...
Algorithms for Guiding Clausal Temporal Resolution (2007)
M. Carmen Fern, Ez Gago, Michael Fisher, Clare Dixon
Abstract. Clausal temporal resolution is characterised by a translation of the formulae whose satisability is to be established to a normal form, step resolution (similar to classical resolution) on...
Computerphobia in Adult Learners (2007)
our lives, incidences of adults experiencing anxiety about technology (`technophobia') are on the increase. The field of technology that has advanced most rapidly in the last 40 years is that of...
Chapter 1 VERIFICATION WITHIN THE KARO AGENT THEORY (2007)
Ullrich Hustadt, Clare Dixon, Renate A. Schmidt, Michael Fisher
Wiebe van der Hoek
An Algorithm for Guiding Temporal Resolution (2007)
M. Carmen Fern, Ez Gago, Michael Fisher, Clare Dixon
Abstract. The clausal resolution method developed for discrete temporal logics involves translation to a normal form, classical resolution on formulae within states (termed step resolution) and...
Clare Dixon, Michael Fisher, Mark Reynolds
Abstract. Both proof, via clausal resolution, and execution, via the imperative future approach, depend on the use of a normal form for temporal formulae. While the systems developed have centred...
Clausal Resolution for CTL (2007)
Er Bolotov, Clare Dixon, Michael Fisher
Abstract. In this paper we consider proof techniques for branching-time temporal logics. While a considerable amount of research has been carried out regarding the relationship between finite...
Ullrich Hustadt, Clare Dixon, Renate A. Schmidt, Michael Fisher, John-jules Meyer
, and Wiebe van der Hoek 3
Alexander Bolotov, Michael Fisher, Clare Dixon
We consider the relationship between!-automata and a specic logical formulation based on a normal form for temporal logic formulae. While this normal form was developed for use with execution and...
Boris Konev, Anatoli Degtyarev, Clare Dixon, Michael Fisher, Ullrich Hustadt
First-order temporal logic is a concise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex, recent...
An Algorithm for Guiding Temporal Resolution (2007)
M. Carmen Fern, Ez Gago, Michael Fisher, Clare Dixon
The clausal resolution method developed for discrete temporal logics involves translation to a normal form, classical resolution on formulae within states (termed step resolution) and temporal...
Verifiable Multi-Agent Programs (2007)
Rafael H. Bordini, Michael Fisher, Willem Visser, Michael Wooldridge
AgentSpeak is a reactive planning language for programming autonomous agents. It has recently been shown that model checking techniques can be applied to the veri cation of AgentSpeak systems,...
Handling Equality in Monodic Temporal Resolution (2007)
Boris Konev Anatoli, Boris Konev, Michael Fisher
First-order temporal logic is a concise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence.
Radiation Pressure in Lyman-alpha Forest Clouds (2007)
The effective recombination coefficient, alpha_eff, is refined for optically thin cases. Radiation pressure in Lyman-alpha and HeII Lyman-alpha is calculated in terms of the number density and the...
The Hot Inter-Galactic Medium and the Cosmic Microwave Background (2007)
The physical characteristics of the Lyman-alpha forest cloud systems are combined with observations on the baryonic mass density of the Universe and constraints from primordial nucleosynthesis to set...
Inhibition of MDR1 expression with altritol-modified siRNAs (2007)
Fisher, Michael, Abramov, Mikhail, Van Aerschot, Arthur, Xu, Dong, Juliano, Rudolph L., Herdewijn, Piet
Altritol-modified nucleic acids (ANAs) support RNA-like A-form structures when included in oligonucleotide duplexes. Thus altritol residues seem suitable as candidates for the chemical modification...
Efficient First-Order Temporal Logic for Infinite-State Systems (2007)
Dixon, Clare, Fisher, Michael, Konev, Boris, Lisitsa, Alexei
In this paper we consider the specification and verification of infinite-state systems using temporal logic. In particular, we describe parameterised systems using a new variety of first-order...
Language Constructs for Multi-Agent Programming (2007)
Abstract. In this paper we are concerned with proposing, analyzing and implementing simple, yet flexible, constructs for multi-agent programming. In particular, we wish to extend programming...
Tractable Temporal Reasoning (2007)
Clare Dixon, Michael Fisher, Boris Konev
Temporal reasoning is widely used within both Computer Science and A.I. However, the underlying complexity of temporal proof in discrete temporal logics has led to the use of simplified formalisms...
A Common Semantic Basis for BDI Languages (2007)
Louise A. Dennis, Berndt Farwer, Rafael H. Bordini, Michael Fisher, Michael Wooldridge
Abstract. We describe the design of an intermediate language (AIL) for BDIstyle programming languages. AIL is not intended as yet another programming language, but is meant to provide a common...
Tractable Temporal Reasoning (2007)
Clare Dixon, Michael Fisher, Boris Konev
Temporal reasoning is widely used within both Computer Science and A.I. However, the underlying complexity of temporal proof in discrete temporal logics has led to the use of simplified formalisms...
A Common Semantic Basis for BDI Languages (2007)
Louise A. Dennis, Berndt Farwer, Rafael H. Bordini, Michael Fisher, Michael Wooldridge
Abstract. We describe the design of an intermediate language (AIL) for BDIstyle programming languages. AIL is not intended as yet another programming language, but is meant to provide a common...
Inhibition of MDR1 expression with altritol-modified siRNAs (2007)
Fisher, Michael, Abramov, Mikhail, Van Aerschot, Arthur, Xu, Dong, Juliano, Rudolph L., Herdewijn, Piet
Altritol-modified nucleic acids (ANAs) support RNA-like A-form structures when included in oligonucleotide duplexes. Thus altritol residues seem suitable as candidates for the chemical modification...
Is There a Future for Deductive Temporal Verification (2006)
Clare Dixon, Michael Fisher, Boris Konev
complexity; clausal temporal resolution. In this paper, we consider a tractable sub-class of propositional linear time temporal logic, and provide a complete clausal resolution calculus for it. The...
Model checking for multiagent systems: the MABLE language and its applications (2006)
Michael Wooldridge, Michael Fisher, Simon Parsons
We present MABLE, a fully implemented programming language for multiagent systems, which is intended to support the automatic verification of such systems via model checking. In addition to the...
Verifying Multi-Agent Programs by Model Checking (2006)
Rafael H. Bordini, Michael Fisher, Willem Visser, Michael Wooldridge
Abstract. This paper gives an overview of our recent work on an approach to verifying multi-agent programs. We automatically translate multi-agent systems programmed in the logic-based agent-oriented...
Is There a Future for Deductive Temporal Verification (2006)
Clare Dixon, Michael Fisher, Boris Konev
In this paper, we consider a tractable sub-class of propositional linear time temporal logic, and provide a complete clausal resolution calculus for it. The fragment is important as it captures...
Model checking for multiagent systems: the MABLE language and its applications (2006)
Michael Wooldridge, Michael Fisher, Simon Parsons
We present MABLE, a fully implemented programming language for multiagent systems, which is intended to support the automatic verification of such systems via model checking. In addition to the...
MetateM: The story so far (2005)
METATEM is a simple programming language based on the direct execution of temporal logic statements. It was introduced through a number of papers [35,2,3] culminating in a book collecting together...
Programming groups of rational agents (2004)
Computational power is increasing, and increasingly available, for example via the development of ubiquitous computing. Once large numbers of computational elements can communicate with each other,...
State-space Reduction Techniques in Agent Verification (2004)
Rafael H. Bordini, Michael Fisher, Willem Visser, Michael Wooldridge
We have developed a set of tools to allow the use of model-checking techniques for the verification of systems directly implemented in an agent-oriented programming language. The success of model...
Monodic ASMs and temporal verification, in (2004)
Michael Fisher, Alexei Lisitsa
Abstract. In this paper, we pursue the goal of automatic deductive verification for certain classes of ASM. In particular, we base our work on a translation of general ASMs to full first-order...
Using temporal logics of knowledge in the formal verification of security protocols (2004)
Temporal logics of knowledge are useful for reasoning about situations where the knowledge of an agent or component is important, and where change may occur in this knowledge over time. Here we use...
Optimal Forcing Patterns for Coupled Models of ENSO (2004)
Andrew M. Moore, Javier Zavala-garay, Youmin Tang, Richard Kleeman, Anthony T. Weaver, Jérôme Vialard, ...
The optimal forcing patterns for El Niño–Southern Oscillation (ENSO) are examined for a hierarchy of hybrid coupled models using generalized stability theory. Specifically two cases are...
Using temporal logics of knowledge in the formal verification of security protocols (2004)
Clare Dixon, Mari-carmen Fern, Ez Gago, Michael Fisher
Temporal logics of knowledge are useful for reasoning about situations where the knowledge of an agent or component is important, and where change may occur in this knowledge over time. Here we use...
Practical Reasoning for Uncertain Agents (2004)
Nivea De Ferreira, Michael Fisher
Logical formalisation of agent behaviour is desirable, not only in order to provide a clear semantics of agent-based systems, but also to provide the foundation for sophisticated reasoning techniques...
Organising Computation through Dynamic Grouping (2004)
Michael Fisher, Chiara Ghidini, Benjamin Hirsch
Abstract. There are a range of abstractions used for both modelling and programming of modern computational systems. While these abstractions may have been devised for specific purposes, the variety...
State-space Reduction Techniques in Agent Verification (2004)
Rafael H. Bordini, Michael Fisher, Willem Visser, Michael Wooldridge
We have developed a set of tools to allow the use of model-checking techniques for the verification of systems directly implemented in an agent-oriented programming language. The success of model...
Using temporal logics of knowledge in the formal verification of security protocols (2004)
Temporal logics of knowledge are useful for reasoning about situations where the knowledge of an agent or component is important, and where change in this knowledge may occur over time. Here we use...
Model checking rational agents (2004)
Rafael H. Bordini, Michael Fisher, Michael Wooldridge
techniques to automatically verify multiagent systems. Furthermore, property-based slicing can reduce a multiagent system’s state space, increasing model-checking efficiency. The analysis of a...
Antonis Kakas, Marinos Georgiades, I Nside, This I Ssue, Michael Fisher
Welcome to the seventh issue of the CoLogNET newsletter, the official newsletter of the Network of Excellence of Computational Logic. This issue includes a variety of interesting contributions. You...
State-space Reduction Techniques in Agent Verification (2004)
Rafael H. Bordini, Michael Fisher, Willem Visser, Michael Wooldridge
We have developed a set of tools to allow the use of model-checking techniques for the verification of systems directly implemented in an agent-oriented programming language. The success of model...
Using temporal logics of knowledge in the formal verification of security protocols (2004)
With the growth of the Internet, wireless computing and ubiquitous computing there is an increasing need to interchange sensitive data. Cryptographic protocols are commonly used to distribute keys...
Annals of Mathematics and Artificial Intelligence: introduction (2004)
Dix, Jurgen, Fisher, Michael, Levesque, Hector, Sterling, Leon
Abstract not available.
Monodic temporal resolution (2003)
Degtyarev, Anatoly, Fisher, Michael, Konev, Boris
Until recently, First-Order Temporal Logic (FOTL) has been little understood. While it is well known that the full logic has no finite axiomatisation, a more detailed analysis of fragments of the...
Model checking AgentSpeak (2003)
Rafael H. Bordini, Michael Fisher, Carmen Pardavila, Michael Wooldridge
This paper introduces AgentSpeak(F), a variation of the BDI logic programming language AgentSpeak(L) intended to permit the model-theoretic verification of multi-agent systems. After briefly...
Organising Logic-Based Agents (2003)
Michael Fisher, Chiara Ghidini, Benjamin Hirsch
Abstract. In this paper we address the task of organising multi-agent systems in order to collectively solve problems. We base our approach on a logical model of rational agency comprising a few...
Monodic temporal resolution (2003)
Anatoli Degtyarev, Michael Fisher, Boris Konev
Abstract. While it is well known that the full First-Order Temporal Logic (FOTL) has no finite axiomatisation, until recently a more detailed analysis of fragments of the logic has not been...
Monodic temporal resolution (2003)
Anatoli Degtyarev, Michael Fisher, Boris Konev
Until recently, First-Order Temporal Logic (FOTL) has been only partially understood. While it is well known that the full logic has no finite axiomatisation, a more detailed analysis of fragments of...
Monodic temporal resolution: the expanding domain case (2003)
Anatoli Degtyarev, Michael Fisher, Boris Konev
Temporal Logic has achieved a significant role in Computer Science, in particular, within the formal specification and verification of concurrent and distributed systems [13, 11, 10]. However, even...
Anatoli Degtyarev, Michael Fisher, Boris Konev
Abstract. Until recently, first-order temporal logic has been little understood. While it is well known that the full logic has no finite axiomatisation, a more detailed analysis of fragments of the...
Monodic temporal resolution (2003)
Anatoly Degtyarev, Michael Fisher, Boris Konev
Abstract. First-order temporal logic is a concise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex,...
Towards the implementation of first-order temporal resolution: the expanding domain case (2003)
Boris Konev, Anatoli Degtyarev, Clare Dixon, Michael Fisher, Ullrich Hustadt
First-order temporal logic is a concise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex, recent...
Model checking AgentSpeak (2003)
Rafael H. Bordini, Michael Fisher, Carmen Pardavila, Michael Wooldridge
This paper introduces AgentSpeak(F), a variation of the BDI logic programming language AgentSpeak(L) intended to permit the model-theoretic verification of multi-agent systems. After briefly...
Clare Dixon, Claudia Nalon, Michael Fisher
The paper describes tableaux based proof methods for temporal logics of knowledge allowing interaction axioms between the modal and temporal components. Such logics can be used to specify systems...
Using Temporal Logics of Knowledge in the Formal Verification of Security Protocols (2003)
Temporal logics of knowledge are useful for reasoning about situations where the knowledge of an agent or component is important, and where change in this knowledge may occur over time. Here we use...
Model checking AgentSpeak (2003)
Rafael H. Bordini, Michael Fisher, Carmen Pardavila, Michael Wooldridge
This paper introduces AgentSpeak(F), a variation of the BDI logic programming language AgentSpeak(L) intended to permit the model-theoretic verification of multi-agent systems. After briefly...
Model Checking Multi-Agent Programs with CASP (2003)
Rafael H. Bordini, Michael Fisher, Carmen Pardavila, Willem Visser, Michael Wooldridge
In order to provide generic development tools for rational agents, a number of agent programming languages are now being developed, often by extending conventional programming languages with...
Limits to the managerial state : negotiating workplace change in the civil service / (2002)
Thesis (Ph. D.)--University of Newcastle upon Tyne, 2002.
Searching for Invariants using Temporal Resolution (2002)
James Brotherston, Anatoli Degtyarev, Michael Fisher, Alexei Lisitsa
Abstract. In this paper, we show how the clausal temporal resolution technique developed for temporal logic provides an effective method for searching for invariants, and so is suitable for...
Equality and Monodic First-Order Temporal Logic (2002)
Anatoli Degtyarev, Michael Fisher, Alexei Lisitsa
Abstract. It has been shown recently that monodic first-order temporal logic without functional symbols but with equality is incomplete, i.e. the set of the valid formulae of this logic is not...
A simplified clausal resolution procedure for propositional linear-time temporal logic (2002)
Anatoly Degtyarev, Michael Fisher, Boris Konev
Abstract. The clausal resolution method for propositional linear-time temporal logics is well known and provides the basis for a number of temporal provers. The method is based on an intuitive...
A simplified clausal resolution procedure for propositional linear-time temporal logic (2002)
Anatoly Degtyarev, Michael Fisher, Boris Konev
Abstract. The clausal resolution method for propositional linear-time temporallogics is well known and provides the basis for a number of temporal provers. The method is based on an intuitive clausal...
Searching for Invariants using Temporal Resolution (2002)
James Brotherston, Anatoli Degtyarev, Michael Fisher, Alexei Lisitsa
Abstract. In this paper, we show how the clausal temporal resolution technique developed for temporal logic provides an effective method for searching for invariants, and so is suitable for...
On the Relationship between -Automata and Temporal Logic Normal Forms (2002)
Er Bolotov, Michael Fisher, Clare Dixon
We consider the relationship between!-automata and a specic logical formulation based on a normal form for temporal logic formulae. While this normal form was developed for use with execution and...
Searching for Invariants using Temporal Resolution (2002)
James Brotherston, James Brotherston, James Brotherston, Anatoli Degtyarev, Anatoli Degtyarev, Anatoli Degtyarev, ...
In this paper, we show how the clausal temporal resolution technique developed for temporal logic provides an effective method for searching for invariants, and so is suitable for mechanising a wide...
On the Relationship between {omega}-automata and Temporal Logic Normal Forms (2002)
Bolotov, Alexander, Fisher, Michael, Dixon, Clare
We consider the relationship between &ohgr;‐automata and a specific logical formulation based on a normal form for temporal logic formulae. While this normal form was developed for use with...
Liu, Bo, Fisher, Michael, Groves, Peter
Objective: Neointimal hyperplasia is a central feature in the pathogenesis of a variety of vascular pathologies. Mitogen-activated protein kinases (MAPK) are involved in the downstream transduction...
Towards first-order temporal resolution (2001)
Anatoli Degtyarev, Michael Fisher
Abstract. In this paper we show how to extend clausal temporal resolution to the ground eventuality fragment of monodic first-order temporal logic, which has recently been introduced by Hodkinson,...
Verification within the KARO agent theory (2001)
Ullrich Hustadt, Clare Dixon, Renate A. Schmidt, Michael Fisher, John-jules Meyer
Abstract. This paper discusses automated reasoning in the KARO framework. The KARO framework accommodates a range of expressive modal logics for describing the behaviour of intelligent agents. We...
Verification within the KARO agent theory (2001)
Ullrich Hustadt, Clare Dixon, Renate A. Schmidt, Michael Fisher
Summary. This chapter proposes two new methods for realising automated reasoning within agent-based systems. We concentrate on a core of the KARO framework, which is a specification framework for...
Resolution in a Logic of Rational Agency (2000)
Clare Dixon, Michael Fisher, Er Bolotov
Abstract. A resolution based proof system for a Temporal Logic of Possible Belief is presented and justified. This logic represents a combination of the branching-time temporal logic CTL and the...
Clausal Resolution for Logics of Time and Knowledge with Synchrony and Perfect Recall (2000)
Temporal logics of knowledge are widely used in the specification and analysis of distributed and multi-agent systems where the behaviour of a component is captured by its set of possible executions....
Resolution-Based Proof for Multi-Modal Temporal Logics of Knowledge (2000)
Temporal logics of knowledge are useful in order to specify complex systems in which agents are both dynamic and have information about their surroundings. We present a resolution method for...
Combinations of Modal Logics (2000)
Brandon Bennett, Clare Dixon, Michael Fisher, Ullrich Hustadt, Enrico Franconi, Ian Horrocks, ...
Combining logics for modelling purposes has become a rapidly expanding enterprise that is inspired mainly by concerns about modularity and the wish to join together different kinds of information. As...
Clausal Temporal Resolution (1999)
Fisher, Michael, Dixon, Clare, Peim, Martin
In this article, we examine how clausal resolution can be applied to a specific, but widely used, non-classical logic, namely discrete linear temporal logic. Thus, we first define a normal form for...
The Camassa-Holm Equation: Conserved Quantities and the Initial Value Problem (1999)
Fisher, Michael, Schiff, Jeremy
Using a Miura-Gardner-Kruskal type construction, we show that the Camassa-Holm equation has an infinite number of local conserved quantities. We explore the implications of these conserved quantities...
Rijke. Combinations of modal logics (1999)
Brandon Bennett, Clare Dixon, Michael Fisher, Ullrich Hustadt, Enrico Franconi, Ian Horrocks
Combining logics for modelling purposes has become a rapidly expanding enterprise that is inspired mainly by concerns about modularity and the wish to join together different kinds of information. As...
A Clausal Resolution Method for CTL Branching-Time Temporal Logic (1999)
Alexander Bolotov, Er Bolotov, Michael Fisher
In this paper we extend our clausal resolution method for linear time temporal logics to a branching-time framework. Thus, we propose an efficient deductive method useful in a variety of applications...
A Tableau-Based Proof Method for Temporal Logics of Knowledge and Belief (1998)
Michael Fisher, Michael Wooldridge, Clare Dixon
Abstract. In this paper we define two logics, KL n and BL n, and present resolutionbased proof methods for both. KL n is a temporal logic of knowledge. Thus, in addition to the usual connectives of...
The Set of Support Strategy in Temporal Resolution (1998)
A variety of proof methods have been developed to support the effective mechanisation of temporal logic. While clausal temporal resolution has been successfully employed for a range of problems, a...
Resolution for Temporal Logics of Knowledge (1998)
Clare Dixon, Michael Fisher, Michael Wooldridge
A resolution based proof system for a temporal logic of knowledge is presented and shown to be correct. Such logics are useful for proving properties of distributed and multi-agent systems. Examples...
A Tableau-Based Proof Method for Temporal Logics of Knowledge and Belief (1998)
Michael Wooldridge, Clare Dixon, Michael Fisher
ABSTRACT. In this paper we define two logics, KLn and BLn, and present tableau-based decision procedures for both. KLn is a temporal logic of knowledge. Thus, in addition to the usual connectives of...
A Tableau-Based Proof Method for Temporal Logics of Knowledge and Belief (1998)
Michael Wooldridge, Clare Dixon, Michael Fisher
. In this paper we define two logics, KLn and BLn , and present tableau-based decision procedures for both. KLn is a temporal logic of knowledge. Thus, in addition to the usual connectives of linear...
Resolution for Temporal Logics of Knowledge (1998)
Clare Dixon, Michael Fisher, Michael Wooldridge
A resolution based proof system for a temporal logic of knowledge is presented and shown to be correct. Such logics are useful for proving properties of distributed and multi-agent systems. Examples...
A Tableau-Based Proof Method for Temporal Logics of Knowledge and Belief (1998)
Michael Fisher, Michael Wooldridge, Clare Dixon
Abstract. In this paper we define two logics, KLn and BLn, and present resolutionbased proof methods for both. KLn is a temporal logic of knowledge. Thus, in addition to the usual connectives of...
Resolution for Temporal Logics of Knowledge (1998)
DIXON, CLARE, FISHER, MICHAEL, WOOLDRIDGE, MICHAEL
A resolution-based proof system for a temporal logic of knowledge is presented and shown to be correct. Such logics are useful for proving properties of distributed and multi-agent systems. Examples...
Guiding Clausal Temporal Resolution (1997)
Abstract. The effective mechanisation of temporal logic is vital to the application of temporal reasoning in many fields, for example the verification of reactive systems, the implementation of...
Formalisms for Multi-Agent Systems (1997)
Michael Fisher, Alessio Lomuscio, Michael Luck, Maarten De Rijke, Mark Ryan, Michael Wooldridge
Methodological foundations for agent-based systems (1997)
Michael Fisher, Jorg Muller, Michael Schroeder, Gerd Wagner, Geof Staniford
In spite of the rapid spread of agent technology, there is, as yet, little evidence of an engineering approach to the development of agent-based systems. In particular, development methods for these...
Distributed Problem-Solving as Concurrent Theorem Proving (1997)
Michael Fisher, Michael Wooldridge
. Our principal aim in this paper is to describe how distributed problem solving may fruitfully be viewed as concurrent theorem proving. Not only does this approach provide an expressive...
A Resolution Method for CTL Branching-Time Temporal Logic (1997)
Alexander Bolotov, Er Bolotov, Michael Fisher
In this paper we extend our clausal resolution method for linear temporal logics to a branching-time framework. The branching-time temporal logics considered are Computation Tree Logic (CTL), often...
An Open Approach to Concurrent Theorem-Proving (1997)
The purpose of this paper is twofold. Its main aim is to present an alternative mechanism for representing concurrent theorem-proving activity which primarily relies upon massive parallelism and...
Formalisms for Multi-Agent Systems (1997)
Mark D'Inverno, Michael Fisher, Alessio Lomuscio, Michael Luck, Maarten De Rijke, Mark Ryan, ...
This report is the result of a panel discussion at the First UK Workshop on Foundations of Multi-Agent Systems (FoMAS '96). All members of the panel are authors, listed alphabetically. as...
Methodological Foundations for Agent-Based Systems (1997)
Michael Fisher, Jörg Müller, Michael Schroeder, Gerd Wagner, Geof Staniford
this document. level, when substantial systems are built by large teams of software engineers, the use of (approved) development methods is likely to be mandatory. 2 Developing Agent-Based Systems
A Normal Form for Temporal Logic and its Application in Theorem-Proving and Execution (1997)
In this paper a normal form, called Separated Normal Form (SNF), for temporal logic formulae is described. A simple propositional temporal logic, based on a discrete linear model structure, is...
Methodological foundations for agent-based systems (1997)
Michael Fisher, Jörg Müller, Michael Schroeder, Gerd Wagner, Geof Staniford
In spite of the rapid spread of agent technology, there is, as yet, little evidence of an engineering approach to the development of agent-based systems. In particular, development methods for these...
Formalisms for Multi-Agent Systems (1997)
Michael Fisher, Alessio Lomuscio, Michael Luck, Maarten De Rijke, Mark Ryan, Michael Wooldridge
A Normal Form for Temporal Logics and its Applications in Theorem-Proving and Execution (1997)
In this paper a normal form, called Separated Normal Form (SNF), for temporal logic formulae is described. A simple propositional temporal logic, based on a discrete linear model structure, is...
Languages, Meta-languages and METATEM, A Discussion Paper (1996)
BARRINGER, HOWARD, GOUGH, GRAHAM, BROUGH, DEREK, GABBAY, DOV, HODKINSON, IAN, HUNTER, ANTHONY, ...
Meta-languages are vital to the development and usage of formal systems, and yet the nature of meta-languages and associated notions require clarification. Here we attempt to provide a clear...
Representing and Executing Agent-Based Systems (1995)
Abstract. In this paper we describe an approach to the representation and implementation of agent-based systems where the behaviour of an individual agent is represented by a set of logical rules in...
Towards a Semantics for Concurrent METATEM (1995)
Abstract. Concurrent METATEM is a programming language based on the notion of concurrent, communicating objects, where each object directly executes a specification given in temporal logic, and...
Parallel Temporal Resolution (1995)
Clare Dixon, Michael Fisher, Rob Johnson
Temporal reasoning is complex. Typically, the proof methods used for temporal logics are both slow and, due to the quantity of information required, consume a large amount of space. The introduction...
Parallel Temporal Resolution (1995)
Clare Dixon, Michael Fisher, Rob Johnson
Temporal reasoning is complex. Typically, the proof methods used for temporal logics are both slow and, due to the quantity of information required, consume a large amount of space. The introduction...
A survey of Concurrent MetateM — the language and its applications (1994)
Abstract. In this paper we present a survey of work relating to the Concurrent METATEM programming language. In addition to a description of the basic Concurrent METATEM system, which incorporates...
Specifying and Executing Protocols for Cooperative Action (1994)
Michael Fisher, Michael Wooldridge
The purpose of this paper is twofold: (i) to illustrate and re-emphasize the use of CONCURRENT METATEM, a programming language based on executable temporal logic, as a viable framework in which to...
A graph-based approach to resolution in temporal logic (1994)
Clare Dixon, Michael Fisher, Howard Barringer
Abstract. In this paper, we present algorithms developed in order to implement a clausal resolution method for discrete, linear temporal logics, presented in [Fis91]. As part of this method, temporal...
Specifying and Executing Protocols for Cooperative Action (1994)
Michael Fisher, Michael Wooldridge
The purpose of this paper is twofold: (i) to illustrate and re-emphasize the use of CONCURRENT METATEM, a programming language based on executable temporal logic, as a viable framework in which to...
A Decision Procedure for a Temporal Belief Logic (1994)
Michael Wooldridge, Michael Fisher
. This paper presents a temporal belief logic called L TB . In addition to the usual connectives of linear discrete temporal logic, L TB contains an indexed set of modal belief connectives, via which...
Agent-Based Software Engineering (1994)
Mike Wooldridge, Michael Fisher
ion . An agent in AOP (as in DAI) is an autonomous concurrently executing reactive process... Autonomy: agents execute without direct human or other intervention, and have control over their own...
Specifying and Executing Protocols for Cooperative Action (1994)
Michael Fisher, Michael Wooldridge
The purpose of this paper is twofold: (i) to illustrate and re-emphasize the use of CONCURRENT METATEM, a programming language based on executable temporal logic, as a viable framework in which to...
A decision procedure for a temporal belief logic (1994)
Michael Wooldridge, Michael Fisher
Abstract. This paper presents a temporal belief logic called ¢ TB. In addition to the usual connectives of linear discrete temporal logic, ¢ TB contains an indexed set of modal belief connectives,...
A decision procedure for a temporal belief logic (1994)
Michael Wooldridge, Michael Fisher
Abstract. This paper presents a temporal belief logic called LTB. In addition tothe usual connectives of linear discrete temporal logic,
METATEM at work: Modelling Reactive Systems using Executable Temporal Logic (1993)
Marcelo Finger, Michael Fisher, Richard Owens
In this paper we describe the application of a high-level programming language to the abstract modelling of transport systems. We show how METATEM, a language based upon the execution of temporal...
Specifying and Verifying Distributed Intelligent Systems (1993)
Michael Fisher, Michael Wooldridge
Abstract. This paper describes first steps towards the formal specification and verification of Distributed Artificial Intelligence (DAI) systems, through the use of temporal belief logics. The paper...
Concurrent MetateM --- A Language for Modeling Reactive Systems (1993)
Abstract. In this paper, a language based on the notion of concurrent, communicating objects is presented. Each object executes a specification given in temporal logic and communicates with other...
Specifying and Verifying Distributed Intelligent Systems (1993)
Michael Fisher, Michael Wooldridge
. This paper describes first steps towards the formal specification and verification of Distributed Artificial Intelligence (DAI) systems, through the use of temporal belief logics. The paper first...
Executable Temporal Logic for Distributed A.I. (1993)
Michael Fisher, Michael Wooldridge, Manchester M Gd
This paper describes Concurrent METATEM, a programming language based on temporal logic, and applies it to the study of Distributed Artificial Intelligence (DAI). A Concurrent METATEM system consists...
Executable Temporal Logic for Distributed A.I. (1993)
Michael Fisher, Michael Wooldridge, Manchester M Gd
This paper describes Concurrent MetateM, a programming language based on temporal logic, and applies it to the study of Distributed Artificial Intelligence (DAI). A Concurrent MetateM system consists...
Executable Temporal Logic for Distributed A.I (1993)
Michael Fisher, Michael Wooldridge
DAI’93 Themes: societies and organisations of agents; modeling through communication in adversarial and cooperative systems This paper describes Concurrent METATEM, a programming language based on...
Specifying and Verifying Distributed Intelligent Systems (1993)
Michael Fisher, Michael Wooldridge
Abstract. This paper describes first steps towards the formal specification and verification of Distributed Artificial Intelligence (DAI) systems, through the use of temporal belief logics. The paper...
From the Past to the Future: Executing Temporal Logic Programs (1992)
Abstract. We describe some of the techniques which have been used to implement METATEM, a programming language based on temporal logic, and address problems such as non-determinism and looping which...
A Model Checker for Linear Time Temporal Logic (1992)
This report describes the design and implementation of a model checker for linear time temporal logic. The model checker uses a depth-first search algorithm that attempts to find a minimal satisfying...
A normal form for first-order temporal formulae (1992)
In this paper a normal form for formulae of a first-order temporal logic is described. This normal form, called First-Order Separated Normal Form (SNF f), forms the basis of both a temporal...
Transformation and Synthesis in METATEM -- Part I: Propositional METATEM (1992)
Michael Fisher, Michael Fisher
In this report, the syntactic manipulation of temporal logic programs is considered. Transformation rules are provided for a temporal programming language that forms part of the METATEM framework for...
A First-Order Branching Time Logic OF MULTI-AGENT SYSTEMS (1992)
Michael Wooldridge, Michael Fisher
This paper presents a first-order branching time temporal logic that is suitable for describing and reasoning about a wide class of computational multi-agent systems. The logic is novel in that it...
Concurrent METATEM Processes --- A Language for Distributed AI (1991)
Michael Fisher, Howard Barringer
In this paper, we introduce Concurrent METATEM Processes, a high-level language for modeling distributed and concurrent systems. This language represents an operational model for a variety of...
Meta-reasoning in Executable Temporal Logic (1991)
Howard Barringer, Michael Fisher, Oxford Road, Dov Gabbay, Anthony Hunter
Temporal logic can be used as a programming language. If temporal formulae are represented in the form of an implication where the antecedent refers to the past, and the consequent refers to the...
A Resolution Method for Temporal Logic (1991)
In this paper, a resolution method for propositional temporal logic is presented. Temporal formulae, incorporating both past-time and future-time temporal operators, are converted to Separated Normal...
Meta-reasoning in Executable Temporal Logic (1991)
Howard Barringer, Michael Fisher, Dov Gabbay, Anthony Hunter
Temporal logic can be used as a programming language. If temporal formulae are represented in the form of an implication where the antecedent refers to the past, and the consequent refers to the...
MetateM: A Framework for Programming in Temporal Logic (1989)
Howard Barringer, Michael Fisher, Dov Gabbay, Graham Gough, Richard Owens
Department of Computer Science, University of Manchester,
MetateM: A Framework for Programming in Temporal Logic (1989)
Howard Barringer, Michael Fisher, Dov Gabbay, Graham Gough, Richard Owens
Abstract. In this paper we further develop the methodology of temporal logic as an executable imperative language, presented by Moszkowski [Mos86] and Gabbay [Gab87, Gab89] and present a concrete...
Accreditation of schools was begun by The University of Michigan in 1871 as a culling process for entering freshmen. Regional accrediting agencies such as the North Central Association of Colleges...
McKallip, Robert J., Fisher, Michael, Gunthert, Ursula, Szakal, Andras K., Nagarkatti, Prakash S., Nagarkatti, Mitzi
Exposure to bacterial superantigens such as staphylococcal enterotoxin B (SEB) leads to the induction of toxic shock syndrome which results in multiorgan failure, including liver damage. In the...
Xu, Dong, McCarty, Doug, Fernandes, Alda, Fisher, Michael, Samulski, R. J., Juliano, R. L.
Small interfering RNAs (siRNAs) are potentially powerful tools for therapeutic gene regulation. DNA cassettes encoding RNA polymerase III promoter-driven hairpin siRNAs allow long-term expression of...
McKallip, Robert J., Fisher, Michael, Gunthert, Ursula, Szakal, Andras K., Nagarkatti, Prakash S., Nagarkatti, Mitzi
Exposure to bacterial superantigens such as staphylococcal enterotoxin B (SEB) leads to the induction of toxic shock syndrome which results in multiorgan failure, including liver damage. In the...
Inhibition of MDR1 expression with altritol-modified siRNAs
Fisher, Michael, Abramov, Mikhail, Van Aerschot, Arthur, Xu, Dong, Juliano, Rudolph L., Herdewijn, Piet
Altritol-modified nucleic acids (ANAs) support RNA-like A-form structures when included in oligonucleotide duplexes. Thus altritol residues seem suitable as candidates for the chemical modification...
Psychiatric Morbidity in an Urban Group Practice [Abridged]1
Shepherd, Michael, Fisher, Michael, Stein, Lilli, Kessel, W. I. N.
Jared Creason, Michael Fisher, Svetlana Semenova, Susan F. Stone
A highly disaggregated emissions factor model is presented. The model generates changes in emissions and resource use by state and 6-digit NAICS sector. Removal of all U.S. import restrictions is...
Intracellular delivery of an anionic antisense oligonucleotide via receptor-mediated endocytosis
Alam, Md Rowshon, Dixit, Vidula, Kang, Hyunmin, Li, Zi-Bo, Chen, Xiaoyuan, Trejo, JoAnn, ...
We describe the synthesis and characterization of a 5′ conjugate between a 2′-O-Me phosphorothioate antisense oligonucleotide and a bivalent RGD (arginine–glycine–aspartic acid) peptide that...
Tudor, Lynne G., Besedin, Elena, Fisher, Michael, Smith, Stuart
The present study focuses on a state-wide case study to evaluate recreational benefits from forthcoming effluent limitation guidelines for the Metal Products and Machinery Industry. The study...
Gilge, Jasen Lee, Fisher, Michael, Chai, Yuh-Cherng
Cellular molecules possess various mechanisms in responding to oxidant stress. In terms of protein responses, protein S-glutathionylation is a unique post-translational modification of protein...
Computational results for very large air crew scheduling problems
Baker, Edward, Fisher, Michael
The airline crew scheduling problem is typically formulated as a set covering problem. The Federal Express Corporation has recently implemented a heuristic crew scheduling system based on this model....
Creason, Jared, Fisher, Michael, Semenova, Svetlana, Stone, Susan F.
A highly disaggregated emissions factor model is presented. The model generates changes in emissions and resource use by state and 6-digit NAICS sector. Removal of all U.S. import restrictions is...