1,721,014 research outputs found
Symbolic model checking for multi-agent systems
No full textMulti-Agent Systems are increasingly complex, and the problem of their verification and validation is acquiring increasing importance. In this paper we show how a well known and effective verification technique, symbolic model checking, can be generalized to deal with Multi-Agent Systems. Our approach is fully amenable to the reuse of data structures used in symbolic model checking, Binary Decision Diagrams in particular, to deal with extremely large state spaces. A preliminary implementation of the approach in the NuMAS system shows promising result
Formal specification of Beliefs in Multi-Agents Systems
No full textThe goal of this paper is to present a logical framework for the formalization of agents` mutual beliefs in a Multi Agent system. The approach is based on a combination of extensional specifications of beliefs and context-based (finite) presentation of the specifications by employing a particular class of Multi Context systems. The extensional specification provides a set-theoretic characterization of beliefs in terms of sets closed under certain conditions. Its finite presentation is provided by using as constructors inference rules inside a Multi Context system. The resulting framework allows for capturing many relevant cases of real (non omniscient) agents, which are very common in Multi Agent scenarios embedded in real world environments. In order to substantiate this claim, two Multi Agent scenarios are formally specified in detail in the specification framework
Model Checking Multiagent Systems
No full textModel checking is a very successful technique which has been applied in the design and verification of finite state concurrent reactive processes. In this paper we show how this technique can be lifted to be applicable to multiagent systems. Our approach allows us to reuse the technology and tools developed in model checking, to design and verify multiagent systems in a modular and incremental way, and also to have a very efficient model checking algorith
Model Checking Multiagent Systems (Extend Abstract)
No full text) Massimo Benerecetti 1 , Fausto Giunchiglia 1;2 , Luciano Serafini 2 1 DISA - University of Trento, Via Inama 13, 38050 Trento, Italy 2 IRST - Istituto Trentino di Cultura, 38050 Povo, Trento, Italy [email protected] ffausto,[email protected] Abstract. Model checking is a very successful technique which has been applied in the design and verification of finite state concurrent reactive processes. In this paper we show how this technique can be lifted to be applicable to multiagent systems. Our approach allows us to reuse the technology and tools developed in model checking, to design and verify multiagent systems in a modular and incremental way, and also to have a very efficient model checking algorithm. 1 Introduction Model checking is a very successful automatic technique which has been devised for the design and verification of finite state reactive systems, e.g., sequential circuit designs, communication protocols, and safety critical control systems (see, e.g., [2])..
Multiagent Systems Verification via Model Checking
No full textModel checking is a very successful technique which has been applied in the design and verification of finite state concurrent reactive processes. In this paper we show how this technique can be lifted to be applicable to multiagent systems. Our approach allows us to reuse the technology and tools developed in model checking, to design and verify multiagent systems in a modular and incremental way, and also to have a very efficient model checking algorith
A Multi Context Approach to Belief Report
No full textOne of the most interesting puzzles in formalizing belief contexts is the fact that many belief reports can be given both an opaque and a transparent reading. A traditional explanation is that the two readings are related to the failure and success of the `principle of substitutivity` respectively, and this in turm is explained with the `de re/de dicto` distinction. We propose an alternative analysis, based on the idea that another agent`s beliefs can just be quoted (preserving opaqueness) or translated into the reporter`s language (allowing transparency). We show that MultiContext systems allow the formalization of these two phenomena at the same time, thanks to their multi-language featur
Context-Based Formal Specification of Multi-Agent Systems
No full textThe formalization of agents attitudes, and belief in particular, has been investigated in the past by the authors of this paper, along two different but related streams. Giunchiglia and Giunchiglia investigate the properties of contexts for the formal specification of agents mutual beliefs, combining extensional specification with (finite) presentation by means of contexts. Cimatti and Serafini address the representational and implementational implications of the use of contexts for representing propositional attitudes by tackling a paradigmatic case study. The goal of this paper is to show how these two streams are actually complementary. I.e. how the methodology proposed in the former ca be successfully applied to formally specify the case study discussed in the latter. In order to achieve this goal, the formal framework is extended to take into account some relevant aspects of the case study, the specification of which in then worked out in detai
An Algorithm for Semantic Coordination
No full textThe problem of finding an agreement on the meaning of heterogeneous semantic models is one of the key issues in the development of the Semantic Web. In this paper, we propose (i) a general algorithm which implements a new approach, called CTXMATCH, for discovering (semantic) relationships across distinct and autonomous generic structures and (ii) a specific algorithm specializing the algorithm to the discovering of mappings across \emph{hierarchical classifications. This approach shifts the problem of semantic coordination from the problem of computing linguistic and/or structural similarities between semantic-based structures (what most other proposed approaches do), to the problem of deducing relations between sets of logical formulas that represent the meaning of concepts belonging to different structure
- …
