Vai al contenuto| Home page|

   Ti trovi in: HOME »Programmi, progetti e risultati »I progetti »PRIN - Programmi di ricerca di Rilevante Interesse Nazionale»Programma di ricerca
INIZIO_TESTO_DA_INDICIZZARE

PROGRAMMA DI RICERCA 2005

italiano - english
Unità di Ricerca
Programmi di ricerca simili:
Classificazione scientifico-disciplinare
Classificazione brevettuale
Classificazione geografica
Bibliografia
[ACKM04] G.Alonso,F.Casati,H.Kuno,V.Machiraju. Web Services. Springer, 2004

[Al03a] M.Alberti,A.Ciampolini,M.Gavanelli,E.Lamma,P.Mello,P.Torroni. Logic based semantics for an agent communication language. Int.Work. on Formal Approaches to MAS, 21-36,2003

[Al03b] M.Alberti,A.Ciampolini,M.Gavanelli,E.Lamma,P.Mello,P.Torroni. A Social ACL Semantics by Deontic Constraints. CEEMAS 2003, LNAI 2691, 204-213,2003

[Alo04] G.Alonso. EDBT Tutorial on Web Services, 2004

[Alfebiite] Web site at alfebiite.ee.ic.ac.uk

[AMMR03] E.Astesiano,M.Martelli,V.Mascardi,G.Reggio. A Combination of a Multiview Use-Case Driven Method and Agent-Oriented Techniques, SEKE'03

[B05] M.Baldoni,C.Baroglio,A.Martelli,V.Patti,C.Schifanella. Verifying protocol conformance for logic-based communicating agents. Int.Work. CLIMA-V, LNAI, 2005

[B03] M.Baldoni,C.Baroglio,L.Giordano,A.Martelli,V.Patti. Reasoning about communicating agents in the semantic web. LNCS 2901, 84-98,2003

[B04] M.Baldoni,L.Giordano,A.Martelli,V.Patti. Programming Rational Agents in a Modal Action Logic. Annals of Mathematics and AI, 41(2-4):207-257,2004

[Bacchus98] F.Bacchus,F.Kabanza. Planning for temporally extended goals. Annals of Mathematics and AI, 22:5-27,1998

[BBFL2001] B.Berard,M.Bidoit,A.Finkel,F.Laroussinie,A.Petit,L.Petrucci, P.Schnoebelen. Systems and Software Verification. Model-Checking Techniques and Tools,2001

[Bal04] M.Baldoni,C.Baroglio,I.Gungui,A.Martelli,M.Martelli, V.Mascardi,V.Patti,C.Schifanella. Reasoning about Agents Interaction Protocols inside DCaseLP, DALT'04,2004

[BF95] M.Barbuceanu,M.S.Fox. COOL: a language for describing coordination in multiagent systems. ICMAS 1995

[BF95] M.Barbuceanu,M.S.Fox. COOL: a language for describing coordination in multi-agent systems. Int.Conf. on Multiagent Systems, 17-24,1995

[BGS98] M.Benerecetti,F.Giunchiglia,L.Serafini. Model Checking Multiagent Systems. J.of Logic and Computation. 8(3):401-423,1998

[BGH2004] J.Billington,G.E.Gallasch,B.Han. A coloured Petri Net Approach to Protocol Verification. ACPN 2003, LNCS 3098, 210-290,2004

[BMO2001] B.Bauer,J.P.Muller,J.Odell. Agent UML: A Formalism for Specifying Multiagent Interaction. Agent-Oriented Software Engineering, Springer, 91-103,2001

[BPEL4WS] BPEL4WS, www-106.ibm.com/developerworks/library/ws-bpel

[Br03] M.Broy. Unifying models and engineering theories of composed software systems. Models, Algebras and Logics of Engineering Software, 1-41,2003

[CCFL99] R.S.Cost,Y.Chen,T.Finin,Y.Labrou,Y.Peng. Modeling agent conversation with colored petri nets. Autonomous Agents Work. on Conversation Policies, 1999

