Fundamenta Informaticae - Volume 105, issue 1-2

Authors: Gavanelli, Marco | Riguzzi, Fabrizio | Pettorossi, Alberto

Article Type: Other

DOI: 10.3233/FI-2010-355

Citation: Fundamenta Informaticae, vol. 105, no. 1-2, pp. v-vi, 2010

Authors: Costantini, Stefania | Formisano, Andrea | Petturiti, Davide

Article Type: Research Article

Abstract: In previous work we have proposed an extension to ASP (Answer Set Programming), called RASP, standing for ASP with Resources. RASP supports declarative reasoning on production and consumption of (amounts of) resources. The approach combines answer set semantics with quantitative reasoning and relies on an algebraic structure to support computations and comparisons of amounts. The RASP framework provides some form of preference reasoning on resources usage. In this paper, we go further in this direction by introducing expressive constructs for supporting complex preferences specification on aggregate resources. We present a refinement of the semantics of RASP so as to take …into account the new constructs. For all the extensions, we provide an encoding into plain ASP. We prove that the complexity of establishing the existence of an answer set, in such an enriched framework, remains NP-complete as in ASP. Finally, we report on raspberry, a prototypical implementation of RASP. This tool consists of a compiler that, given a ground RASP program, produces a pure ASP encoding suitable to be processed by commonly available ASP-solvers. Show more

Keywords: Answer set programming, quantitative reasoning, preferences, language extensions

DOI: 10.3233/FI-2010-356

Citation: Fundamenta Informaticae, vol. 105, no. 1-2, pp. 1-33, 2010

Authors: Ricca, Francesco | Dimasi, Antonella | Grasso, Giovanni | Ielpa, Salvatore Maria | Iiritano, Salvatore | Manna, Marco | Leone, Nicola

Article Type: Research Article

Abstract: In this paper we present a successful application of logic programming for e-tourism: the iTravel system. The system exploits two technologies that are based on the state-of-the-art computational logic system DLV: (i) a system for ontology representation and reasoning, called OntoDLV; and, (ii) H$\dotlessi$LεX a semantic information-extraction tool. The core of iTravel is an ontology which models the domain of tourism offers. The ontology is automatically populated by extracting the information contained in the tourism leaflets produced by tour operators. A set of specifically devised logic programs is used to reason on the information contained in the ontology for selecting …the holiday packages that best fit the customer needs. An intuitive web-based user interface eases the task of interacting with the system for both the customers and the operators of a travel agency. Show more

Keywords: Answer Set Programming, ASP, E-Tourism, Knowledge Representation and Reasoning, Information Extraction

DOI: 10.3233/FI-2010-357

Citation: Fundamenta Informaticae, vol. 105, no. 1-2, pp. 35-55, 2010

Authors: Bistarelli, Stefano | Gosti, Giorgio

Article Type: Research Article

Abstract: Constraint solving problems (CSPs) are the formalization of a large range of problems that emerge from computer science. The solving methodology described here is based on the naming game. The two main features that distinguish this methodology from most distributed constraint solving problem (DCSPs) methods are: the system can react to small instance changes, and it does not require pre-agreed agent/variable ordering. The naming game was introduced to represent N agents that have to bootstrap an agreement on a name to give to an object. The agents do not have a hierarchy, and use a minimal protocol. Still they converge …to a consistent state by using a distributed strategy. For this reason, the naming game can be used to untangle DCSPs. It was shown that a distributed system of uniform finite state machines does not solve the ring ordering problem in all the algorithm executions. Our algorithm is a distributed uniform system of agents able to perform random decisions when presented with equivalent alternatives. We show that this algorithm solves the ring ordering problem with a probability one. Show more

DOI: 10.3233/FI-2010-358

Citation: Fundamenta Informaticae, vol. 105, no. 1-2, pp. 57-78, 2010

Authors: Dovier, Agostino | Formisano, Andrea | Pontelli, Enrico

Article Type: Research Article

Abstract: This paper explores the use of Constraint Logic Programming (CLP) as a platform for experimenting with planning problems in the presence of multiple interacting agents. The paper develops a novel constraint-based action language, ℬMAP , that enables the declarative description of large classes of multi-agent and multi-valued domains. ℬMAP supports several complex features, including combined effects of concurrent and interacting actions, concurrency control, and delayed effects. The paper presents a mapping of ℬMAP theories to CLP and it demonstrates the effectiveness of an implementation in SICStus Prolog on several benchmark problems. The effort is an evolution of previous …research on using CLP for single-agent domains, demonstrating the flexibility of CLP technology to handle the more complex issues of multi-agency and concurrency. Show more

Keywords: Action Description Languages, Multi Agent Planning, Constraint Logic Programming

DOI: 10.3233/FI-2010-359

