Project Description

Problem Addressed

Software agents have recently become a popular means of exploiting the increased computing resources and concurrency available in modern computing systems, especially distributed systems. Agents are processes to which tasks are delegated. Typically, they can migrate among nodes to promote load balancing, they can be cloned to promote dynamic concurrency, and they are relatively autonomous to promote low user interaction. To realize the paradigm fully, an agent is endowed with a certain autonomous competence, or knowledge, and engages in goal-directed behavior; these are attributes that bring agents within the realm of artificial intelligence (AI). To implement agents, we must be able to characterize them and what is required of them. To begin with, there are the competence and dispositions (knowledge and beliefs) attributed to agents. A very significant sort of knowledge is the common knowledge shared by a group of agents, which enables collaboration. There are also the actions and activities in which agents engage and the preconditions required by and effects established by the actions. Finally, agents must communicate; indeed, perhaps the most significant acts of agents are communication acts.

Many of the issues that arise when we attempt to characterize agents are issues that have traditionally been addressed by philosophy. To analyze such issues, philosophers have developed extensive logic formalisms. Some of these formalisms have been used in AI or in formal methods for concurrent systems, and some are now being applied to agents. This transfer of formalisms is natural since the emphasis is on formal aspects that can characterize either humans or software processes. Such a transfer of formalisms has already been widely accepted in the study of concurrency, where temporal logics, originally developed by philosphers, are used not only for specification and thus for the development of reliable software but also to supply the semantics for concurrency constructs in programming languages. Although temporal and similar logics apply to systems of agents (which are concurrent processes) other aspects of agents (such as knowledge and communication acts) call for other kinds of formalisms. To develop reliable agent software and to supply semantics for agent communication languages, we need the appropriate formalisms to capture requirements, to express and to reason about specifications, and to express the meanings of language constructs.

Several formalisms developed in philosophy have been applied to agents with considerable promise. The primary problem we propose to address is the specification, using a selection of formalisms, of certain aspects and intended applications of the AGENTS model of distributed agents being developed at the Goddard Space Flight Center. This includes reasoning about such specifications to establish their adequacy and to draw out their implications. The aspects include user interfaces (one of the three major classes of agents in the AGENTS model is User Interface Agents) and sharable ontologies (another major class of agents in this model is Domain Specific Agents, whose collaboration depends on commitment to shared ontologies). The aspects also include higher-level capabilities emphasized above (such as knowledge) and communication mechanisms (with communication acts viewed in the speech-act tradition developed in philosophy). Once the specification problem has been adequately addressed, we propose to explore the application of our concepts and frameworks to issues that bear on implementation, such as the semantics of language constructs and collaborative default reasoning.

Objectives

The first and principal objective of the proposed effort will be to select and develop the appropriate formalisms for specifying agent systems and to develop a methodology for the use of these formalisms. The agent systems of interest will be assumed to conform to the AGENTS model of distributed agents being developed at the Goddard Space Flight Center. The scope of the formalisms will cover agent knowledge (including common or shared knowledge), agent actions and activities, and agent communication acts (viewed as speech acts). This scope will also encompass temporal aspects, the subject of concurrency formalisms, including temporal logics. Also, formalisms concerning user interfaces will be investigated; user interfaces will be subsumed as much as possible under agent interfaces in general, so the formalisms of general interest will be applied to user interfaces as well. Finally, general ontology will be exploited for foundations for domain-specific ontologies, which are critically involved in analyses of agent speech acts, agent knowledge, and agent actions.

We shall aim at developing formalisms and methodologies that equal in rigor and utility the concurrency formalisms already in use. Methodology will fall under both software engineering and AI. On the side of software engineering, our methodology will be located in the early part of the software life cycle: requirements capture and analysis. In particular, we shall use domain analysis, which has borrowed knowledge acquisition techniques from AI for requirements capture, and state-of-the-art approaches in object-oriented analysis. Reusability will be emphasized and design patterns will be formulated to assist in requirements capture and analysis. Of course, our formalisms will be used throughout. On the side of AI, our methodology will relate to knowledge acquisition; the knowledge representation schemes this presupposes will be furnished by our formalisms. In particular, the view we shall take of knowledge acquisition will be similar to that of the DS methodology, that is, as an incremental modeling process embedded in a software life cycle, consistent with contemporary software engineering practice. Our use of formalisms will be similar to several formal knowledge modeling approaches, such as the KARL knowledge acquisition and representation language, that have enhanced the general KADS framework.

