Name
Abstract | ||
|---|---|---|
The paper presents a proposal for the specification and verification of systems of communicating agents in a tem- poral logic. The proposal is based on a social approach to agent communication, where communication is described in terms of changes to the social state, and interaction protocols are defined by a set of temporal constraints, which specify the effects and preconditions of the communicative actions on the social state. The paper addresses the problem of combining protocols to define new more specialized protocols and exploits this idea in the specification of clinical guidelines. I. INTRODUCTION Agent technology has been rapidly developing in the last decade to answer the needs for new conceptual tools for modelling and developing complex software systems and it has given rise to a large amount of literature (6). Autonomous agents can communicate, cooperate and negotiate using com- monly agreed communication languages (ACLs) and proto- cols. The issue of interoperability has lead to the development of standardized agent communication languages, including KQML (21) and FIPA-ACL (4). One of the central issues in the field concerns the specification of conversation policies, which govern the communication between software agents in an agent communication language (ACL). Conversation policies (or interaction protocols) define stereotypical interactions in which ACL messages are used to achieve communicative goals. The specification of interaction protocols has been tradi- tionally done by making use of finite state machines, but the transition net approach has been soon recognized to be too rigid to allow for the flexibility needed in agent communi- cation (24), (16). For these reasons, several proposals have been put forward to address the problem of specifying (and verifying) agent protocols in a flexible way. One of the most promising approaches to agent communication, first proposed by Singh (28), is the social approach (1), (8), (18), (24). In the social approach, communicative actions affect the "social state" of the system, rather than the internal (mental) states of the agents. The social state records social facts, like the permissions and the commitments of the agents. In this paper we present a temporal approach to the specifi- cation and verification of interaction protocols among agents. Temporal logics are extensively used in the area of reasoning about actions and planning (2), (14), (11), (26), (3), and, in particular, they have been used in the specification and in the verification of systems of communicating agents. In (34), (22) agents are written in MABLE, an imperative programming lan- guage, and the formal claims about the system are expressed using a quantified linear time temporal BDI logic and can be automatically verified by making use of the SPIN model checker. Guerin in (17) defines an agent communication frame- work which gives agent communication a grounded declarative semantics. In such a framework, temporal logic is used for formalizing temporal properties of the system. Our theory for reasoning about communicative actions is based on the Dynamic Linear Time Temporal Logic (DLTL) (19), which extends LTL by strengthening the until operator by indexing it with the regular programs of dynamic logic. As a difference with (34) we adopt a social approach to agent communication. The dynamics of the system emerges from the interactions of the agents, which must respect permissions and commitments (if they are compliant with the protocol). The social approach allows a high level specification of the protocol, and it is well suited for dealing with "open" multi-agent systems, where the history of communications is observable, but the internal states of the single agents may not be observable. The paper provides an overview of the approach developed in (12), (13), and describes the different kinds of verification problems which can be addressed, which can be formalized either as validity or as satisfiability problems in DLTL. These verification tasks can be automated by making use of B¨ uchi |
Year | Venue | Keywords |
|---|---|---|
2005 | WOA | indexation,satisfiability,software agent,col,dynamic logic,software systems,autonomous agent,finite state machine,temporal logic |
Field | DocType | Citations |
Software engineering,Computer science,Exploit,Theoretical computer science,Social identity approach | Conference | 1 |
PageRank | References | Authors |
0.38 | 28 | 5 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Laura Giordano | 1 | 115 | 16.64 |
| Alberto Martelli | 2 | 585 | 44.25 |
| Paolo Terenziani | 3 | 924 | 112.83 |
| A. Bottrighi | 4 | 247 | 24.69 |
| Stefania Montani | 5 | 901 | 81.42 |