1

Progetto COFIN2003 Progetto COFIN2003

Logica computazionale basata su abduzione per Logica computazionale basata su abduzione per modellare il ragionamento e l'interazione in società modellare il ragionamento e l'interazione in società

di agentidi agentiRISULTATI ED OBIETTIVI FUTURI

Paola Mello DEISPaola Mello DEISUniversità di BolognaUniversità di Bologna

Alessandria, 14 Luglio 2005Alessandria, 14 Luglio 2005

2

Composizione dell’ Unità Composizione dell’ Unità (estensione) (estensione)

• Componenti:Componenti:– Prof. Paola Mello (PO)Prof. Paola Mello (PO)– Prof. Anna Ciampolini (PS)Prof. Anna Ciampolini (PS)– Dr. Ing. Paolo Torroni (Ric)Dr. Ing. Paolo Torroni (Ric)– Dr. Ing. Sergio Storari (Tecnico Laureato- Ferrara)Dr. Ing. Sergio Storari (Tecnico Laureato- Ferrara)– Dr. Ing. Federico Chesani (Dottorando)Dr. Ing. Federico Chesani (Dottorando)

+ Estensione + Estensione (per sperimentazione applicazioni e-commerce, (per sperimentazione applicazioni e-commerce,

negoziazione e aste combinatorie):negoziazione e aste combinatorie): Dr. Ing. Alessio Guerri (Dottorando)Dr. Ing. Alessio Guerri (Dottorando)

Dr. Ing. Dr. Ing. Zeynep Kiziltan Zeynep Kiziltan (Assegnista di Ricerca)(Assegnista di Ricerca)

3

Progetti correlati (in corso)Progetti correlati (in corso)• Progetto di ricerca locale (ex60%)Progetto di ricerca locale (ex60%)

– Un’architettura basata sulla logica per l’integrazione di Un’architettura basata sulla logica per l’integrazione di ragionamento eterogeneoragionamento eterogeneo

• Progetto UE IST-2001-32530 (SOCS)Progetto UE IST-2001-32530 (SOCS)– A computational logic model for the description,

analysis and verification of global and open societies of heterogeneous computees

– ICSTM, City, UCY,ICSTM, City, UCY, UNIBO, UNIPI, UNIFE (finito UNIBO, UNIPI, UNIFE (finito il 30 Giugno 2005)il 30 Giugno 2005)

• Progetto Regionale per Applicazioni in Campo Progetto Regionale per Applicazioni in Campo Medico (SPRING) approvato ed in fase di avvioMedico (SPRING) approvato ed in fase di avvio– Indagine sul Potenziale di Sviluppo delle basi Indagine sul Potenziale di Sviluppo delle basi

Informative SanitarieInformative Sanitarie– Dianoema, UNIFE, BMGDianoema, UNIFE, BMG

4

Attività della U.O. nel progettoAttività della U.O. nel progetto

• Descrivere mediante modelli basati su logica computazionale, il comportamento individuale e collettivo di agenti che interagiscono in società aperte.

• Tali modelli devono permettere sia la specifica formale e la verifica di proprietà, sia la concreta implementazione.

5

Ambito logico-computazionaleAmbito logico-computazionale• Gli agenti e la societa` hanno solo conoscenza

incompleta e non precisa dell'ambiente. • Identificazione di un linguaggio di program-

mazione logica (opportunamento esteso) • Identificazione di procedure di dimostrazione

quale supporto.• Applicabilita` di forme di ragionamento abduttivo

allo scopo di modellare sia le interazioni tra agenti logici, che il comportamento del singolo agente

6

Ambito Applicativo• Analizzare e validare i modelli e i linguaggi

definiti in diversi scenari applicativi. • Realizzazione di interazioni tra agenti

basate su dialoghi, con particolare attenzione alla negoziazione per l’allocazione di risorse.

• Sistemi di supporto alla diagnosi medica e di verifica di protocolli in campo medico (linee guida).

7

RISULTATII anno:• Studio dello stato dell’arte• Definizione di un modello logico-

computazionale adatto a descrivere le interazioni tra agenti in un contesto sociale aperto ed eterogeneo.

SINERGIA CON SOCS

8

RISULTATIII anno : • Definizione di una procedura di dimostrazione

(SCIFF e GSCIFF) per i modelli identificati nel corso del I anno (SOCS)

• Verifiche formali di proprietà (positive e negative) degli agenti e delle società di agenti. (SOCS)