[CDV02] D.Calvanese,G.De Giacomo,M.Y.Vardi. Reasoning about Actions and Planning in LTL Action Theories. KR'02, 2002

[CGP2000] E.Clarke,O.Grumberg,D.Peled. ModelChecking. MIT Press, 2000

[CT2004] R.Cervenka,I.Trencansky. Agent Modeling Language, Language Specification. Draft proposal v.0.9, Whitestein Technologies

[EMST04] U.Endriss,N.Maudet,F.Sadri,F.Toni. Logic-based agent communication protocols. LNAI 2922, 91-107,2004

[ES03] J.Euzenat,H.Stuckenschmidt. The family of languages approach to the semantic interoperability. Knowledge Transformation for the Semantic Web,2003

[Ev03] A.Evans,G.Maskeri,P.Sammut,J.S.Willans. Building families of languages for model-driven system development. Work. in Software Model Engineering, 2003

[GC2004] M.Alberti,F.Chesani,M.Gavanelli,E.Lamma,P.Mello,P.Torroni. The SOCS Computational Logic Approach to the Specification and Verification of Agent Societies. Global Computing Work., LNAI 3267,2004

[GMP2004] B.Genest,A.Muscholl,D.Peled. Message Sequence Charts. ACPN 2003, LNCS 3098, 537-558,2004

[GMS00a] L.Giordano,A.Martelli,C.B.Schwind. Ramification and Causality in a Modal Action Logic. J.of Logic and Computation, 10(5):625-662,2000

[GMS00b] L.Giordano,A.Martelli,C.Schwind. Reasoning about Actions in Dynamic Linear Time Temporal Logic. J.of IGPL, 9(2):289-303,2001

[GMS04] L.Giordano,A.Martelli,C.Schwind. Verifying Communicating Agents by Model Checking in a Temporal Action Logic. JELIA'04, LNAI 3229,2004

[Gollmann2003] D.Gollman. Analysing Security Protocols. FASec 2002, LNCS 2629, 71-80,2003

[GP03] F.Guerin,J.Pitt. Verification and Compliance Testing. In LNAI 2650, 98-112,2003

[Guerin02] F.Guerin. Specifying Agent Communication Languages. PhD Thesis, Imperial College, London,2002

[Ha04] D.Harel,B.Rumpe. Meaningful Modeling: What's the Semantics of "Semantics"?. IEEE Computer,2004

[Henriksen99] J.G.Henriksen,P.S.Thiagarajan. Dynamic Linear Time Temporal Logic. Annals of Pure and Applied logic, 96(1-3):187-207,1999

[HK03] M.P.Huget, J.L.Koning. Interaction Protocol Engineering. LNAI 2650, 179-193,2003

[Holzmann1992] G.Holzmann. Description and Validation of Computer Protocols. Prentice Hall,1992

[Hu04] R.Hull. Web Services Composition. EDBT Summer School,2004

[Huget2004] M.P.Huget. Agent UML Notation for Multiagent System Design. Internet Computing, IEEE, 8(4):63-71,2004

[KFD98] J.L.Koning,G.Franois,Y.Demazeau. Formalization and pre-validation for interaction protocols in multiagent systems. ECAI 1998

[KS03] J.Koehler,B.Srivastava. Web Service Composition: Current Solutions and Open Problems. Work. on Planning for Web Services, 28-35,2003

[ITU-TS-Z120] ITU-TS recommendation Z.120,1996

[Jensen1997] K.Jensen. Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use, v.1., Monographs in Theoretical Computer Science,1997

[Mallya04] A.U.Mallya,M.P.Singh. A Semantic Approach for Designing E-Business Protocols. Int. Conf. on Web Services, 742-745,2004

[MM02] A.Maedche,B.Motik, N.Silva, R.Volz. MAFRA-A MApping FRAmework for Distributed Ontologies. LNCS 2473,2002

