Intelligenza Artificiale

In this paper we focus on proof methods and theorem proving for normal conditional logics, by describing nested sequent calculi as well as a theorem prover for them. We first present some nested sequent calculi, recently introduced, for the basic conditional logic CK and some of its significant extensions with axioms ID, MP and CEM. We also describe a calculus for the flat fragment of the conditional logic CK+CSO+ID, which corresponds to Kraus, Lehmann and Magidor’s cumulative logic C. The calculi are internal, cut-free and analytic. Next, we describe NESCOND, a Prolog implementation of these calculi in the style of leanT^AP. We finally present an experimental comparison between our theorem prover NESCOND and other known theorem provers for conditional logics. Our tests show that the performances of NESCOND are promising and in all cases better, with the only exception of systems including CEM, than those ones of the other provers. The program NESCOND, as well as all the Prolog source files, are available at http://www.di.unito.it/~pozzato/nescond/.

We propose an approach for designing, formalizing and implementing, on top of existing MultiAgent Systems and without interfering with them, sentinels that detect errors in fail-uncontrolled multiagent systems, and controllers that identify particular situations in ambient intelligence (AmI) systems. The formalism we use for representing the expected patterns of actions is that of trace expressions extended with features for dealing with exceptions, timeouts, and their handlers. In this paper we provide the syntax and semantics of the extended trace expressions formalism and examples of their use, in the different contexts of fail-uncontrolled and AmI systems.

This paper presents the key aspects of a proposed formalization of JADE agents and multi-agent systems based on transition systems. Such a formalization is meant to be useful to describe and clarify how JADE multi-agent systems work and to provide a theoretical instrument to validate and analyze the semantics of JADE agents. This is needed to decouple agent-oriented and object-oriented parts of an agent design and to avoid misunderstandings on the semantics of JADE agents. The chosen approach is to define a structural operational semantics for Java programs written using JADE, and the proposed formalization consists in two parts: the first identifies and defines the main entities that together compose a JADE multi-agent system; the second provides the transition system and rewriting rules. The paper terminates with two explanatory examples of the usage of the transition system. A brief recapitulation of the work concludes the paper.

Pedestrian and crowd simulation is generally focused on operational level decisions, providing the choice of exact steps of pedestrians in a representation of the environment, with the aim of replicating observed patterns of space utilization, trajectories and timings. When relatively large environments are considered, though, tactical level decisions become equally important: in general, multiple paths can be followed to reach a target from an entrance or starting point, and path length might not be the only reasonable criterion. This paper presents a hybrid agent architecture for modeling different types of decisions in a pedestrian simulation system, encompassing a floor-field based operational level (based on a “least effort” principle) and an adaptive tactical level component, provided with a graph-like representation of the envornment, considering both perceived congestion and characteristics of potential paths in the related decision. The model is experimented and evaluated both qualitatively and quantitatively in benchmark scenarios to show its adequacy and expressiveness.

In the last years, we assisted to an increase of healthcare facilities based on the adoption of robotic devices in patients daily life scenarios. In these contexts, the time needed to monitor the patients’ state is a crucial issue in order to limit the occurrence of emergencies. For this reason, the adoption of multi-robot systems (MRSs) allowing to shorten the time to perform critical tasks is growing its applicability in this field. In order to benefit of the adoption of an MRS, an efficient task allocation algorithm is required. The use of market-based mechanisms, such as auctions and negotiations, is often contemplated in MRS for efficient task allocation in domains where tasks are characterized by quality parameters that are related to the way the task is executed depending on the specific robot capabilities. In this work, we propose a market-based negotiation mechanism to allocate tasks to a team of robots, by taking into account end-to-end requirements that the complete allocation should meet in terms of the considered quality parameters. These parameters are considered as goods to be traded by individual robots that negotiate upon their values to meet the end-to-end requirements. In case of successful negotiation, they obtain the task assignment. Robots are endowed with negotiation strategies determining the quality parameter values they offer. These strategies are designed to simulate a stochastic behavior of the market, and they take into account dynamic information related to the current robot state depending on its functioning. We present and discuss the results obtained by adopting the proposed methodology within a simulated healthcare scenario.

Innovation efforts within the Smart Energy domain have been used to build an Internet of Energy. Each and every electrical device and generator are connected, transmitting and receiving data, reacting in real time to events and stimuli that come from other devices and from the grid. This is a scattered network of sensors, actuators, communication nodes, systems control and monitoring applications. The Internet of Things is enabling the development of such new paradigm by the pervasive deployment of distributed smart objects with communication, learning and reasoning capabilities. In this scenario households, buildings, plants become micro-grids where smart devices are able to interact within and across them. In this paper collaboration among smart micro-grids, is modeled, implemented and evaluated as a peer to peer overlay of multi-agent systems, whose emergent behavior is the effective management of green energy produced by photo-voltaic panels.

Users engaging in online social networks provide sparse data about themselves, e.g. by participating in groups to discuss some topics, linking to each other, etc. Such sparse data can be carefully used to build both user and group profiles, automatically. We put forward a multi-agent system that collects and analyses data scattered on an online social network. The analysis aims at characterising both users, by inserting them into categories, and groups, with a set of key words. The user classification technology is an especially devised neural network that extracts relevant characteristics from raw data characterising user behaviour, and then provides for unknown users the most likely category. Thanks to the said classification tool, some online activities performed by a given user that are unusual for such a user are automatically detected. Moreover, according to the user interests, contents inserted on public pages, which the user is unaware of, can be automatically found and suggested.