• Studio dell’adeguatezza dei modelli in alcuni ambiti applicativi: – linee guida in campo medico– e-learning.

04/22/23 9

Attivita` ancora in atto• Studio di linguaggi (anche grafici) per la

definizione dei protocolli: aspetti semantici e operazionali.

• Capacità espressiva del linguaggio di definizione (Ics)

• Eseguibilità dei protocolli (dal protocollo/societa` all’agente).

• Proprietà dei protocolli – come esprimerle, come verificarle

04/22/23 10

Situazione attuale

• Linguaggio ICs• Molto potente ed espressivo, forse troppo

(negazione esplicita degli E/EN ? ), forse troppo poco (?)

• Testuale al fine di essere utilizzato, un approccio grafico (più intuitivo) sarebbe utile.

• Definizione e realizzazione di un algoritmo per la traslazione da AUML (o altri linguaggi grafici) ad ICs.

04/22/23 11

Confronto con altri linguaggi per la specifica di protocolli …

• Nell’ambito dei protocolli di interazione in generale:• Message Sequence Charts (apparentemente uno standard nell’ambito

Telecommunications)• Coloured Petri Nets (offrono anche alcuni metodi formali di verifica di

proprietà)• Model Checking & related (ad es. ProMeLa / Spin)

• Nell’ambito dei protocolli di sicurezza:• Tecniche di Model Checking varie, tra cui il progetto AVISPA (IST-2001) con

il sistema On-theFly Model Checker (OFMC, Viganò)

• Nell'ambito delle linee guida in campo medico:• glare, proforma, asbru, guide, ecc.

• Nell'ambito del business:• BPMN, BPEL4WS, ecc.

12

Quadro generale dello studio sulle “proprietà”

• Proprietà dell’interazione– punto di vista del meccanismo: proprietà (negate)

espresse mediante formule (verifica statica)– punto di vista dell’agente: aderenza ai protocolli

(verifica dinamica)• Proprietà generali (del framework)

– well-definedness di programmi e vincoli ICS– proprietà della proof

04/22/23 13

Situazione attuale: verifica di compliance on-the-fly

• Mediante la procedura abduttiva SCIFF:• Corretta• Completa• Termina sotto opportune condizioni sintattiche.

– MA…• Non ha meccanismi di recovery in seguito a violation• Struttura delle violazioni “piatta”: le violazioni sono

tutte uguali, e non c’è possibilità di:1. Distinguere violazioni di divieti (EN) da violazioni di positive

expectation (E)2. L’utente non può indicare diverse gravità di violazioni (uccidere

un uomo è più grave che evadere le tasse…)3. Identificare il colpevole.

04/22/23 14

Situazione attuale:dimostrazione di proprieta`

• Mediante la procedura abduttiva ` g-SCIFF:• Ottenuta come Modifica della SCIFF• Corretta • Non completa • La realizzazione e’ sotto testing, ma andra’

riveduta

04/22/23 15