[MM03] D.J.Mandell,S.A.McIlraith. Adapting BPEL4WS for the Semantic Web: The Bottom-Up Approach to Web Service Interoperation. Int. Semantic Web Conf.,2003

[MS01] S.McIlraith,T.Son. Adapting Golog for Programming the Semantic Web. Int.Symp. on Logical Formalization of Commonsense Reasoning, 195-202,2001

[OPB00] J.Odell,H.Parunak,B.Bauer. Extending UML for agents. In Agent-Oriented Information System Work.,2000

[OWLS] OWL-S, www.daml.org/services/owl-s/1.1/,2004

[Pe03] M.Peleg,S.W.Tu,J.Bury,P.Ciccarese,J.Fox,R.A.Greenes,R.Hall, P.D.Johnson,N.Jones,A.Kumar,S.Miksch,S.Quaglini,A.Seyfang,E.H Shortliffe,M.Stefanelli. Comparing computer-interpretable guideline models: a case-study approach. JAMIA 10:52-68,2003

[PL03] W.Penczek,A.Lomuscio. Verifying Epistemic Properties of Multi-agent Systems via Bounded Model Checking. Fundamenta Informaticae, 55(2):167-185,2003

[Pistore01] M.Pistore,P.Traverso. Planning as Model Checking for Extended Goals in Nondeterministic Domains. IJCAI'01, 479-484,2001

[QVT] QVT-Partners. MOF Query/Views/Transformations. OMG Document: ad/2003-08-08

[RFC793] J.Postel. Transmission Control Protocol, STD 7, RFC 793, IETF,1981

[SG00] C.Schlenoff,M.Gruninger,F.Tissot,J.Valois,J.Lubell,J.Lee. The process specification language (PSL): Overview and v. 1.0 specification. 2000. At www.mel.nist.gov/psl/pubs.html

[SOCS] Web site at www-lia.deis.unibo.it/Research/Projects/SOCS

[SPIN] netlib.bell-labs.com/netlib/spin/index.html

[Ter04] P.Terenziani,S.Montani,A.Bottrighi,M.Torchio,G.Molino, G.Correndo. The GLARE approach to Clinical Guidelines: main features, Computer-based Support for Clinical guidelines and Protocols. Symposium on Computerized Guidelines and Protocols, 162-166,2004

[TMT01] P.Terenziani,G.Molino,M.Torchio. A Modular Approach for Representing and Executing Clinical Guidelines, AI in Medicine 23, 249-276,2001

[UML2] UML 2.0 specification. At www.omg.org

[WSFM04] M.Bravetti,G.Zavattaro. Int.Work. on Web Services and Formal Methods, ENTCS 105,2004

[Wooldridge02b] M.Wooldridge,M.Fisher,M.P.Huget,S.Parsons. Model Checking Multi-Agent Systems with MABLE. AAMAS'02, 952-959,2002

[YS02] P.Yolum,M.P.Singh. Flexible Protocol Specification and Execution: Applying Event Calculus Planning using Commitments. AAMAS'02, 527-534,2002
Parole Chiave
SISTEMI MULTIAGENTE; PROTOCOLLI DI INTERAZIONE; VERIFICA AUTOMATICA; LOGICA COMPUTAZIONALE; LOGICA TEMPORALE

Specifica e verifica di protocolli di interazione fra agenti