Critical for this effort will be not only a clear methodology for exploiting our formalisms but also rigorous methods for reasoning with these formalisms; this latter goal is achieved by only the more formal approaches to software engineering and knowledge acquisition. Such reasoning methods allow one to verify that certain desired properties have been captured by a specification; they also allow one to elaborate specifications and to verify that the desired properties are preserved, thus supporting incremental analysis and design.

Test cases for our formalisms and methodology will be taken from the intended application areas of the Goddard AGENTS model, essentially mission operations systems, where one end is the spacecraft and the other consists of the ground-based operators and mission scientists. We shall in particular handle the proof-of-concept applications under development: (1) on-line and off-line flight operations support services, (2) spacecraft platform and instrument Fault Detection, Isolation, and Recovery services, and (3) information location, retrieval, and processing services. Test cases for our methodology will be developed to the point where prototypes are implemented in languages deemed appropriate by the Goddard personnel.

A major output of this effort will be a user's document presenting the formalisms and methodology. This document will be largely self-contained and will focus on the practical use of the methodology by users who have little background in the formalisms.

The primary goal of the document will be to allow our formalisms and methodology to be integrated into the work with agents at Goddard. Subsequent objectives will be directed to issues that broadly fall under the heading of implementation. We believe that the conceptual and formal issues in the area of distributed agents are best addressed initially in the realm of specification since this abstracts from the difficulties introduced by implementation. Once, however, we have a handle on these issues, our insights and results can be exploited in agent languages and systems. Thus, one subsequent objective is to relate our formalisms to Goddard's focus on developing an agent communication language. This will involve supplying the semantics for language constructs that relate to agent knowledge, agent activity, and agent speech acts. Other subsequent objectives relate to the development of algorithms and protocols required by agent systems; these algorithms and protocols would help enable such activities as multi-agent planning, collaborative reasoning and action, and default reasoning in communication. Selection of which activities to facilitate will be made after the specification formalisms have been soundly established and the power of these formalisms for expressing data structures, algorithms, and protocols can be properly assessed.

Finally, a general objective to be pursued throughout the proposed effort is to develop African-American student researchers in computer science. All of the undergraduate researchers involved in the proposed effort will be African-American and it is anticipated that most will go on to pursue advanced degrees in computer science. Also, all of the masters students involved will be African-American, and it is anticipated that some of these will pursue doctoral degrees in computer science; the others will have research experience that they will apply in industry and government. In particular, these minority students will develop close research relations with NASA.

Relation to Other Work