Situazione attuale:dimostrazione di proprieta`

• Definizione delle proprietà• tramite positive expectations esprimiamo

caratteristiche desiderate• tramite negative expectations esprimiamo

caratteristiche non desiderate.• Nel society goal è possibile inserire anche predicati

generici “dovrebbe” essere possibile esprimere qualunque proprietà

• Per ora ci siamo limitati a:• dimostrare proprietà positive esistenziali• refutare proprietà universali

16

proof procedure per la verifica statica: g-SCIFF

• input:– una sequenza di eventi– KB sociale (statica e dinamica)

• output:– history compliant, oppure– fallimento

• rispetto alla SCIFF, usa un modulo aggiuntivo: fulfiller

17

Fulfiller

• Dato un nodo Nk in cui le exp. pend. sono:

PEXPk = PEXP’ ∪ {E(E,T)}e non sono applicabili transizioni di fulfillment, genera un nodo Nk+1 identico a Nk eccetto che:

PEXPk+1 = PEXP’FULFk+1 = FULFk ∪ {E(E,T)}HAPk+1 = HAPk ∪ {H(E,T)}

04/22/23 18

Domande aperte

• Siamo in grado di esprimere tutte le proprietà che vogliamo?

• Esistono dei criteri su “come” e su “quanto” descrivere un protocollo, al fine di poter garantire la generazione di tutte le history compliant con tale protocollo? Se si, quali?

• Data la descrizione di un protocollo, come generare tutte le history compliant? (quale transizione di fulfiller?)

• A cosa ci serve esattamente tutta la potenza concessa dal nostro formalismo?

19

Conclusioni• Studio delle proprietà dei protocolli di sicurezza

tramite ALP :Case study: Needham-Schroeder

• verifica che il protocollo (non) è ‘sicuro’• generazione dell’attacco di Lowe

• È possibile trattare due tipi diversi di verifica in un unico framework

• Implementazione e sperimentazione– migliorare efficienza e proseguire con testing

• Proprietà di soundness, termination, (completeness) per SCIFF e g-SCIFF– da verificare: completezza di g-SCIFF

20

Pubblicazioni 20051. Marco Alberti, Federico Chesani, Marco Gavanelli, Alessio Guerri,

Evelina Lamma, Paola Mello, and Paolo Torroni. “Expressing interaction in combinatorial auction through social integrity constraints”. Intelligenza Artificiale, II(1):22-29, 2005.

2. Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, Paola Mello, and Paolo Torroni. “Security protocols verification in Abductive Logic Programming: a case study”. CILC 2005, Roma, June 21-22, 2005.

3. Marco Alberti, Federico Chesani. “The computational behaviour of the SCIFF abductive proof procedure and the SOCS-SI system”. RCRA 2005, Ferrara, June 10, 2005.

4. Anna Ciampolini, Paola Mello, Marco Montali, Sergio Storari. “Using social integrity constraints for on-the-fly compliance verification of medical protocol”. Proceedings of the CBMS 2005 conference, LNCS, Springer -Verlag, Dublin, 23-24, June 2005.

21

Pubblicazioni 20055. Marco Alberti, Marco Gavanelli, Evelina Lamma, Paola Mello, Giovanni Sartor,

Paolo Torroni. “Mapping Deontic Operators into Abductive Expectations”. 1st International Symposium on Normative Multiagent Systems (NorMAS2005), April 2005.

6. Marco Alberti, Federico Chesani, Marco Gavanelli, Alessio Guerri, Evelina Lamma, Michela Milano, and Paolo Torroni. “Expressing interaction in combinatorial auction through social integrity constraints”. W(C)LP 2005, Ulm, February 2005, pages 53-64.

7. Marco Alberti, Federico Chesani, Marco Gavanelli, and Evelina Lamma. “The CHR-based implementation of a system for generation and confirmation of hypotheses”. W(C)LP 2005, Ulm, February 2005, pages 111-122.

8. Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, Paola Mello, and Paolo Torroni. “The SOCS computational logic approach to the specification and verification of agent societies”. In Priami and Quaglia editors, Global Computing: IST/FET International Workshop, GC 2004 Rovereto, Revised Selected Papers, volume 3267 of LNCS, February 2005. Springer Verlag.

9. Marco Alberti, Marco Gavanelli, Evelina Lamma, Paola Mello, and Paolo Torroni. The SCIFF abductive proof-procedure. In Fabio Zanzotto, editor, IX Congresso nazionale Associazione Italiana per l'Intelligenza Artificiale, Lecture Notes in Artificial Intelligence, Berlin, 2005. Università degli studi di Milano Bicocca, Springer Verlag. to appear

22

Risultati generali:(1) proprietà della SCIFF

• Soundness:– data una istanza di società SHAP

f,– dato un goal G

SHAPi ⊢ G

EXP HAPf

SHAPf ⊨ G

EXP

con expect. answ. (EXP ∪ FULF,)

23

Risultati generali:(1) proprietà della SCIFF

• Completeness: – esiste una proof di completezza per la SCIFF,

con le seguenti restrizioni:• negli abducibili non compaiono variabili

quantificate universalmente• non esistono literal ¬H

– ongoing work: rilassare queste restrizioni

24

Risultati generali:(1) proprietà della SCIFF

• Termination– la SCIFF termina se:

• i vincoli di integrità sociali + social KB costituiscono nell’insieme un programma aciclico rispetto a un level mapping, e

• il goal G e tutte le implicazioni negli ICS sono bounded rispetto a tale level mapping

25

Risultati generali:(2) proprietà della g-SCIFF

• Soundness:– data una istanza di società SHAP

i,– dato un goal G

SHAPi ⊢ G

EXPg HAPf

SHAPf ⊨ G

EXP

con expectation answer (EXP,)

26

Risultati generali:(2) proprietà della g-SCIFF

• Termination– la g-SCIFF termina se i vincoli di integrità

sociali + social KB + il vincolo:

E( X, T ) ⇒ H( X, T )costituiscono nell’insieme un programma aciclico.