Università degli Studi di Torino
Abstract
I servizi forniti in molti domini applicativi sempre più possono essere descritti e realizzati come espressione di un insieme di agenti cooperanti. Rispetto all'approccio più tradizionale della programmazione a componenti, il paradigma ad agenti esplicita aspetti sociali, connessi alla caratteristica degli agenti di essere autonomi e proattivi: le componenti comunicano e si coordinano in maniera dinamica, utilizzando linguaggi ad alto livello, per perseguire scopi comuni (o propri). Tra gli aspetti sociali è particolarmente importante definire "regole comportamentali", espresse mediante protocolli di comunicazione (interazione), finalizzate a controllare l'organizzazione del sistema. I protocolli di comunicazione possono essere utilizzati per regolare l'interazione fra gli agenti specificando un insieme di conversazioni accettabili, ossia sequenze di operazioni (in particolare scambi di messaggi) che si possono svolgere fra agenti diversi.
Con la rapida espansione di internet, gli agenti si trovano sempre più ad operare in ambienti fortemente dinamici. Diventa quindi essenziale che gli agenti soddisfino proprietà che ne garantiscano l'interoperabilità, come ad esempio che un agente sia conforme a un protocollo di interazione, che un agente stia rispettando i suoi vincoli sociali o che un protocollo ottenuto per composizione conservi le proprietà dei protocolli che lo compongono.
Per dimostrare se un protocollo garantisce o meno determinate proprietà >>>

Coordinatore Scientifico del Programma di Ricerca
Alberto MARTELLI Università degli Studi di TORINO
Obiettivo del Programma di Ricerca
I servizi forniti in molti domini applicativi sempre più possono essere descritti e realizzati come espressione di un insieme di agenti cooperanti. Rispetto all'approccio più tradizionale della programmazione a componenti, il paradigma ad agenti esplicita aspetti sociali, connessi alla caratteristica degli agenti di essere autonomi e proattivi: le componenti comunicano e si coordinano in maniera dinamica, utilizzando linguaggi ad alto livello, per perseguire scopi comuni (o propri). Tra gli aspetti sociali è particolarmente importante definire "regole comportamentali", espresse mediante protocolli di comunicazione (interazione), finalizzate a controllare l'organizzazione del sistema. I protocolli di comunicazione possono essere utilizzati per regolare l'interazione fra gli agenti specificando un insieme di conversazioni accettabili, ossia sequenze di operazioni (in particolare scambi di messaggi) che si possono svolgere fra agenti diversi.
Già da tempo l'avvento dei sistemi distribuiti ha portato l'attenzione della comunità scientifica sui protocolli di interazione tra le varie entità coinvolte in una computazione. Con la rapida espansione di internet, poi, ha assunto particolare importanza la specifica di protocolli di comunicazione che garantiscano proprietà generali (ad esempio assenza di deadlock nell'interazione) e particolari al protocollo stesso, ed è sorta l'esigenza di poter verificare se un protocollo garantisca o meno determinate proprietà. A tale scopo >>>

Durata
24 mesi
Base di partenza scientifica nazionale o internazionale
I servizi forniti in molti domini applicativi sempre più possono essere descritti e realizzati come espressione di un insieme di agenti cooperanti. Alcuni esempi sono i processi manufatturieri, i web service, i mercati on-line, la gestione distribuita di reti, le presentazioni multimediali. Rispetto all'approccio più tradizionale della programmazione a componenti, il paradigma ad agenti esplicita aspetti sociali, connessi alla caratteristica degli agenti di essere autonomi e proattivi. L'approccio tradizionale si fonda su una visione funzionale, in cui le componenti richiedono determinati input e producono determinati risultati. Il sistema ha un'architettura basata sul principio di decomposizione statica-funzionale dove le interazioni fra le componenti sono date dalle loro dipendenze. In quello ad agenti, invece, le componenti comunicano e si coordinano in maniera dinamica, utilizzando linguaggi ad alto livello, per perseguire scopi comuni (o propri). Tra gli aspetti sociali è quindi particolarmente rilevante la definizione di "regole comportamentali", finalizzate a controllare l'organizzazione del sistema; fra queste i protocolli di comunicazione sono l'esempio più significativo. I protocolli di comunicazione possono essere utilizzati per regolare l'interazione fra gli agenti, e per verificare se un agente può o meno fare parte del sistema o per controllare se un sistema si sta comportando nel modo stabilito. In generale, tale astrazione consente di realizzare e gestire >>>