The term "agent" has been used for many things in computational settings. In AI, "agent" is generally used for a persistent entity in an often unpredictable environment including a community of other agents. Shoham [Sh93] defines an agent as an entity whose state is viewed as consisting of mental components. So the question of agenthood is the question of what can be viewed as having mental states, and the answer is anything, although it is not always advantageous to do so. We question the utility of talk about the mental; it suffices that certain processes perform communication (or speech) acts, have dispositions that agree from a formal point of view with our talk of knowledge and belief, and be subject to rules that promote cooperative behavior. For our purposes, we can assume that the rules are social laws imposed in advance, although emergent conventions are an important topic in agent theory. The current consensus, with which we agree, is to treat agent communication as speech acts. The minimal units of human communication are taken to be certain speech acts called illocutionary acts [Se69]. An illocutionary act consists of an illocutionary force (e.g., of asserting, questioning, accepting, or proclaiming) and a propositional content. Illocutionary logic, which has recently been formalized [SV85], is the logical theory of illocutionary acts. In this agent paradigm, a central role is occupied by agent communication languages based on speech act theory. Shoham [Sh93] views agent-oriented programming (AOP) as a specialization of object-oriented programming (OOP), taking OOP in the spirit of Hewitt's Actors formalism. AOP specializes OOP by (1) constraining the (mental) states of the agents (modules) so that they are consonant with ascription of knowledge, commitment, and so on, and (2) viewing computation as patterns of speech acts. Smith and Cohen [SC95] view agent communication as a task-oriented dialogue for building, maintaining, and disbanding teams. They use a speech act model based on joint intentions. We propose, rather than to take agent communication languages as our point of departure, to begin with the problem of specifying agent systems, especially agent behavior, including speech acts. Specification is more tractable since it does not face the complexities of implementation and allows several complementary approaches to be used simultaneously. Furthermore, specification will be particularly useful for Goddard in applying their AGENTS model. Finally, specification can be picked up incrementally by the graduate and undergraduate research assistants as they come on the project. Moving beyond speech acts, the family of formalisms that apply perhaps most ubiquitously to agents are those for time and concurrency. There is a mature research discipline of concurrency formalisms for communicating parallel and distributed systems. The major formalisms for modeling concurrency are temporal logics, process algebras, and Petri nets. A temporal logic includes temporal operators (corresponding to, for example, "always" and "eventually") applied to propositions to indicate the extent of time these propositions hold. The power of a temporal logic is needed to describe the effects of a reactive program, whose role is to maintain some ongoing interaction with its environment. A process algebra is a mathematical language with basic constants, operators to construct larger processes, and equations as axioms to describe the nature of processes. Process terms constitute an abstract concurrent language that stresses how complex processes are composed from simpler ones by a set of process operators (e.g., parallel, sequential, and alternative composition). A Petri net is an automaton that is generally portrayed as a graph connecting each transition with its input and output places. A transition represents a discrete event; its input places describe the preconditions of that event, and its output places describe the postconditions of that event. Temporal logics are similar to modal logics; when time is discrete, they can be assimilated to modal logics. A modal logic enhances standard logic with modal operators, especially ( and (, where (p is read "it is necessary that p" and (p is read "it is possible that p". The interpretation of a modal logic assumes a set of "possible worlds" and an accessibility relation between worlds. Atomic propositions are assigned possibly different truth values in different worlds. (p is true in a given world w if p is true in all worlds accessible to w; (p is true in w if p is true in some world accessible to w. Temporal logics in AI and computer science generally refer only to the present and future time. ( is interpreted as "always" and ( is interpreted as "eventually". Some temporal logics are interpreted over instants and others are interpreted over intervals of time. Instant temporal logics may require a linear time or a branching time; in the latter case, other operators are usually introduced to indicate all branches (possibilities) or some. Temporal logics have been used in the proof of correctness of programs but more often are used for specification. They have also been used in AI in connection with planning and action. Model checking affords an efficient way to check whether formulas in certain propositional instant temporal logics are valid relative to a finite system. More general, but less efficient, verification techniques have been developed. There are modal logics that are not properly temporal logics that have been used for specification of concurrent systems. Dynamic logic allows modal formulas of the form (r(p, where r is a regular program over a set of program symbols; it is true if p is true after some execution of r (that is, after some sequence of actions in the set of such sequences denoted by r). [r]p is true if p is true after every execution of r. Logics similar to dynamic logic are used in conjunction with process algebras (or Petri nets). Temporal (or concurrency) formalisms used for agent and kindred systems in AI have generally been restricted to temporal logics although dynamic logic has spawned some interest. One of the exceptions is our work [Es96] (following Georgeff and Stuart) that uses a modified form of process algebra as an algebra for composing plans; we derive from plan terms constraints in an executable interval temporal logic that prevent attempted executions of atomic plans whose preconditions are unfulfilled. We intend to consider the utility of process algebras and Petri nets for agents. Also, process algebras appear to be appropriate formalisms for expressing the semantics of concurrent programming languages. And process algebras have been combined with formalisms for specifying data types and algorithms on them to allow both communication and local computation to be specified. This combination, however, has led to complex specifications that often go beyond practical analysis techniques. This is a lesson that should be taken to heart by those who seek to specify both the communication and the local computation of agents. All three types of concurrency formalisms have timed extensions to model real-time systems. Agents are generally assumed to operate in a real-time context; we intend to consider appropriate timed extensions of the formalisms we adopt. Epistemic logics [MV95] are modal logics in which ( (the "strong" modality) is written as Ka, where a denotes an agent; Kap means that a knows that p. In the semantics of epistemic logics, the accessibility relation between possible worlds is usually taken to reflect some sort of similarity or possible evolution between worlds. We can define and operator E, where Ep means "everyone knows that p", as Ep = K1p ( K2p ( ¬ ( Kmp, where {1,2,¬,m} is the set of agents. We then define C, where Cp means "it is common knowledge that p", as Cp = p ( Ep ( EEp ( ¬. Epistemic logics have been used to reason about distributed systems [HM90]. The set of possible worlds then is taken to be the set of global states of the system, each a vector of local processor states. Using epistemic operators, it is also possible to give compact and exact specifications of protocols, which can be easily transferred into programs [HZ87]. A group of agents has implicit (or distributed) knowledge of a fact if the knowledge of the fact is distributed over the members of that group. [FV86] show how to apply the notion of implicit knowledge to distributed systems. Generally, we accept the proposition Kap r p as logically true; if we replace 'Ka' with 'Ba', where Bap means that a believes that p, this is no longer necessarily true. Logics of belief are called doxastic logics. Multi-modal systems involving temporal and epistemic operators or temporal and doxastic operators are motivated by change of knowledge or belief over time in a principled way, say, due to agent actions. In fact, some systems have temporal, epistemic, and doxastic operators. We intend to use epistemic logics in specifications of agent systems. They have shown their value for distributed systems in general, and the notions that can be defined with them clearly relate to agents in our sense. Epistemic states tie in with speech acts, which allow illocutionary forces of informing, correcting, and so on. Temporal or dynamic logic operators fit naturally in this setting since speech act patterns dictate important relations of temporal order. Doxastic logics do not have the track record of epistemic logics, but they too may be natural here since the actions of an agent depend on its beliefs, and speech acts in particular depend on and engender beliefs. Deontic logics [Aq84,MW93] are modal logics of obligation. ( is replaced by O ("one is obligated to ¬"), ( is replaced by P ("one is permitted to ¬"), and (P is abbreviated as F ("one is forbidden to ¬"). Using an atom that represents a violation, one can reduce deontic logics to dynamic logic. In any case, since obligations are incurred by actions, deontic logics are often enhanced with action operators. The deontic operators, like the K of epistemic logic, are often indexed with an agent name. Legal reasoning is full of deontic notions, and several AI approaches to legal reasoning have employed deontic logic. Authorization mechanisms, which provide actors with the permission to perform certain activities, have been modeled with deontic logic. [KM87] have used deontic logic in system specification. Using the appropriate sense of "precondition", they can specify fault-tolerant systems, where bad behavior cannot be banished. Use of deontic logic allows one to specify which corrective action should be taken to ameliorate the result of a bad system behavior. Their deontic logic is based on a modal action logic, similar to dynamic logic. [WMW89] distinguish integrity constraints that are deontic in nature. They maintain that a database should be able to represent a violation of a norm as such and not just as another fact. This leads to deontic logic for database integrity constraints; their deontic logic too is based on modal action logic. Electronic contracting has been analyzed with speech act theory and deontic logic. Office documents may have one of several illocutionary forces. McCarthy's Elephant 2000 is a speech act based transaction language that is directed to such contexts. The logic here could be an illocutionary logic, but particular illocutionary forces could be formalized more simply either with operators that establish deontic modalities or with these modalities themselves. Weigand [We93] addresses the Environment of Discourse (EoD) of an information system, modeled graphically by a Communications Structure Diagram (CSD), which models patterns of speech acts and the material actions related to them. A CSD specification supports the use of deontic operators. Deontic rules are parts of "contracts" stating the obligations and permissions of each partner. The communication structure of a domain is decomposed into several contracts (each a set of related speech acts), which gives the advantages of object-oriented analysis since contracts are referenced as complex objects and can be generalized and specialized. We intend to model user interfaces (cf. the User Interface Agents of the Goddard AGENTS model) with the same formalisms we use for other parts of agent systems. Temporal formalisms have already been used for interfaces [JH94], and the other formalisms are similarly applicable. Indeed, our various formalisms generally were first applied to humans, who appear at the other side of the interface from agents. We have concentrated so far on agent communication. We turn briefly to how content and local agent computation relate to communication. To avoid intractably complex specifications, we intend to keep specifications of abstract data types and operations on them, as these interact with communication, at a high level. Philosophically, speech acts are bound up with the notion of intention, as are the actions we perform in general and plans. The broader issue is agent rationality, as discussed, for example, by Bratman [Br87], who, with his colleagues at CSLI, has had significant influence on the agent research community. Plans will be represented with the formal resources we have already mentioned. We have used a modified process algebra to represent plans [Es96], but other means may prove useful. Moore [Mo85] presents an integrated theory of knowledge and action that involves epistemic modalities and constructs similar to the modalities of dynamic logic. Shared content in an agent system relates to knowledge sharing, usually considered to depend on commitment to a common ontology. In the knowledge-sharing community [Gr93], an ontology is an explicit specification of a conceptualization, where a conceptualization is an abstract view of the world used for some purpose and includes the objects, concepts, and other entities assumed in the domain in question and the relationships among them. Common ontologies are used to describe ontological commitments for a set of agents so they can communicate about a domain without the need to share a knowledge base or theory. The most extensive project in this area is the ARPA Knowledge Sharing Effort, which has developed an agent-communication language, KQML, for knowledge sharing and a Knowledge Interchange Format (KIF). Ontolingua [Gr92], intended for ontology sharing, extends KIF with standard primitives for defining classes and relations and organizing knowledge in object-centered hierarchies. Ontologies for knowledge sharing are domain-specific ontologies. General ontology is a branch of philosophy that has been very active recently. A formal ontology in the general sense is a theory of a priori distinctions among the meta-level categories used to model the world and explicates the notions of part and whole and the notion of connected parts. As such, general ontology has been investigated by AI researchers [Gu94] and by researchers in natural-language understanding, who formulate an "upper' ontology not directly related to the lexicon. General ontology has also been used in software engineering to model both the real world and information systems. We are completing a project to exploit general ontology in AI and software engineering. We model ontological aspects with feature terms and animate the resulting specifications using the logic programming language LIFE, which implements feature terms ("(-terms") [GE95]. For specifying the content communicated in agent systems, we intend to proceed in the tradition of general ontology since, compared with domain-specific ontologies, this gives greater flexibility, avoids design-level details, and gives more widely applicable results. The reasoning performed by agents, especially as members of a community of agents, is significant even at the level of specification since the knowledge and action of an agent depends not only on what is communicated to it but also on what the agent can infer from what it receives. Default reasoning, by which we accept certain conclusions (roughly, what is normal) in the absence of conflicting information, is pervasive in communication among reasoning agents. Default reasoning is a form of nonmonotonic reasoning, where previous conclusions may become invalid when we add new premises. Several systems of default or nonmonotonic logic, some based on epistemic logic, have been published. The philosopher Kenney, following Aristotle, describes "practical inference" as reasoning about what is required rather than (as with classical logic) what is true. The logic of practical inference is something like the dual of classical logic (e.g., modus ponens and affirming the consequent exchange roles). Although practical inference has not been noticed by AI researchers, it has obvious connections with agent actions and plans, and with deontic and other logics. Philosophers have also considered practical reasoning in a broader sense, encompassing actions and their preconditions and effects. We intend to address agent reasoning in our specifications to the extent that this is needed for coherent specifications. We anticipate that default and some other nonmonotonic reasoning will be significant. Practical inference could be invoked to subsume agent behavior under patterns that relate to the inferences drawn. In any case, agent reasoning can assume still more importance when we move beyond the specification level. Implementations of agent systems should address default reasoning and communication and practical inference in collaborative action if these systems are to attain the functionality desired of them.

Plan of Work

The following table outlines the months in which various activities will be pursued. It is assumed that month 1 will be August 1996. The first two years will be primarily occupied with specification methodology, including selecting and (if necessary) refining appropriate formalisms. This includes developing a course on formalisms and specification techniques for agent systems. The course will first be given as an independent study course to select students. It will then be offered once a year for the duration of this effort as a special topics course. Various applications of agents at Goddard will be specified so that ideas may be tried out. A description of the Goddard AGENTS model will be produced using the selected formalisms; this will ensure that the specification techniques do not drift from the vision of the Goddard personnel. The major deliverable from the first two years will be a user's document presenting the formalisms and explaining the specification methodology. This document will have numerous appendices where formalisms are expounded rigorously Evaluation and revision of this document will extend into the third and final year. The third year of the proposed effort will extend the insight and results gained with agent specification to agent languages and systems. Semantics will be produced for certain constructs in the Goddard agent communication language. Several features of agent systems will be designed. This will involve designing data structures, algorithms, inference methods, or protocols that could be implemented in software. The features will not be selected until the effort is well underway so that experience may result in informed choice. Some of the possible features are agent communication, knowledge sharing and ontologies, collaborative planning, and collaborative reasoning.

Months

Activities

1/5 Offer independent study course. Develop background

1/3 Familiarize with the general Goddard activities with agents

4/6 Specification of a small application at Goddard

6/10 Teach the course for the first time

7/12 Specification of a larger application. Prepare preliminary user's document

11/12 Construct a comprehensive view of the AGENTS model and its applications.

13/24 Specifications of tractable but significant parts of agent applications at Goddard. Description of AGENTS model in our formalisms.

13/18 Prepare first draft of user's document

19/24 Prepare the final draft of the user's document

25/27 Evaluation of the user's document

28/30 Revision of the user's document

18/24 Background on agent communication language and its development at Goddard

25/36 Development of the semantics of key constructs in the agent communication language. Design of certain features of agent systems.

The following table gives the check points for the proposed effort and what is to be delivered and evaluated at each There is a check at the end of the first year and then at the end of each six-month period until the end of the effort.

Month

Items Checked

12- Example specifications. Preliminary user's document.

18- First draft of the user's document. Specifications of agent applications. Preliminary description of the AGENTS model.

24- Final draft of the user's document. More specifications of agent applications. Final description of the AGENTS model.

30- Revised user's document. Semantics of some constructs in the agent communication language. Preliminary designs for agent-system features.

36- Semantics for additional language constructs. Final designs for agent-system features.

All deliverables will be evaluated by the Goddard personnel. The user's document, in its various versions, will be evaluated on its usability by users (including those with little background), its technical soundness, its completeness, its pedagogical soundness, and the utility of the specifications produced in conformity with it. Specifications will be evaluated on their clarity, completeness, lack of ambiguity, utility for supporting design, and ability to reveal logical connections. The description of the AGENTS model in the selected formalisms will be evaluated on its faithfulness and on the criteria applied to specifications. Finally, the semantics of language constructs and designs for agent-system features will be evaluated on the same criteria as specifications except that utility for supporting design will be replaced by utility for supporting implementation. The proposed effort will employ two graduate and two undergraduate research assistants throughout its duration. All research assistants will be African-American and will be employed for one year (their final year) barring exceptional circumstances. All will be expected to take the planned course on agent formalisms in their first semester of employment unless they have already taken it. The group will meet weekly and each student will be individually advised at least once a week. Advising will fall under the mentoring program of the Computer Science Department so will cover all aspects of academic life. Graduate students will be encouraged to take the thesis option for their masters degrees; if this is not feasible, they will be expected to take the project option. Emphasis will be on completing their degrees on time and on developing research and communication skills.

Bibliography

[Aq84] L. Aqvist, "Deontic Logic," in D.M. Gabbay and F. Guenther (eds.), Handbook of Philosophical Logic, Vol. II. Boston: Reidel, 1984, pp. 605-714.

[Br87] M.E. Bratman, Intention, Plans, and Practical Reason. Cambridge, MA: Harvard Univ. Press, 1987.

[Es96] Esterline, A.C., "Generating Constraints in an Executable Temporal Logic from Terms in a Plan Algebra," submitted to the Journal of Symbolic Computation.

[FV86] R. Fagin and M.Y. Vardi, "Knowledge and Implicit Knowledge in a Distributed Environment," in J.Y. Halpern (ed.), Proc 1st Conf. on Theoretical Aspects of Knowledge, Los Altos, CA: Morgan Kaufmann, 1986, pp. 187-206.

[GE95] Goldstein, D. and Esterline, A.C., "Methods for Building Sharable Ontologies," IJCAI Workshop on Basic Ontological Issues in Knowledge Sharing, Montreal, 1995.

[Gr92] T. Gruber, "Ontolingua: A Mechanism to Support Portable Ontologies," Tech. Rep., Knowledge Systems Lab., Stanford Univ., 1992.

[Gr93] T. Gruber, "Toward Principles for the Design of Ontologies Used for Knowledge Sharing," Int. Workshop on Formal Ontology in Conceptual Analysis and Knowledge Representation, Padua, 1993.

[Gu94] M. Guarino, "The Ontological Level," in R. Casati, B. Smith, and G. White (eds.), Philosophy and the Cognitive Sciences. Vienna: Hoelder-Pichler-Tempsky Verlag, 1994, pp. 443-457.

[HM90] J.Y. Halpern and Y.O. Moses, "Knowledge and Common Knowledge in a Distributed Environment," J. ACM 37 (1990), pp. 549-587.

[HZ87] J.Y. Halpern and L.D. Zuck, "A Little Knowledge Goes a Big Way: Simple Knowledge-Based Derivations and Correctness Proofs," Proc. 6th ACM Symp. on Principles of Distributed Systems, 1987, pp. 269-280.

[JH94] C. Johnson and M. Harrison (eds.), "Software Engineering of Human Computer Interaction: Papers from a Workshop on Formal Methods for the Design of Interactive Systems," ACM SIGCHI Bulletin 26 (1994), pp. 46-73.

[KM87] S. Khosla and T.S.E. Maibaum, "The Prescription and Description of State Based Systems," in B. Banieqbal, H. Barringer, and A. Pnueli (eds.), Temporal Logic of Specifications. Berlin: Springer-Verlag, 1987, pp. 243-294.

[Mo85] R.C. Moore, "A Formal Theory of Knowledge and Action," in J.R. Hobbs and R.C. Moore (eds.), Formal Theories of the Commonsense World, Norwood, NJ: Ablex, 1985, pp. 319-358.

[MV95] J.-J.C. Meyer and W. van der Hoek, Epistemic Logic for AI and Computer Science, Cambridge: Cambridge Univ. Press, 1995.

[MW93] J.-J.C. Meyer and R.J. Wieringa (eds.), Deontic Logic in Computer Science, Chichester, U.K.: Wiley, 1993.

[SC95] I.A. Smith and P.R. Cohen, "Toward a Semantics for a Speech Act Based Agent Communication Language," in CIKM'95 Intelligent Information Agents Workshop, Baltimore, MD, 1995.

[Se69] J.R. Searle, Speech Acts. Cambridge: Cambridge Univ. Press, 1969.

[Sh93] Y. Shoham, "Agent-Oriented Programming," Artif. Intell. 60 (1993), pp. 51-92.

[SV85] J.R. Searle and D. Vanderveken, Foundations of Illocutionary Logic, Cambridge: Cambridge Univ. Press, 1985.

[We93] H. Weigand, "Deontic Aspects of Communication," in [MW93].

[WMW89] R.J. Wieringa, J.-J.C. Meyer, and W. Weigand, "Specifying Dynamic and Deontic Integrity Constraints," Data and Knowledge Engineering 4 (1989), pp. 157-189.