@article{AlbGavLam05-TPLP-IJ, key = 001, author = {Marco Alberti And Marco Gavanelli And Evelina Lamma And Paola Mello And Michela Milano}, title = {A {CHR}-based implementation of known arc-consistency}, journal = {Theory and Practice of Logic Programming}, year = 2005, volume = 5, number = {4/5}, pages = {419-440}, month = jul, http = {http://journals.cambridge.org/action/displayIssue?jid=TLP&volumeId=5&issueId=4-5}, doi = {http://dx.doi.org/10.1017/S147106840500236X}, abstract = { In classical CLP(FD) systems, domains of variables are completely known at the beginning of the constraint propagation process. However, in systems interacting with an external environment, this assumption may lead to waste of computation time, or even to obsolescence of the acquired data at the time of use. For such cases, the Interactive Constraint Satisfaction Problem (ICSP) model has been proposed as an extension of the CSP model, to make it possible to start constraint propagation even when domains are not fully known, performing acquisition of domain elements only when necessary and without the need to restart propagation after every acquisition. In this paper, we present a two sorted CLP language to express and solve ICSPs, and its implementation in the Constraint Handling Rules (CHR) language, a declarative language particularly suitable for high level implementation of constraint solvers.}, issn = {1471-0684}, note = {IF: 1.372} }
@inproceedings{AlbGavLam05-IJCAI-IC, author = {Marco Alberti and Marco Gavanelli and Evelina Lamma and Paola Mello and Paolo Torroni}, title = {Abduction with hypotheses confirmation}, booktitle = {IJCAI-05 Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence}, year = {2005}, editor = {Fausto Giunchiglia}, pages = {1545--1546}, publisher = {Professional Book Center}, address = {USA}, isbn = {0-938075-93-4}, url = {http://www.ing.unife.it/docenti/MarcoGavanelli/publications/poster-ijcai05.ppt}, pdf = {http://ijcai.org/papers/post-0385.pdf} }
@article{AlbGavLam05-AIIA-IC, author = {Marco Alberti and Marco Gavanelli and Evelina Lamma and Paola Mello and Paolo Torroni}, title = {The \textit{S}{CIFF} abductive proof-procedure}, booktitle = {AI*IA 2005: Advances in Artificial Intelligence: 9th Congress of the Italian Association for Artificial Intelligence, Milan, Italy, September 21-32, 2005. Proceedings}, year = {2005}, editor = {Stefania Bandini and Sara Manzoni}, journal = {Lecture Notes in Artificial Intelligence}, address = {Berlin}, publisher = {Springer Verlag}, pages = {135-147}, volume = {3673}, issn = {0302-9743}, abstract = {We propose an operational framework which builds on the classical understanding of abductive reasoning in logic programming, and extends it in several directions. The new features include the ability to reason with a dynamic knowledge base, where new facts can be added anytime, the ability to generate expectations about such new facts occurring in the future (forecasting), and the process of confirmation/disconfirmation of such expectations.}, note = {IF: 0.302} }
@article{AlbCheGav05-GC-IW, author = {Marco Alberti and Federico Chesani and Marco Gavanelli and Evelina Lamma and Paola Mello and Paolo Torroni}, title = {The {SOCS} Computational Logic Approach to the Specification and Verification of Agent Societies}, booktitle = {Global Computing: {IST/FET} International Workshop, GC 2004 Rovereto, Italy, March 9-12, 2004 Revised Selected Papers}, year = {2005}, issn = {0302-9743}, month = feb, editor = {Corrado Priami and Paola Quaglia}, journal = {Lecture Notes in Computer Science}, doi = {10.1007/b103251}, publisher = {Springer Verlag}, address = {Berlin, Germany}, abstract = {This article summarises part of the work done during the first two years of the SOCS project, with respect to the task of modelling interaction amongst CL-based agents. It describes the SOCS social model: an agent interaction specification and verification framework equipped with a declarative and operational semantics, expressed in terms of abduction. The operational counterpart of the proposed framework has been implemented and integrated in SOCS-SI, a tool that can be used for on-the-fly verification of agent compliance with respect to specified protocols.}, pages = {314 - 339}, volume = 3267, note = {IF: 0.402} }
@article{AlbChe05-IA-NJ, author = {Marco Alberti and Federico Chesani}, title = {The computational behaviour of the {SCIFF} abductive proof procedure and the {SOCS-SI} system}, journal = {Intelligenza Artificiale}, year = 2005, volume = {II}, number = 3, pages = {45--51}, month = {September}, issn = {1724-8035}, abstract = {The high computational cost of abduction has limited the application of this powerful and expressive formalism to practical cases. SCIFF is an abductive proof procedure used for verifying the compliance of agent behaviour to interaction protocols in multi-agent systems; SCIFF has been integrated in SOCS-SI, a system able to observe the agent interaction, pass it to SCIFF for the reasoning process and to display in a GUI the results of the SCIFF computation. In order to assess the applicability of SCIFF and SOCS-SI to practical cases, we have evaluated qualitatively and experimentally (not yet formally) their computational behaviour, concerning limitations and scalability. In this paper we show the results of the analysis.} }
@article{AlbCheGav05-IA-NJ, author = {Marco Alberti and Federico Chesani and Marco Gavanelli and Alessio Guerri and Evelina Lamma and Paola Mello and Paolo Torroni}, title = {Expressing Interaction in Combinatorial Auction through Social Integrity Constraints}, journal = {Intelligenza Artificiale}, year = {2005}, pages = {22--29}, volume = {{II}}, number = {1}, abstract = {Combinatorial Auctions are an attractive application of intelligent agents; their applications are countless and are shown to provide good revenues. On the other hand, one of the issues they raise is the computational complexity of the solving process (the Winner Determination Problem, WDP), that delayed their practical use. Recently, efficient solvers have been applied to the WDP, so the framework starts to be viable. % A second issue, common to many other agent systems, is {\em trust}: in order for an agent system to be used, the users must {\em trust} both their representative and the other agents inhabiting the society: malicious agents must be found, and their violations discovered. The SOCS project addresses such issues, and provided a language, the social integrity constraints, for defining the allowed interaction moves, together with a proof procedure able to detect violations. % In this paper we show how to write a protocol for the combinatorial auctions by using social integrity constraints. In the devised protocol, the auctioneer interacts with an external solver for the winner determination problem.}, issn = {1724-8035}, url = {http://ia.di.uniba.it/} }
@inproceedings{CheCiaMel05-WOA-NW, author = {Federico Chesani and Anna Ciampolini and Paola Mello and Marco Montali and Paolo Torroni and Marco Alberti and Sergio Storari}, title = {Protocol Specification and Verification by Using Computational Logic.}, editor = {Flavio Corradini and Flavio De Paoli and Emanuela Merelli and Andrea Omicini}, booktitle = {WOA 2005: Dagli Oggetti agli Agenti. 6th AI*IA/TABOO Joint Workshop "From Objects to Agents": Simulation and Formal Analysis of Complex Systems, 14-16 November 2005, Camerino, MC, Italy}, publisher = {Pitagora Editrice Bologna}, year = {2005}, isbn = {88-371-1590-3}, pages = {184-192}, ee = {http://lia.deis.unibo.it/books/woa2005/papers/26.pdf}, bibsource = {0DBLP, http://dblp.uni-trier.de}, abstract = { The aim of this paper is to report on some preliminary results obtained in the context of the MASSIVE research project (http://www.di.unito.it/massive/) relating the formal specification and verification of protocols in some different application field. A protocol is a way to express the right behavior of entities involved in a (possibly complex and distributed) process. The formalism to be used for protocol description should be as intuitive as possible, but it should be also formally defined, in order to allow formal checks both on the features of the protocol itself (e.g. termination), and also on the execution of it. To this purpose, we will show some results obtained by exploiting the SOCS-SI logic-based framework for the specification and the verification of protocols in various applicative fields such as electronic commerce, medicine and e-learning. We will also present a new graphical notation to express medical guidelines, which could be automatically translated into the SOCS formalism.} }
@phdthesis{Alb05-PT, author = {Marco Alberti}, title = {A Computational Logic-based System for Specification and Verification of Agent Interaction}, school = {University of Ferrara}, year = 2005, month = {March}, note = {Available at \url{http://docente.unife.it/marco.alberti/alberti-phd-final.pdf/at_download/file}} }
This file was generated by bibtex2html 1.98.