Citation: Fundamenta Informaticae, vol. 105, no. 1-2, pp. 79-103, 2010

Authors: Campagna, Dario | De Rosa, Christian | Dovier, Agostino | Montanari, Angelo | Piazza, Carla

Article Type: Research Article

Abstract: Product configuration systems are an emerging software technology that supports companies in deploying mass customization strategies. In this paper, we describe a CLP-based reasoning engine that we developed for a commercial configuration system. We first illustrate the advantages of the CLP approach to product configuration over other ones. Then, we describe the actual encoding of the considered product configuration problem as a constraint satisfaction problem. We devote a special attention to the key issues of constraint propagation and optimization as well as to the relevant process of assignment revision. A comparison with existing systems for product configuration concludes the paper.

DOI: 10.3233/FI-2010-360

Citation: Fundamenta Informaticae, vol. 105, no. 1-2, pp. 105-133, 2010

Authors: Chesani, Federico | Mello, Paola | Montali, Marco | Torroni, Paolo

Article Type: Research Article

Abstract: Since its introduction, the Event Calculus (ℰ𝒞) has been recognized for being an excellent framework to reason about time and events, and it has been applied to a variety of domains. However, its formalization inside logic-based frameworks has been mainly based on backward, goal-oriented reasoning: given a narrative (also called execution trace) and a goal, logic-based formalizations of ℰ𝒞 focus on proving the goal, i.e., establishing if a property (called fluent) holds. These approaches are therefore unsuitable in dynamic environments, where the narrative typically evolves over time: indeed, each occurrence of a new event requires to restart the reasoning process …from scratch. Ad-hoc, procedural methods and implementations have been then proposed to overcome this issue. However, they lack a strong formal basis and cannot guarantee formal properties. As a consequence, the applicability of ℰ𝒞 has been somehow limited in large application domains such as run-time monitoring and event processing, which require at the same time reactivity features as well as formal properties to provide guarantees about the computed response. We overcome the highlighted issues by proposing a Reactive and logic-based axiomatization of ℰ𝒞, called ℛℰ𝒞, on top of the SCIFF Abductive Logic Programming framework. Our solution exhibits the features of a reactive verification facility, while maintaining a solid formal background. Show more

Keywords: Event Calculus, Reactive Reasoning, Monitoring, Computational Logic, Abductive Logic Programming

DOI: 10.3233/FI-2010-361

Citation: Fundamenta Informaticae, vol. 105, no. 1-2, pp. 135-161, 2010

Authors: Nicolini, Enrica | Ringeissen, Christophe | Rusinowitch, Michael

Article Type: Research Article

Abstract: We present some decidability results for the universal fragment of theories modeling data structures and endowed with arithmetic constraints. More precisely, all the theories taken into account extend a theory that constrains the function symbol for the successor. A general decision procedure is obtained, by devising an appropriate calculus based on superposition. Moreover, we derive a decidability result for the combination of the considered theories for data structures and some fragments of arithmetic by applying a general combination schema for theories sharing a common subtheory. The effectiveness of the resulting algorithm is ensured by using the proposed calculus and a …careful adaptation of standard methods for reasoning about arithmetic, such as Gauss elimination, Fourier-Motzkin elimination and Groebner bases computation. Show more

Keywords: Satisfiability Procedure, Combination, Equational Reasoning, Union of Non-Disjoint Theories, Integer Offsets

DOI: 10.3233/FI-2010-362

Citation: Fundamenta Informaticae, vol. 105, no. 1-2, pp. 163-187, 2010

Authors: Faella, Marco | Napoli, Margherita | Parente, Mimmo

Article Type: Research Article

Abstract: Recently, temporal logics such as μ-calculus and Computational Tree Logic, CTL, augmented with graded modalities have received attention from the scientific community, both from a theoretical side and from an applicative perspective. In both these settings, graded modalities enrich the universal and existential quantifiers with the capability to express the concept of at least k or all but k, for a non-negative integer k. Both μ-calculus and CTL naturally apply as specification languages for closed systems: in this paper, we study how graded modalities may affect specification languages for open systems. We extend the Alternating-time Temporal Logic (ATL) introduced by …Alur et al., that is a derivative of CTL interpreted on game structures, rather than transition systems. We solve the model-checking problem in the concurrent and turn-based settings, proving its PTIME-completeness. We present, and compare with each other, two different semantics: the first seems suitable to off-line synthesis applications while the second may find application in the verification of fault-tolerant controllers. We also study the case where players can only employ memoryless strategies, showing that also in this case the model-checking problem is in PTIME. Show more

DOI: 10.3233/FI-2010-363

Citation: Fundamenta Informaticae, vol. 105, no. 1-2, pp. 189-210, 2010